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

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/CategoryTheory/Limits/Shapes/Reflexive.lean

@@ -514,7 +514,7 @@ lemma mk_π {X : C} (π : F.obj zero ⟶ X) (h : F.map left ≫ π = F.map right
     (mk π h).π = π := rfl
 
 lemma condition (G : ReflexiveCofork F) : F.map left ≫ G.π = F.map right ≫ G.π := by
-  erw [Cocone.w G left, Cocone.w G right]
+  rw [Cocone.w G left, Cocone.w G right]
 
 @[simp]
 lemma app_one_eq_π (G : ReflexiveCofork F) : G.ι.app zero = G.π := rfl

Mathlib/CategoryTheory/Shift/Basic.lean

@@ -519,7 +519,7 @@ lemma shiftFunctorCompIsoId_add'_inv_app :
   dsimp [shiftFunctorCompIsoId]
   simp only [Functor.map_comp, Category.assoc]
   congr 1
-  erw [← NatTrans.naturality]
+  rw [← NatTrans.naturality]
   dsimp
   rw [← cancel_mono ((shiftFunctorAdd' C p' p 0 hp).inv.app X), Iso.hom_inv_id_app,
     Category.assoc, Category.assoc, Category.assoc, Category.assoc,

Mathlib/Condensed/Discrete/Colimit.lean

@@ -276,7 +276,7 @@ lemma isoLocallyConstantOfIsColimit_inv (X : Profinite.{u}ᵒᵖ ⥤ Type (u+1))
   simp only [types_comp_apply, isoFinYoneda_inv_app, counitApp_app]
   apply presheaf_ext.{u, u+1} (X := X) (Y := X) (f := f)
   intro x
-  erw [incl_of_counitAppApp]
+  rw [incl_of_counitAppApp]
   simp only [counitAppAppImage, CompHausLike.coe_of]
   letI : Fintype (fiber.{u, u+1} f x) :=
     Fintype.ofInjective (sigmaIncl.{u, u+1} f x).1 Subtype.val_injective
@@ -551,7 +551,7 @@ lemma isoLocallyConstantOfIsColimit_inv (X : LightProfinite.{u}ᵒᵖ ⥤ Type u
   simp only [types_comp_apply, isoFinYoneda_inv_app, counitApp_app]
   apply presheaf_ext.{u, u} (X := X) (Y := X) (f := f)
   intro x
-  erw [incl_of_counitAppApp]
+  rw [incl_of_counitAppApp]
   simp only [counitAppAppImage, CompHausLike.coe_of]
   letI : Fintype (fiber.{u, u} f x) :=
     Fintype.ofInjective (sigmaIncl.{u, u} f x).1 Subtype.val_injective

Mathlib/Geometry/RingedSpace/OpenImmersion.lean

@@ -1120,8 +1120,8 @@ theorem lift_range (H' : Set.range g.base ⊆ Set.range f.base) :
   have : _ = (pullback.fst f g).base :=
     PreservesPullback.iso_hom_fst
       (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _) f g
-  rw [LocallyRingedSpace.comp_base, ← this, ← Category.assoc, coe_comp]
-  rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ]
+  rw [LocallyRingedSpace.comp_base, ← this, ← Category.assoc, coe_comp, Set.range_comp,
+      Set.range_iff_surjective.mpr, Set.image_univ]
   -- Porting note (#11224): change `rw` to `erw` on this lemma
   · erw [TopCat.pullback_fst_range]
     ext

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.")

Mathlib/Topology/Order/ScottTopology.lean

@@ -177,7 +177,7 @@ variable {α D}
 
 lemma isOpen_iff [IsScottHausdorff α D] :
     IsOpen s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a : α⦄, IsLUB d a →
-      a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s := by erw [topology_eq_scottHausdorff (α := α) (D := D)]; rfl
+      a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s := by rw [topology_eq_scottHausdorff (α := α) (D := D)]; rfl
 
 lemma dirSupInaccOn_of_isOpen [IsScottHausdorff α D] (h : IsOpen s) : DirSupInaccOn D s :=
   fun d hd₀ hd₁ hd₂ a hda hd₃ ↦ by
@@ -241,7 +241,7 @@ lemma topology_eq [IsScott α D] : ‹_› = scott α D := topology_eq_scott
 variable {α} {D} {s : Set α} {a : α}
 
 lemma isOpen_iff_isUpperSet_and_scottHausdorff_open [IsScott α D] :
-    IsOpen s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s := by erw [topology_eq α D]; rfl
+    IsOpen s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s := by rw [topology_eq α D]; rfl
 
 lemma isOpen_iff_isUpperSet_and_dirSupInaccOn [IsScott α D] :
     IsOpen s ↔ IsUpperSet s ∧ DirSupInaccOn D s := by