Fixes from the erw linter

leanprover-community · Oct 18, 2024 · af3c28c · af3c28c
1 parent 109e158
commit af3c28c
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 8 deletions.
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean b/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

diff --git a/Mathlib/CategoryTheory/Shift/Basic.lean b/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,

diff --git a/Mathlib/Condensed/Discrete/Colimit.lean b/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

diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/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

diff --git a/Mathlib/Topology/Order/ScottTopology.lean b/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