feat(Tactic): erw tries rw first and warns if that succeeds

This PR adds a macro rule to the `erw` tactic that first tries `rw` at reducible transparency, and displays a "Try this:" if that succeeded. This should help us get rid of uselessly slow `erw`s.

This is a relatively simple implementation that does not verify if `erw` and `rw` would have resulted in the same exact rewrite. So it is possible that `erw` and `rw` both succeed but rewrite different occurrences, and there would be a suggestion to replace `erw` with `rw` in that case. I think the complication of running both at the same time and checking the goal state afterwards doesn't weigh up to accepting that this happens and adding an explanation to the warning generated by `erw`.

I import the `erw` extension in `Tactic.Common`: it might be nice to migrate this up even earlier in the import hierarchy but `Mathlib.Tactic.TryThis` is a somewhat heavy import to put in `Mathlib.Tactic.Core`.

Mathlib.lean

@@ -4307,6 +4307,7 @@ import Mathlib.Tactic.DeriveFintype
 import Mathlib.Tactic.DeriveToExpr
 import Mathlib.Tactic.DeriveTraversable
 import Mathlib.Tactic.Eqns
+import Mathlib.Tactic.Erw
 import Mathlib.Tactic.Eval
 import Mathlib.Tactic.ExistsI
 import Mathlib.Tactic.Explode

Mathlib/Tactic.lean

@@ -69,6 +69,7 @@ import Mathlib.Tactic.DeriveFintype
 import Mathlib.Tactic.DeriveToExpr
 import Mathlib.Tactic.DeriveTraversable
 import Mathlib.Tactic.Eqns
+import Mathlib.Tactic.Erw
 import Mathlib.Tactic.Eval
 import Mathlib.Tactic.ExistsI
 import Mathlib.Tactic.Explode

Mathlib/Tactic/Common.lean

@@ -47,6 +47,7 @@ import Mathlib.Tactic.DefEqTransformations
 import Mathlib.Tactic.DeprecateMe
 import Mathlib.Tactic.DeriveToExpr
 import Mathlib.Tactic.Eqns
+import Mathlib.Tactic.Erw
 import Mathlib.Tactic.ExistsI
 import Mathlib.Tactic.ExtractGoal
 import Mathlib.Tactic.ExtractLets

Mathlib/Tactic/Erw.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2024 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+
+import Mathlib.Tactic.TryThis
+
+/-!
+# Extension to the `erw` tactic
+
+This file adds a macro rule to the `erw` tactic that first tries to run the `rw` tactic at the
+faster `reducible` transparency, and adds a suggestion if that also succeeds.
+
+Note that `rw` succeeding is not the same as `rw` and `erw` doing exactly the same rewrite: they may
+have operated on different subterms. Since the suggested `rw` may not be an exact replacement, we
+display a hint explaining what to do if this happens.
+-/
+
+/-- If we call `erw`, first try running regular `rw` and warn if that succeds. -/
+macro_rules
+  | `(tactic| erw $s $(loc)?) =>
+    `(tactic|
+      try_this rw $(.none)? $s $(loc)?;
+      trace "Hint: `rw` succeeded here, but may have performed a different rewrite than `erw` would.
+If `erw` really is needed, try preceding this line with a `rw` to get rid of the other occurrences,
+or use `conv` to specify exactly which subterm to rewrite.")