chore(*): replace erw with rw where possible (#17703)

Go through Mathlib and replace `erw` calls where `rw` would also succeed.

This PR is split off from #17638, containing all the changes that the linter suggested.



Co-authored-by: Anne Baanen <[email protected]>

Archive/Wiedijk100Theorems/Partition.lean

@@ -329,7 +329,7 @@ theorem partialDistinctGF_prop [CommSemiring α] (n m : ℕ) :
 -/
 theorem distinctGF_prop [CommSemiring α] (n m : ℕ) (h : n < m + 1) :
     ((Nat.Partition.distincts n).card : α) = coeff α n (partialDistinctGF m) := by
-  erw [← partialDistinctGF_prop, Nat.Partition.distincts]
+  rw [← partialDistinctGF_prop, Nat.Partition.distincts]
   congr with p
   apply (and_iff_left _).symm
   intro i hi

Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean

@@ -201,7 +201,7 @@ instance : Subsingleton (SMulCandidate α φ r m) where
       all_goals apply Presheaf.imageSieve_mem
     apply A.isSeparated _ _ hS
     intro Y f ⟨⟨r₀, hr₀⟩, ⟨m₀, hm₀⟩⟩
-    erw [h₁ f.op r₀ hr₀ m₀ hm₀, h₂ f.op r₀ hr₀ m₀ hm₀]
+    rw [h₁ f.op r₀ hr₀ m₀ hm₀, h₂ f.op r₀ hr₀ m₀ hm₀]
 
 noncomputable instance : Unique (SMulCandidate α φ r m) :=
   uniqueOfSubsingleton (Nonempty.some inferInstance)
@@ -225,13 +225,13 @@ protected lemma one_smul : smul α φ 1 m = m := by
 protected lemma zero_smul : smul α φ 0 m = 0 := by
   apply A.isSeparated _ _ (Presheaf.imageSieve_mem J φ m)
   rintro Y f ⟨m₀, hm₀⟩
-  erw [map_smul_eq α φ 0 m f.op 0 (by simp) m₀ hm₀, zero_smul, map_zero,
+  rw [map_smul_eq α φ 0 m f.op 0 (by simp) m₀ hm₀, zero_smul, map_zero,
     (A.val.map f.op).map_zero]
 
 protected lemma smul_zero : smul α φ r 0 = 0 := by
   apply A.isSeparated _ _ (Presheaf.imageSieve_mem J α r)
   rintro Y f ⟨r₀, hr₀⟩
-  erw [(A.val.map f.op).map_zero, map_smul_eq α φ r 0 f.op r₀ hr₀ 0 (by simp),
+  rw [(A.val.map f.op).map_zero, map_smul_eq α φ r 0 f.op r₀ hr₀ 0 (by simp),
     smul_zero, map_zero]
 
 protected lemma smul_add : smul α φ r (m + m') = smul α φ r m + smul α φ r m' := by
@@ -241,7 +241,7 @@ protected lemma smul_add : smul α φ r (m + m') = smul α φ r m + smul α φ r
     all_goals apply Presheaf.imageSieve_mem
   apply A.isSeparated _ _ hS
   rintro Y f ⟨⟨⟨r₀, hr₀⟩, ⟨m₀ : M₀.obj _, hm₀⟩⟩, ⟨m₀' : M₀.obj _, hm₀'⟩⟩
-  erw [(A.val.map f.op).map_add, map_smul_eq α φ r m f.op r₀ hr₀ m₀ hm₀,
+  rw [(A.val.map f.op).map_add, map_smul_eq α φ r m f.op r₀ hr₀ m₀ hm₀,
     map_smul_eq α φ r m' f.op r₀ hr₀ m₀' hm₀',
     map_smul_eq α φ r (m + m') f.op r₀ hr₀ (m₀ + m₀')
       (by rw [map_add, map_add, hm₀, hm₀']),
@@ -254,7 +254,7 @@ protected lemma add_smul : smul α φ (r + r') m = smul α φ r m + smul α φ r
     all_goals apply Presheaf.imageSieve_mem
   apply A.isSeparated _ _ hS
   rintro Y f ⟨⟨⟨r₀ : R₀.obj _, hr₀⟩, ⟨r₀' : R₀.obj _, hr₀'⟩⟩, ⟨m₀, hm₀⟩⟩
-  erw [(A.val.map f.op).map_add, map_smul_eq α φ r m f.op r₀ hr₀ m₀ hm₀,
+  rw [(A.val.map f.op).map_add, map_smul_eq α φ r m f.op r₀ hr₀ m₀ hm₀,
     map_smul_eq α φ r' m f.op r₀' hr₀' m₀ hm₀,
     map_smul_eq α φ (r + r') m f.op (r₀ + r₀') (by rw [map_add, map_add, hr₀, hr₀'])
       m₀ hm₀, add_smul, map_add]
@@ -266,7 +266,7 @@ protected lemma mul_smul : smul α φ (r * r') m = smul α φ r (smul α φ r' m
     all_goals apply Presheaf.imageSieve_mem
   apply A.isSeparated _ _ hS
   rintro Y f ⟨⟨⟨r₀ : R₀.obj _, hr₀⟩, ⟨r₀' : R₀.obj _, hr₀'⟩⟩, ⟨m₀ : M₀.obj _, hm₀⟩⟩
-  erw [map_smul_eq α φ (r * r') m f.op (r₀ * r₀')
+  rw [map_smul_eq α φ (r * r') m f.op (r₀ * r₀')
     (by rw [map_mul, map_mul, hr₀, hr₀']) m₀ hm₀, mul_smul,
     map_smul_eq α φ r (smul α φ r' m) f.op r₀ hr₀ (r₀' • m₀)
       (map_smul_eq α φ r' m f.op r₀' hr₀' m₀ hm₀).symm]
@@ -292,7 +292,7 @@ lemma map_smul :
     all_goals apply Presheaf.imageSieve_mem
   apply A.isSeparated _ _ hS
   rintro Y f ⟨⟨r₀, hr₀⟩, ⟨m₀, hm₀⟩⟩
-  erw [← comp_apply, ← Functor.map_comp,
+  rw [← comp_apply, ← Functor.map_comp,
     map_smul_eq α φ r m (π ≫ f.op) r₀ (by rw [hr₀, Functor.map_comp, comp_apply]) m₀
       (by rw [hm₀, Functor.map_comp, comp_apply]),
     map_smul_eq α φ (R.val.map π r) (A.val.map π m) f.op r₀ hr₀ m₀ hm₀]

Mathlib/Algebra/Homology/ShortComplex/Ab.lean

@@ -37,7 +37,7 @@ variable (S : ShortComplex Ab.{u})
 
 @[simp]
 lemma ab_zero_apply (x : S.X₁) : S.g (S.f x) = 0 := by
-  erw [← comp_apply, S.zero]
+  rw [← comp_apply, S.zero]
   rfl
 
 /-- The canonical additive morphism `S.X₁ →+ AddMonoidHom.ker S.g` induced by `S.f`. -/
@@ -81,7 +81,7 @@ noncomputable def abCyclesIso : S.cycles ≅ AddCommGrp.of (AddMonoidHom.ker S.g
 lemma abCyclesIso_inv_apply_iCycles (x : AddMonoidHom.ker S.g) :
     S.iCycles (S.abCyclesIso.inv x) = x := by
   dsimp only [abCyclesIso]
-  erw [← comp_apply, S.abLeftHomologyData.cyclesIso_inv_comp_iCycles]
+  rw [← comp_apply, S.abLeftHomologyData.cyclesIso_inv_comp_iCycles]
   rfl
 
 /-- Given a short complex `S` of abelian groups, this is the isomorphism between
@@ -129,7 +129,7 @@ lemma ab_exact_iff_range_eq_ker : S.Exact ↔ S.f.range = S.g.ker := by
   · intro h
     refine le_antisymm ?_ h
     rintro _ ⟨x₁, rfl⟩
-    erw [AddMonoidHom.mem_ker, ← comp_apply, S.zero]
+    rw [AddMonoidHom.mem_ker, ← comp_apply, S.zero]
     rfl
   · intro h
     rw [h]

Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean

@@ -32,7 +32,7 @@ lemma ShortComplex.zero_apply
     [Limits.HasZeroMorphisms C] [(forget₂ C Ab).PreservesZeroMorphisms]
     (S : ShortComplex C) (x : (forget₂ C Ab).obj S.X₁) :
     ((forget₂ C Ab).map S.g) (((forget₂ C Ab).map S.f) x) = 0 := by
-  erw [← comp_apply, ← Functor.map_comp, S.zero, Functor.map_zero]
+  rw [← comp_apply, ← Functor.map_comp, S.zero, Functor.map_zero]
   rfl
 
 section preadditive

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -326,7 +326,7 @@ theorem range_fromSpec :
   delta IsAffineOpen.fromSpec; dsimp [IsAffineOpen.isoSpec_inv]
   rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ]
   · exact Subtype.range_coe
-  erw [← coe_comp, ← TopCat.epi_iff_surjective] -- now `erw` after #13170
+  rw [← coe_comp, ← TopCat.epi_iff_surjective]
   infer_instance
 
 @[simp]
@@ -398,7 +398,7 @@ theorem _root_.AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion
   refine ⟨fun hU => @isAffine_of_isIso _ _
     (IsOpenImmersion.isoOfRangeEq (X.ofRestrict U.openEmbedding ≫ f) (Y.ofRestrict _) ?_).hom ?_ hU,
     fun hU => hU.image_of_isOpenImmersion f⟩
-  · erw [Scheme.comp_val_base, coe_comp, Set.range_comp] -- now `erw` after #13170
+  · rw [Scheme.comp_val_base, coe_comp, Set.range_comp]
     dsimp [Opens.coe_inclusion', Scheme.restrict]
     erw [Subtype.range_coe, Subtype.range_coe] -- now `erw` after #13170
     rfl

Mathlib/AlgebraicGeometry/Cover/Open.lean

@@ -106,7 +106,7 @@ def OpenCover.bind (f : ∀ x : 𝒰.J, OpenCover (𝒰.obj x)) : OpenCover X wh
     change x ∈ Set.range ((f (𝒰.f x)).map ((f (𝒰.f x)).f y) ≫ 𝒰.map (𝒰.f x)).1.base
     use z
     erw [comp_apply]
-    erw [hz, hy] -- now `erw` after #13170
+    rw [hz, hy]
   -- Porting note: weirdly, even though no input is needed, `inferInstance` does not work
   -- `PresheafedSpace.IsOpenImmersion.comp` is marked as `instance`
   IsOpen x := PresheafedSpace.IsOpenImmersion.comp _ _

Mathlib/AlgebraicGeometry/Gluing.lean

@@ -228,15 +228,13 @@ theorem ι_eq_iff (i j : D.J) (x : (D.U i).carrier) (y : (D.U j).carrier) :
     (TopCat.GlueData.ι_eq_iff_rel
       D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData
       i j x y)
-  rw [← ((TopCat.mono_iff_injective D.isoCarrier.inv).mp _).eq_iff]
-  · erw [← comp_apply] -- now `erw` after #13170
-    simp_rw [← D.ι_isoCarrier_inv]
+  rw [← ((TopCat.mono_iff_injective D.isoCarrier.inv).mp _).eq_iff, ← comp_apply]
+  · simp_rw [← D.ι_isoCarrier_inv]
     rfl -- `rfl` was not needed before #13170
   · infer_instance
 
 theorem isOpen_iff (U : Set D.glued.carrier) : IsOpen U ↔ ∀ i, IsOpen ((D.ι i).1.base ⁻¹' U) := by
-  rw [← (TopCat.homeoOfIso D.isoCarrier.symm).isOpen_preimage]
-  rw [TopCat.GlueData.isOpen_iff]
+  rw [← (TopCat.homeoOfIso D.isoCarrier.symm).isOpen_preimage, TopCat.GlueData.isOpen_iff]
   apply forall_congr'
   intro i
   rw [← Set.preimage_comp, ← ι_isoCarrier_inv]
@@ -342,7 +340,7 @@ theorem fromGlued_injective : Function.Injective 𝒰.fromGlued.1.base := by
   intro x y h
   obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x
   obtain ⟨j, y, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective y
-  erw [← comp_apply, ← comp_apply] at h -- now `erw` after #13170
+  rw [← comp_apply, ← comp_apply] at h
   simp_rw [← SheafedSpace.comp_base, ← LocallyRingedSpace.comp_val] at h
   erw [ι_fromGlued, ι_fromGlued] at h
   let e :=
@@ -390,7 +388,7 @@ instance : Epi 𝒰.fromGlued.val.base := by
   intro x
   obtain ⟨y, h⟩ := 𝒰.covers x
   use (𝒰.gluedCover.ι (𝒰.f x)).1.base y
-  erw [← comp_apply] -- now `erw` after #13170
+  rw [← comp_apply]
   rw [← 𝒰.ι_fromGlued (𝒰.f x)] at h
   exact h
 

Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean

@@ -112,8 +112,7 @@ theorem iso_isometry_of_normNoninc {V W : SemiNormedGrp} (i : V ≅ W) (h1 : i.h
   intro v
   apply le_antisymm (h1 v)
   calc
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    ‖v‖ = ‖i.inv (i.hom v)‖ := by erw [Iso.hom_inv_id_apply]
+    ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [Iso.hom_inv_id_apply]
     _ ≤ ‖i.hom v‖ := h2 _
 
 end SemiNormedGrp

Mathlib/Analysis/Normed/Group/SemiNormedGrp/Completion.lean

@@ -94,8 +94,7 @@ instance : Preadditive SemiNormedGrp.{u} where
     -- Porting note: failing simps probably due to instance synthesis issues with concrete
     -- cats; see the gymnastics below for what used to be
     -- simp only [add_apply, comp_apply. map_add]
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    rw [NormedAddGroupHom.add_apply]; erw [CategoryTheory.comp_apply, CategoryTheory.comp_apply,
+    rw [NormedAddGroupHom.add_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply,
       CategoryTheory.comp_apply, @NormedAddGroupHom.add_apply _ _ (_) (_)]
     convert map_add g (f x) (f' x)
   comp_add _ _ _ _ _ _ := by

Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean

@@ -145,14 +145,12 @@ def cokernelCocone {X Y : SemiNormedGrp.{u}} (f : X ⟶ Y) : Cofork f 0 :=
       ext a
       simp only [comp_apply, Limits.zero_comp]
       -- Porting note: `simp` not firing on the below
-      -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-      erw [comp_apply, NormedAddGroupHom.zero_apply]
+      rw [comp_apply, NormedAddGroupHom.zero_apply]
       -- Porting note: Lean 3 didn't need this instance
       letI : SeminormedAddCommGroup ((forget SemiNormedGrp).obj Y) :=
         (inferInstance : SeminormedAddCommGroup Y)
       -- Porting note: again simp doesn't seem to be firing in the below line
-      -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-      erw [← NormedAddGroupHom.mem_ker, f.range.ker_normedMk, f.mem_range]
+      rw [← NormedAddGroupHom.mem_ker, f.range.ker_normedMk, f.mem_range]
     -- This used to be `simp only [exists_apply_eq_apply]` before leanprover/lean4#2644
       convert exists_apply_eq_apply f a)
 

Mathlib/Geometry/RingedSpace/OpenImmersion.lean

@@ -1119,17 +1119,15 @@ theorem lift_range (H' : Set.range g.1.base ⊆ Set.range f.1.base) :
   have : _ = (pullback.fst f g).val.base :=
     PreservesPullback.iso_hom_fst
       (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _) f g
-  erw [LocallyRingedSpace.comp_val, SheafedSpace.comp_base, ← this, ← Category.assoc, coe_comp]
-   -- now `erw` after #13170
-  rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ]
+  rw [LocallyRingedSpace.comp_val, SheafedSpace.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
     constructor
     · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
     · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
-  · erw [← TopCat.epi_iff_surjective] -- now `erw` after #13170
-    rw [show (inv (pullback.snd f g)).val.base = _ from
+  · rw [← TopCat.epi_iff_surjective, show (inv (pullback.snd f g)).val.base = _ from
         (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _).map_inv _]
     infer_instance
 

Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

@@ -190,20 +190,18 @@ theorem snd_invApp_t_app' (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k)
     replace this := (congr_arg ((PresheafedSpace.Hom.base ·)) this).symm
     replace this := congr_arg (ContinuousMap.toFun ·) this
     dsimp at this
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [coe_comp, coe_comp] at this
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [this, Set.image_comp, Set.image_comp, Set.preimage_image_eq]
+    rw [coe_comp, coe_comp] at this
+    rw [this, Set.image_comp, Set.image_comp, Set.preimage_image_eq]
     swap
     · refine Function.HasLeftInverse.injective ⟨(D.t i k).base, fun x => ?_⟩
-      erw [← comp_apply, ← comp_base, D.t_inv, id_base, id_apply] -- now `erw` after #13170
+      rw [← comp_apply, ← comp_base, D.t_inv, id_base, id_apply]
     refine congr_arg (_ '' ·) ?_
     refine congr_fun ?_ _
     refine Set.image_eq_preimage_of_inverse ?_ ?_
     · intro x
-      erw [← comp_apply, ← comp_base, IsIso.inv_hom_id, id_base, id_apply] -- now `erw` after #13170
+      rw [← comp_apply, ← comp_base, IsIso.inv_hom_id, id_base, id_apply]
     · intro x
-      erw [← comp_apply, ← comp_base, IsIso.hom_inv_id, id_base, id_apply] -- now `erw` after #13170
+      rw [← comp_apply, ← comp_base, IsIso.hom_inv_id, id_base, id_apply]
   · rw [← IsIso.eq_inv_comp, IsOpenImmersion.inv_invApp, Category.assoc,
       (D.t' k i j).c.naturality_assoc]
     simp_rw [← Category.assoc]
@@ -260,7 +258,7 @@ theorem ι_image_preimage_eq (i j : D.J) (U : Opens (D.U i).carrier) :
     change (D.t i j ≫ D.t j i).base '' _ = _
     rw [𝖣.t_inv]
     simp
-  · erw [← coe_comp, ← TopCat.mono_iff_injective] -- now `erw` after #13170
+  · rw [← coe_comp, ← TopCat.mono_iff_injective]
     infer_instance
 
 /-- (Implementation). The map `Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_{U_j}, 𝖣.ι j ⁻¹' (𝖣.ι i '' U))` -/
@@ -412,9 +410,9 @@ theorem ιInvApp_π {i : D.J} (U : Opens (D.U i).carrier) :
     · exact h2.symm
     · have := D.ι_gluedIso_inv (PresheafedSpace.forget _) i
       dsimp at this
-      erw [← this, coe_comp] -- now `erw` after #13170
+      rw [← this, coe_comp]
       refine Function.Injective.comp ?_ (TopCat.GlueData.ι_injective D.toTopGlueData i)
-      erw [← TopCat.mono_iff_injective] -- now `erw` after #13170
+      rw [← TopCat.mono_iff_injective]
       infer_instance
   delta ιInvApp
   rw [limit.lift_π]

Mathlib/Topology/Category/TopCat/Limits/Products.lean

@@ -224,7 +224,7 @@ theorem range_prod_map {W X Y Z : TopCat.{u}} (f : W ⟶ Y) (g : X ⟶ Z) :
   · rintro ⟨y, rfl⟩
     simp_rw [Set.mem_inter_iff, Set.mem_preimage, Set.mem_range]
     -- sizable changes in this proof after #13170
-    erw  [← comp_apply, ← comp_apply]
+    rw [← comp_apply, ← comp_apply]
     simp_rw [Limits.prod.map_fst,
       Limits.prod.map_snd, comp_apply]
     exact ⟨exists_apply_eq_apply _ _, exists_apply_eq_apply _ _⟩

Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean

@@ -71,12 +71,14 @@ def pullbackConeIsLimit (f : X ⟶ Z) (g : Y ⟶ Z) : IsLimit (pullbackCone f g)
       refine ⟨?_, ?_, ?_⟩
       · delta pullbackCone
         ext a
-        -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-        erw [comp_apply, ContinuousMap.coe_mk]
+        -- This used to be `rw`, but we need `rw; rfl` after leanprover/lean4#2644
+        rw [comp_apply, ContinuousMap.coe_mk]
+        rfl
       · delta pullbackCone
         ext a
-        -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-        erw [comp_apply, ContinuousMap.coe_mk]
+        -- This used to be `rw`, but we need `rw; rfl` after leanprover/lean4#2644
+        rw [comp_apply, ContinuousMap.coe_mk]
+        rfl
       · intro m h₁ h₂
         -- Porting note (#11041): used to be `ext x`.
         apply ContinuousMap.ext; intro x
@@ -198,13 +200,13 @@ theorem range_pullback_map {W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶
   constructor
   · rintro ⟨y, rfl⟩
     simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_range]
-    erw [← comp_apply, ← comp_apply] -- now `erw` after #13170
+    rw [← comp_apply, ← comp_apply]
     simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, comp_apply]
     exact ⟨exists_apply_eq_apply _ _, exists_apply_eq_apply _ _⟩
   rintro ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩⟩
   have : f₁ x₁ = f₂ x₂ := by
     apply (TopCat.mono_iff_injective _).mp H₃
-    erw [← comp_apply, eq₁, ← comp_apply, eq₂, -- now `erw` after #13170
+    rw [← comp_apply, eq₁, ← comp_apply, eq₂,
       comp_apply, comp_apply, hx₁, hx₂, ← comp_apply, pullback.condition]
     rfl -- `rfl` was not needed before #13170
   use (pullbackIsoProdSubtype f₁ f₂).inv ⟨⟨x₁, x₂⟩, this⟩