This makes `linarith` print the goal (including hypotheses) when it fails, as many other tactics do.

This was motivated by watching the `sagredo` tactic trying to use `linarith`, but failing to see that it didn't quite have the correct hypotheses yet. Once it gave up on using `linarith`, it tried `contradiction`, which printed a more helpful error message (in which a human, although not quite GPT, could easily see the inequalities weren't quite right).



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

Per suggestion on [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/New.20.60propose.60.20tactic/near/350961701).



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Those used to be necessary because of a linarith bug, which was fixed in
#2611



Co-authored-by: Moritz Firsching <firsching@google.com>

mac users should have this in their `.gitignore` file, but sometimes don't, as evidenced by #3511, which then unfortunately broke the port-status bot for a day!



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

This PR also make `Prod.rec` computable.



Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

* leanprover-community/mathlib3#18442

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

~~This is still WIP.~~ There may be a change to `reassoc` that would make this nicer, see [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Bug.20in.20reassoc.3F/near/351111877)

Co-authored-by: Moritz Firsching <firsching@google.com>

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

We had some unfortunate spaghetti code in `solve_by_elim`. When @hrmacbeth had requested additional features for `apply_rules`, the easiest way to provide them was to re-use `solve_by_elim`'s parsing and lemma handling. (See #856.) However `apply_rules` doesn't to backtracking, and `solve_by_elim` is all about it. At the time, `solve_by_elim` didn't have clean separation between its "lemma application" and "backtracking" considerations, so the solution was to add some hacks the prevented the backtracking from actually occurring, in the backtracking code...

Since #2920, those considerations have been cleanly separated out. Thus it's possible to greatly simplify how we don't backtrack when we don't want to (in `apply_rules`). This PR does that.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Hide the unsafe inductive powering `ListM` behind a safe API using `implemented_by`.

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

One was missed; curiously it wasn't harmful in `master`, but when we turn on `etaExperiment` globally this causes a breakage 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Johan Commelin <johan@commelin.net>

Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>

…nstantiateMVars` (#3758)

This PR factors out a `MetaM` version of the `rfl` tactic and adds a missing `whnfR` and `instantiateMVars` in front of the goal type. This means that a few `rw`s across mathlib4 now close the goal instead of e.g. requiring a trailing `exact le_rfl`.

Note: we do not use `whnfR` on the return type when adding the `refl` extension in the first place, as `forallMetaTelescopeReducing` already performs `whnf` (here, at reducible transparency).

See [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233758.20.E2.80.93.20rfl.20refactor.20.26.20fix) for some discussion on the internal changes made.



Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

closes #3680, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Stepping.20through.20simp_rw/near/326712986

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Also fixes some spacing in their `syntax` commands, which impacts pretty printing.

Co-authored-by: Moritz Firsching <firsching@google.com>

Co-authored-by: Moritz Firsching <firsching@google.com>

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Komyyy <pol_tta@outlook.jp>

Co-authored-by: Moritz Firsching <firsching@google.com>

Co-authored-by: Moritz Firsching <firsching@google.com>

Match leanprover-community/mathlib3#18512



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

I forgot to update it in #3753.

* `data.mv_polynomial.basic`, `data.mv_polynomial.funext`: leanprover-community/mathlib3#18839
* `category_theory.limits.preserves.finite`, `category_theory.preadditive.projective`:  leanprover-community/mathlib3#18890
* `category_theory.abelian.basic`, `category_theory.abelian.opposite`:  leanprover-community/mathlib3#18740
* `topology.category.Top.limits.basic`: leanprover-community/mathlib3#18871. Note that this does not show a useful diff on the dashboard pages as file splits aren't tracked well by git.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>