chore: clean up after #17615 (#17617)

This PR goes through the diff of #17615, which automatically replaced `erw` with `rw`, to clean up as follows: * delete obsolote comments * merge adjacent `rw` calls * restore old code that was commented out when it broke at some point but now works again Co-authored-by: Anne Baanen <[email protected]>
leanprover-community · Oct 11, 2024 · c585207 · c585207
1 parent e4fa33c
commit c585207
Show file tree

Hide file tree

Showing 31 changed files with 80 additions and 102 deletions.
diff --git a/Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean b/Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean
@@ -136,17 +136,21 @@ theorem toDirectSum_mul [DecidableEq ι] [AddMonoid ι] [Semiring M] (f g : AddM
     AddMonoidHom.mul_apply, Finsupp.singleAddHom_apply]
   -- This was not needed before leanprover/lean4#2644
   erw [AddMonoidHom.compl₂_apply]
+  -- If we remove the next `rw`, the `erw` after it will complain (when we get an `erw` linter)
+  -- that it could be a `rw`. But the `erw` and `rw` will rewrite different occurrences.
+  -- So first get rid of the `rw`-able occurrences to force `erw` to do the expensive rewrite only.
+  rw [AddMonoidHom.coe_mk, AddMonoidHom.coe_mk]
   -- This was not needed before leanprover/lean4#2644
   erw [AddMonoidHom.coe_mk]
   simp only [AddMonoidHom.coe_mk, ZeroHom.coe_mk, toDirectSum_single]
   -- This was not needed before leanprover/lean4#2644
   dsimp
-  erw [AddMonoidAlgebra.single_mul_single, AddMonoidHom.coe_mk, ZeroHom.coe_mk,
+  rw [AddMonoidAlgebra.single_mul_single, AddMonoidHom.coe_mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk,
     AddMonoidAlgebra.toDirectSum_single]
   simp only [AddMonoidHom.coe_comp, AddMonoidHom.coe_mul, AddMonoidHom.coe_mk, ZeroHom.coe_mk,
     Function.comp_apply, toDirectSum_single, AddMonoidHom.id_apply, Finsupp.singleAddHom_apply,
     AddMonoidHom.coe_mulLeft]
-  erw [DirectSum.of_mul_of, Mul.gMul_mul]
+  rw [DirectSum.of_mul_of, Mul.gMul_mul]
 
 end AddMonoidAlgebra
 

diff --git a/Mathlib/Algebra/Polynomial/Module/Basic.lean b/Mathlib/Algebra/Polynomial/Module/Basic.lean
@@ -312,8 +312,7 @@ noncomputable def comp (p : R[X]) : PolynomialModule R M →ₗ[R] PolynomialMod
   LinearMap.comp ((eval p).restrictScalars R) (map R[X] (lsingle R 0))
 
 theorem comp_single (p : R[X]) (i : ℕ) (m : M) : comp p (single R i m) = p ^ i • single R 0 m := by
-  rw [comp_apply]
-  rw [map_single, eval_single]
+  rw [comp_apply, map_single, eval_single]
   rfl
 
 theorem comp_eval (p : R[X]) (q : PolynomialModule R M) (r : R) :

diff --git a/Mathlib/AlgebraicGeometry/Cover/Open.lean b/Mathlib/AlgebraicGeometry/Cover/Open.lean
@@ -73,7 +73,7 @@ def affineCover (X : Scheme.{u}) : OpenCover X where
     rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ]
     · erw [Subtype.range_coe_subtype]
       exact (X.local_affine x).choose.2
-    rw [← TopCat.epi_iff_surjective] -- now `erw` after #13170
+    rw [← TopCat.epi_iff_surjective]
     change Epi ((SheafedSpace.forget _).map (LocallyRingedSpace.forgetToSheafedSpace.map _))
     infer_instance
 
@@ -136,7 +136,7 @@ def OpenCover.copy {X : Scheme.{u}} (𝒰 : OpenCover X) (J : Type*) (obj : J
       rw [e₂, Scheme.comp_val_base, TopCat.coe_comp, Set.range_comp, Set.range_iff_surjective.mpr,
         Set.image_univ, e₁.rightInverse_symm]
       · exact 𝒰.covers x
-      · rw [← TopCat.epi_iff_surjective]; infer_instance -- now `erw` after #13170
+      · rw [← TopCat.epi_iff_surjective]; infer_instance
     -- Porting note: weirdly, even though no input is needed, `inferInstance` does not work
     -- `PresheafedSpace.IsOpenImmersion.comp` is marked as `instance`
     IsOpen := fun i => by rw [e₂]; exact PresheafedSpace.IsOpenImmersion.comp _ _ }

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory.lean b/Mathlib/AlgebraicTopology/SimplexCategory.lean
@@ -802,7 +802,6 @@ theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ
     simp only [len_mk, Category.assoc, comp_toOrderHom, OrderHom.comp_coe, Function.comp_apply]
     by_cases h' : θ.toOrderHom x ≤ i
     · simp only [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk]
-      -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
       rw [Fin.predAbove_of_le_castSucc _ _ (by rwa [Fin.castSucc_castPred])]
       dsimp [δ]
       rw [Fin.succAbove_of_castSucc_lt i]

diff --git a/Mathlib/CategoryTheory/GradedObject/Unitor.lean b/Mathlib/CategoryTheory/GradedObject/Unitor.lean
@@ -124,8 +124,8 @@ lemma mapBifunctorLeftUnitor_inv_naturality :
   rw [mapBifunctorLeftUnitor_inv_apply, mapBifunctorLeftUnitor_inv_apply, assoc, assoc,
     ι_mapBifunctorMapMap]
   dsimp
-  rw [Functor.map_id, NatTrans.id_app, id_comp]
-  erw [← NatTrans.naturality_assoc, ← NatTrans.naturality_assoc]
+  rw [Functor.map_id, NatTrans.id_app, id_comp, ← NatTrans.naturality_assoc,
+    ← NatTrans.naturality_assoc]
   rfl
 
 @[reassoc]
@@ -242,7 +242,7 @@ lemma mapBifunctorRightUnitor_inv_naturality :
     ι_mapBifunctorMapMap]
   dsimp
   rw [Functor.map_id, id_comp, NatTrans.naturality_assoc]
-  erw [← NatTrans.naturality_assoc]
+  erw [← NatTrans.naturality_assoc e.inv]
   rfl
 
 @[reassoc]

diff --git a/Mathlib/CategoryTheory/Limits/Presheaf.lean b/Mathlib/CategoryTheory/Limits/Presheaf.lean
@@ -202,8 +202,7 @@ noncomputable def coconeOfRepresentable (P : Cᵒᵖ ⥤ Type v₁) :
     { app := fun x => yonedaEquiv.symm x.unop.2
       naturality := fun {x₁ x₂} f => by
         dsimp
-        rw [comp_id]
-        rw [← yonedaEquiv_symm_map]
+        rw [comp_id, ← yonedaEquiv_symm_map]
         congr 1
         rw [f.unop.2] }
 

diff --git a/Mathlib/CategoryTheory/Limits/VanKampen.lean b/Mathlib/CategoryTheory/Limits/VanKampen.lean
@@ -701,7 +701,7 @@ theorem isVanKampenColimit_extendCofan {n : ℕ} (f : Fin (n + 1) → C)
     rotate_left
     · ext ⟨j⟩
       dsimp
-      rw [colimit.ι_desc] -- Why?
+      rw [colimit.ι_desc]
       rfl
     simpa [Functor.const_obj_obj, Discrete.functor_obj, extendCofan_pt, extendCofan_ι_app,
       Fin.cases_succ, BinaryCofan.mk_pt, colimit.cocone_x, Cofan.mk_pt, Cofan.mk_ι_app,

diff --git a/Mathlib/CategoryTheory/Localization/SmallHom.lean b/Mathlib/CategoryTheory/Localization/SmallHom.lean
@@ -249,11 +249,7 @@ lemma equiv_smallHomMap (G : D₁ ⥤ D₂) (e : Φ.functor ⋙ L₂ ≅ L₁
   have hγ : ∀ (X : C₁), γ.hom.app (W₁.Q.obj X) =
       E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor.obj X) ≫
         e.hom.app X ≫ G.map (α₁.inv.app X) := fun X ↦ by
-    dsimp [γ]
-    rw [liftNatTrans_app]
-    dsimp
-    rw [id_comp, id_comp, comp_id]
-    rw [id_comp, comp_id]
+    simp [γ, id_comp, comp_id]
   simp only [Functor.map_comp, assoc]
   erw [← NatIso.naturality_1 γ]
   simp only [Functor.comp_map, ← cancel_epi (e.inv.app X), ← cancel_epi (G.map (α₁.hom.app X)),

diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean
@@ -1395,7 +1395,8 @@ theorem exp_bound_div_one_sub_of_interval' {x : ℝ} (h1 : 0 < x) (h2 : x < 1) :
       -- Porting note: was `norm_num [Finset.sum] <;> nlinarith`
       -- This proof should be restored after the norm_num plugin for big operators is ported.
       -- (It may also need the positivity extensions in #3907.)
-      repeat erw [Finset.sum_range_succ]
+      erw [Finset.sum_range_succ]
+      repeat rw [Finset.sum_range_succ]
       norm_num [Nat.factorial]
       nlinarith
     _ < 1 / (1 - x) := by rw [lt_div_iff₀] <;> nlinarith

diff --git a/Mathlib/Data/Multiset/Fintype.lean b/Mathlib/Data/Multiset/Fintype.lean
@@ -217,8 +217,7 @@ theorem Multiset.card_coe (m : Multiset α) : Fintype.card m = Multiset.card m :
 @[to_additive]
 theorem Multiset.prod_eq_prod_coe [CommMonoid α] (m : Multiset α) : m.prod = ∏ x : m, (x : α) := by
   congr
-  -- Porting note: `simp` fails with "maximum recursion depth has been reached"
-  rw [map_univ_coe]
+  simp
 
 @[to_additive]
 theorem Multiset.prod_eq_prod_toEnumFinset [CommMonoid α] (m : Multiset α) :

diff --git a/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean b/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean
@@ -40,10 +40,9 @@ theorem colimit_exists_rep (x : colimit (C := SheafedSpace C) F) :
     (isColimitOfPreserves (SheafedSpace.forget _) (colimit.isColimit F)) x
 
 instance {X Y : SheafedSpace C} (f g : X ⟶ Y) : Epi (coequalizer.π f g).base := by
-  rw [←
-    show _ = (coequalizer.π f g).base from
-      ι_comp_coequalizerComparison f g (SheafedSpace.forget C)]
-  rw [← PreservesCoequalizer.iso_hom]
+  rw [← show _ = (coequalizer.π f g).base from
+      ι_comp_coequalizerComparison f g (SheafedSpace.forget C),
+      ← PreservesCoequalizer.iso_hom]
   apply epi_comp
 
 end SheafedSpace

diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
@@ -369,29 +369,31 @@ def ιInvApp {i : D.J} (U : Opens (D.U i).carrier) :
                   ((D.f k j).c.app _ ≫ (D.t j k).c.app _) ≫ (D.V (j, k)).presheaf.map (eqToHom _)
             rw [opensImagePreimageMap_app_assoc]
             simp_rw [Category.assoc]
-            rw [opensImagePreimageMap_app_assoc, (D.t j k).c.naturality_assoc]
-            rw [snd_invApp_t_app_assoc]
-            rw [← PresheafedSpace.comp_c_app_assoc]
+            rw [opensImagePreimageMap_app_assoc, (D.t j k).c.naturality_assoc,
+                snd_invApp_t_app_assoc,
+                ← PresheafedSpace.comp_c_app_assoc]
             -- light-blue = green is relatively easy since the part that differs does not involve
             -- partial inverses.
             have :
               D.t' j k i ≫ (π₁ k, i, j) ≫ D.t k i ≫ 𝖣.f i k =
                 (pullbackSymmetry _ _).hom ≫ (π₁ j, i, k) ≫ D.t j i ≫ D.f i j := by
               rw [← 𝖣.t_fac_assoc, 𝖣.t'_comp_eq_pullbackSymmetry_assoc,
                 pullbackSymmetry_hom_comp_snd_assoc, pullback.condition, 𝖣.t_fac_assoc]
-            rw [congr_app this]
-            rw [PresheafedSpace.comp_c_app_assoc (pullbackSymmetry _ _).hom]
+            rw [congr_app this,
+                PresheafedSpace.comp_c_app_assoc (pullbackSymmetry _ _).hom]
             simp_rw [Category.assoc]
             congr 1
-            rw [← IsIso.eq_inv_comp]
-            rw [IsOpenImmersion.inv_invApp]
+            rw [← IsIso.eq_inv_comp,
+                IsOpenImmersion.inv_invApp]
             simp_rw [Category.assoc]
             erw [NatTrans.naturality_assoc, ← PresheafedSpace.comp_c_app_assoc,
               congr_app (pullbackSymmetry_hom_comp_snd _ _)]
             simp_rw [Category.assoc]
             erw [IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.inv_naturality_assoc,
               IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_invApp_assoc]
-            repeat' erw [← (D.V (j, k)).presheaf.map_comp]
+            rw [← (D.V (j, k)).presheaf.map_comp]
+            erw [← (D.V (j, k)).presheaf.map_comp]
+            repeat rw [← (D.V (j, k)).presheaf.map_comp]
             -- Porting note: was just `congr`
             exact congr_arg ((D.V (j, k)).presheaf.map ·) rfl } }
 

diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
@@ -326,9 +326,9 @@ theorem colimitPresheafObjIsoComponentwiseLimit_inv_ι_app (F : J ⥤ Presheafed
   rw [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app,
     congr_app (Iso.symm_inv _)]
   dsimp
-  rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality]
-  rw [← comp_c_app_assoc]
-  rw [congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc]
+  rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality,
+      ← comp_c_app_assoc,
+      congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc]
   erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc]
   -- Porting note: `convert` doesn't work due to meta variable, so change to a `suffices` block
   set f := _

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean b/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
@@ -225,8 +225,8 @@ theorem gradedMul_algebraMap (x : (⨁ i, 𝒜 i) ⊗[R] (⨁ i, ℬ i)) (r : R)
   ext
   dsimp
   erw [tmul_of_gradedMul_of_tmul]
-  rw [mul_zero, uzpow_zero, one_smul, smul_tmul']
-  rw [mul_one, _root_.Algebra.smul_def, Algebra.commutes]
+  rw [mul_zero, uzpow_zero, one_smul, smul_tmul',
+      mul_one, _root_.Algebra.smul_def, Algebra.commutes]
   rfl
 
 theorem gradedMul_one (x : (⨁ i, 𝒜 i) ⊗[R] (⨁ i, ℬ i)) :

diff --git a/Mathlib/RepresentationTheory/Character.lean b/Mathlib/RepresentationTheory/Character.lean
@@ -89,7 +89,7 @@ variable [Fintype G] [Invertible (Fintype.card G : k)]
 
 theorem average_char_eq_finrank_invariants (V : FDRep k G) :
     ⅟ (Fintype.card G : k) • ∑ g : G, V.character g = finrank k (invariants V.ρ) := by
-  rw [← (isProj_averageMap V.ρ).trace] -- Porting note: Changed `rw` to `erw`
+  rw [← (isProj_averageMap V.ρ).trace]
   simp [character, GroupAlgebra.average, _root_.map_sum]
 
 end Group

diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean b/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean
@@ -146,7 +146,6 @@ and the homogeneous `linearYonedaObjResolution`. -/
   -- https://github.com/leanprover-community/mathlib4/issues/5164
   change d n A f g = diagonalHomEquiv (n + 1) A
     ((resolution k G).d (n + 1) n ≫ (diagonalHomEquiv n A).symm f) g
-  -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
   rw [diagonalHomEquiv_apply, Action.comp_hom, ModuleCat.comp_def, LinearMap.comp_apply,
     resolution.d_eq]
   erw [resolution.d_of (Fin.partialProd g)]

diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
@@ -221,14 +221,11 @@ theorem diagonalSucc_inv_single_left (g : G) (f : Gⁿ →₀ k) (r : k) :
       diagonalSucc_inv_single_single, hx, Finsupp.sum_single_index, mul_comm b,
       zero_mul, single_zero] -/
   · rw [TensorProduct.tmul_zero, map_zero]
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
     rw [map_zero]
   · intro _ _ _ _ _ hx
-    rw [TensorProduct.tmul_add, map_add]; rw [map_add, hx]
+    rw [TensorProduct.tmul_add, map_add, map_add, hx]
     simp_rw [lift_apply, smul_single, smul_eq_mul]
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    rw [diagonalSucc_inv_single_single]
-    rw [sum_single_index, mul_comm]
+    rw [diagonalSucc_inv_single_single, sum_single_index, mul_comm]
     rw [zero_mul, single_zero]
 
 theorem diagonalSucc_inv_single_right (g : G →₀ k) (f : Gⁿ) (r : k) :
@@ -240,15 +237,11 @@ theorem diagonalSucc_inv_single_right (g : G →₀ k) (f : Gⁿ) (r : k) :
   · intro a b x ha hb hx
     simp only [lift_apply, smul_single', map_add, hx, diagonalSucc_inv_single_single,
       TensorProduct.add_tmul, Finsupp.sum_single_index, zero_mul, single_zero] -/
-  · rw [TensorProduct.zero_tmul, map_zero]
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    rw [map_zero]
+  · rw [TensorProduct.zero_tmul, map_zero, map_zero]
   · intro _ _ _ _ _ hx
-    rw [TensorProduct.add_tmul, map_add]; rw [map_add, hx]
+    rw [TensorProduct.add_tmul, map_add, map_add, hx]
     simp_rw [lift_apply, smul_single']
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    rw [diagonalSucc_inv_single_single]
-    rw [sum_single_index]
+    rw [diagonalSucc_inv_single_single, sum_single_index]
     rw [zero_mul, single_zero]
 
 end Rep
@@ -266,7 +259,6 @@ def ofMulActionBasisAux :
       (ofMulAction k G (Fin (n + 1) → G)).asModule :=
   { (Rep.equivalenceModuleMonoidAlgebra.1.mapIso (diagonalSucc k G n).symm).toLinearEquiv with
     map_smul' := fun r x => by
-      -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
       rw [RingHom.id_apply, LinearEquiv.toFun_eq_coe, ← LinearEquiv.map_smul]
       congr 1
       /- Porting note (#11039): broken proof was
@@ -357,21 +349,23 @@ theorem diagonalHomEquiv_symm_apply (f : (Fin n → G) → A) (x : Fin (n + 1)
     Category.comp_id, Action.comp_hom, MonoidalClosed.linearHomEquivComm_symm_hom]
   -- Porting note: This is a sure sign that coercions for morphisms in `ModuleCat`
   -- are still not set up properly.
-  -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
   rw [ModuleCat.coe_comp]
   simp only [ModuleCat.coe_comp, Function.comp_apply]
   -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
   erw [diagonalSucc_hom_single]
-  erw [TensorProduct.uncurry_apply, Finsupp.lift_apply, Finsupp.sum_single_index]
-  · simp only [one_smul]
-    erw [Representation.linHom_apply]
-    simp only [LinearMap.comp_apply, MonoidHom.one_apply, LinearMap.one_apply]
-    erw [Finsupp.llift_apply]
-    rw [Finsupp.lift_apply]
-    erw [Finsupp.sum_single_index]
-    · rw [one_smul]
+  -- The prototype linter that checks if `erw` could be replaced with `rw` would time out
+  -- if it replaces the next `erw`s with `rw`s. So we focus down on the relevant part.
+  conv_lhs =>
+    erw [TensorProduct.uncurry_apply, Finsupp.lift_apply, Finsupp.sum_single_index]
+    · simp only [one_smul]
+      erw [Representation.linHom_apply]
+      simp only [LinearMap.comp_apply, MonoidHom.one_apply, LinearMap.one_apply]
+      erw [Finsupp.llift_apply]
+      rw [Finsupp.lift_apply]
+      erw [Finsupp.sum_single_index]
+      · rw [one_smul]
+      · rw [zero_smul]
     · rw [zero_smul]
-  · rw [zero_smul]
 
 /-- Auxiliary lemma for defining group cohomology, used to show that the isomorphism
 `diagonalHomEquiv` commutes with the differentials in two complexes which compute

diff --git a/Mathlib/RingTheory/EisensteinCriterion.lean b/Mathlib/RingTheory/EisensteinCriterion.lean
@@ -34,8 +34,7 @@ theorem map_eq_C_mul_X_pow_of_forall_coeff_mem {f : R[X]} {P : Ideal R}
     by_cases hf0 : f = 0
     · simp [hf0]
     rcases lt_trichotomy (n : WithBot ℕ) (degree f) with (h | h | h)
-    · rw [coeff_map, eq_zero_iff_mem.2 (hfP n h), coeff_C_mul, coeff_X_pow, if_neg,
-        mul_zero]
+    · rw [coeff_map, eq_zero_iff_mem.2 (hfP n h), coeff_C_mul, coeff_X_pow, if_neg, mul_zero]
       rintro rfl
       exact not_lt_of_ge degree_le_natDegree h
     · have : natDegree f = n := natDegree_eq_of_degree_eq_some h.symm

diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean
@@ -229,13 +229,7 @@ instance (priority := 100) IsAdicComplete.henselianRing (R : Type*) [CommRing R]
         clear hmn
         induction' k with k ih
         · rw [add_zero]
-        rw [← add_assoc]
-        #adaptation_note /-- nightly-2024-03-11
-        I'm not sure why the `erw` is now needed here. It looks like it should work.
-        It looks like a diamond between `instHAdd` on `Nat` and `AddSemigroup.toAdd` which is
-        used by `instHAdd` -/
-        rw [hc]
-        rw [← add_zero (c m), sub_eq_add_neg]
+        rw [← add_assoc, hc, ← add_zero (c m), sub_eq_add_neg]
         refine ih.add ?_
         symm
         rw [SModEq.zero, Ideal.neg_mem_iff]

diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean
@@ -1070,17 +1070,17 @@ theorem subset_union_prime' {R : Type u} [CommRing R] {s : Finset ι} {f : ι
         rw [Finset.coe_insert] at h ⊢
         rw [Finset.coe_insert] at h
         simp only [Set.biUnion_insert] at h ⊢
-        rw [← Set.union_assoc (f i : Set R)] at h
-        rw [Set.union_eq_self_of_subset_right hfji] at h
+        rw [← Set.union_assoc (f i : Set R),
+            Set.union_eq_self_of_subset_right hfji] at h
         exact h
       specialize ih hp' hn' h'
       refine ih.imp id (Or.imp id (Exists.imp fun k => ?_))
       exact And.imp (fun hk => Finset.insert_subset_insert i (Finset.subset_insert j u) hk) id
     by_cases Ha : f a ≤ f i
     · have h' : (I : Set R) ⊆ f i ∪ f b ∪ ⋃ j ∈ (↑t : Set ι), f j := by
         rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_assoc,
-          Set.union_right_comm (f a : Set R)] at h
-        rw [Set.union_eq_self_of_subset_left Ha] at h
+          Set.union_right_comm (f a : Set R),
+          Set.union_eq_self_of_subset_left Ha] at h
         exact h
       specialize ih hp.2 hn h'
       right
@@ -1091,8 +1091,8 @@ theorem subset_union_prime' {R : Type u} [CommRing R] {s : Finset ι} {f : ι
     by_cases Hb : f b ≤ f i
     · have h' : (I : Set R) ⊆ f a ∪ f i ∪ ⋃ j ∈ (↑t : Set ι), f j := by
         rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_assoc,
-          Set.union_assoc (f a : Set R)] at h
-        rw [Set.union_eq_self_of_subset_left Hb] at h
+          Set.union_assoc (f a : Set R),
+          Set.union_eq_self_of_subset_left Hb] at h
         exact h
       specialize ih hp.2 hn h'
       rcases ih with (ih | ih | ⟨k, hkt, ih⟩)

diff --git a/Mathlib/RingTheory/PowerSeries/Basic.lean b/Mathlib/RingTheory/PowerSeries/Basic.lean
@@ -214,8 +214,9 @@ theorem coeff_zero_eq_constantCoeff_apply (φ : R⟦X⟧) : coeff R 0 φ = const
 
 @[simp]
 theorem monomial_zero_eq_C : ⇑(monomial R 0) = C R := by
-  -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-  erw [monomial, Finsupp.single_zero, MvPowerSeries.monomial_zero_eq_C]
+  -- This used to be `rw`, but we need `rw; rfl` after leanprover/lean4#2644
+  rw [monomial, Finsupp.single_zero, MvPowerSeries.monomial_zero_eq_C]
+  rfl
 
 theorem monomial_zero_eq_C_apply (a : R) : monomial R 0 a = C R a := by simp
 
@@ -251,7 +252,6 @@ theorem coeff_X (n : ℕ) : coeff R n (X : R⟦X⟧) = if n = 1 then 1 else 0 :=
 
 @[simp]
 theorem coeff_zero_X : coeff R 0 (X : R⟦X⟧) = 0 := by
-  -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
   rw [coeff, Finsupp.single_zero, X, MvPowerSeries.coeff_zero_X]
 
 @[simp]

diff --git a/Mathlib/RingTheory/PowerSeries/Inverse.lean b/Mathlib/RingTheory/PowerSeries/Inverse.lean
@@ -54,7 +54,6 @@ theorem coeff_inv_aux (n : ℕ) (a : R) (φ : R⟦X⟧) :
         -a *
           ∑ x ∈ antidiagonal n,
             if x.2 < n then coeff R x.1 φ * coeff R x.2 (inv.aux a φ) else 0 := by
-  -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
   rw [coeff, inv.aux, MvPowerSeries.coeff_inv_aux]
   simp only [Finsupp.single_eq_zero]
   split_ifs; · rfl

diff --git a/Mathlib/RingTheory/Valuation/Integral.lean b/Mathlib/RingTheory/Valuation/Integral.lean
@@ -38,7 +38,7 @@ theorem mem_of_integral {x : R} (hx : IsIntegral O x) : x ∈ v.integer :=
       one_mul (v x ^ p.natDegree)]
     cases' (hv.2 <| p.coeff i).lt_or_eq with hvpi hvpi
     · exact mul_lt_mul₀ hvpi (pow_lt_pow_right₀ hvx <| Finset.mem_range.1 hi)
-    · rw [hvpi]; rw [one_mul, one_mul]; exact pow_lt_pow_right₀ hvx (Finset.mem_range.1 hi)
+    · rw [hvpi, one_mul, one_mul]; exact pow_lt_pow_right₀ hvx (Finset.mem_range.1 hi)
 
 protected theorem integralClosure : integralClosure O R = ⊥ :=
   bot_unique fun _ hr =>