Replace *a lot* of erws with rw

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/AlgebraicGeometry/AffineScheme.lean

@@ -269,7 +269,7 @@ theorem range_fromSpec :
   delta IsAffineOpen.fromSpec; dsimp
   rw [Function.comp_assoc, 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]
@@ -313,7 +313,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
@@ -533,7 +533,7 @@ theorem fromSpec_primeIdealOf (x : U) :
   -- Porting note: in the porting note of `Scheme.comp_val_base`, it says that `elementwise` is
   -- unnecessary, indeed, the linter did not like it, so I just use `elementwise_of%` instead of
   -- adding the corresponding lemma in `Scheme.lean` file
-  erw [← elementwise_of% Scheme.comp_val_base] -- now `erw` after #13170
+  rw [← elementwise_of% Scheme.comp_val_base]
   simp only [Scheme.Opens.toScheme_presheaf_obj, Category.assoc, ← Spec.map_comp_assoc,
     ← Functor.map_comp, ← op_comp, eqToHom_trans, eqToHom_refl, op_id,
     CategoryTheory.Functor.map_id, Spec.map_id, Category.id_comp, Iso.hom_inv_id_assoc]

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

@@ -229,7 +229,7 @@ theorem ι_eq_iff (i j : D.J) (x : (D.U i).carrier) (y : (D.U j).carrier) :
       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
+  · rw [← comp_apply]
     simp_rw [← D.ι_isoCarrier_inv]
     rfl -- `rfl` was not needed before #13170
   · infer_instance
@@ -342,7 +342,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 +390,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/Geometry/RingedSpace/OpenImmersion.lean

@@ -1120,17 +1120,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 [LocallyRingedSpace.comp_val, SheafedSpace.comp_base, ← this, ← Category.assoc, coe_comp]
   rw [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))` -/
@@ -391,7 +389,9 @@ def ιInvApp {i : D.J} (U : Opens (D.U i).carrier) :
             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]
+            repeat' 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 } }
 
@@ -410,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/CompHaus/Projective.lean

@@ -51,8 +51,9 @@ instance projective_ultrafilter (X : Type*) : Projective (of <| Ultrafilter X) w
     -- The next two lines should not be needed.
     let g'' : ContinuousMap Y Z := g
     have : g'' ∘ g' = id := hg'.comp_eq_id
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [comp_assoc, ultrafilter_extend_extends, ← comp_assoc, this, id_comp]
+    -- This used to be `rw`, but we need `rw; rfl` after leanprover/lean4#2644
+    rw [comp_assoc, ultrafilter_extend_extends, ← comp_assoc, this, id_comp]
+    rfl
 
 /-- For any compact Hausdorff space `X`,
   the natural map `Ultrafilter X → X` is a projective presentation. -/

Mathlib/Topology/Category/Profinite/Projective.lean

@@ -50,8 +50,9 @@ instance projective_ultrafilter (X : Type u) : Projective (of <| Ultrafilter X)
      -- Porting note: same fix as in `Topology.Category.CompHaus.Projective`
     let g'' : ContinuousMap Y Z := g
     have : g'' ∘ g' = id := hg'.comp_eq_id
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [comp_assoc, ultrafilter_extend_extends, ← comp_assoc, this, id_comp]
+    -- This used to be `rw`, but we need `rw; rfl` after leanprover/lean4#2644
+    rw [comp_assoc, ultrafilter_extend_extends, ← comp_assoc, this, id_comp]
+    rfl
 
 /-- For any profinite `X`, the natural map `Ultrafilter X → X` is a projective presentation. -/
 def projectivePresentation (X : Profinite.{u}) : ProjectivePresentation X where

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] -- now `erw` after #13170
     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₂, -- now `erw` after #13170
       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⟩

Mathlib/Topology/Gluing.lean

@@ -121,8 +121,7 @@ def Rel (a b : Σ i, ((D.U i : TopCat) : Type _)) : Prop :=
 theorem rel_equiv : Equivalence D.Rel :=
   ⟨fun x => Or.inl (refl x), by
     rintro a b (⟨⟨⟩⟩ | ⟨x, e₁, e₂⟩)
-    exacts [Or.inl rfl, Or.inr ⟨D.t _ _ x, e₂, by erw [← e₁, D.t_inv_apply]⟩], by
-     -- previous line now `erw` after #13170
+    exacts [Or.inl rfl, Or.inr ⟨D.t _ _ x, e₂, by rw [← e₁, D.t_inv_apply]⟩], by
     rintro ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ (⟨⟨⟩⟩ | ⟨x, e₁, e₂⟩)
     · exact id
     rintro (⟨⟨⟩⟩ | ⟨y, e₃, e₄⟩)
@@ -237,17 +236,15 @@ theorem image_inter (i j : D.J) :
     · exact ⟨inv (D.f i i) x₁, by
         -- porting note (#10745): was `simp [eq₁]`
         -- See https://github.com/leanprover-community/mathlib4/issues/5026
-        rw [TopCat.comp_app]
-        erw [CategoryTheory.IsIso.inv_hom_id_apply]
-        rw [eq₁]⟩
+        rw [TopCat.comp_app, CategoryTheory.IsIso.inv_hom_id_apply, eq₁]⟩
     · -- Porting note: was
       -- dsimp only at *; substs e₁ eq₁; exact ⟨y, by simp⟩
       dsimp only at *
       substs eq₁
       exact ⟨y, by simp [e₁]⟩
   · rintro ⟨x, hx⟩
     refine ⟨⟨D.f i j x, hx⟩, ⟨D.f j i (D.t _ _ x), ?_⟩⟩
-    erw [D.glue_condition_apply] -- now `erw` after #13170
+    rw [D.glue_condition_apply]
     exact hx
 
 theorem preimage_range (i j : D.J) : 𝖣.ι j ⁻¹' Set.range (𝖣.ι i) = Set.range (D.f j i) := by
@@ -361,7 +358,7 @@ def mk' (h : MkCore.{u}) : TopCat.GlueData where
     exact (h.V_id i).symm ▸ (Opens.inclusionTopIso (h.U i)).isIso_hom
   f_open := fun i j : h.J => (h.V i j).openEmbedding
   t := h.t
-  t_id i := by ext; erw [h.t_id]; rfl  -- now `erw` after #13170
+  t_id i := by ext; rw [h.t_id]; rfl
   t' := h.t'
   t_fac i j k := by
     delta MkCore.t'
@@ -376,19 +373,12 @@ def mk' (h : MkCore.{u}) : TopCat.GlueData where
     simp only [Iso.inv_hom_id_assoc, Category.assoc, Category.id_comp]
     rw [← Iso.eq_inv_comp, Iso.inv_hom_id]
     ext1 ⟨⟨⟨x, hx⟩, ⟨x', hx'⟩⟩, rfl : x = x'⟩
-    -- The next 9 tactics (up to `convert ...` were a single `rw` before leanprover/lean4#2644
+    -- The next 3 tactics (up to `convert ...` were a single `rw` before leanprover/lean4#2644
     -- rw [comp_app, ContinuousMap.coe_mk, comp_app, id_app, ContinuousMap.coe_mk, Subtype.mk_eq_mk,
     --   Prod.mk.inj_iff, Subtype.mk_eq_mk, Subtype.ext_iff, and_self_iff]
-    erw [comp_app] --, comp_app, id_app] -- now `erw` after #13170
-    -- erw [ContinuousMap.coe_mk]
-    conv_lhs => erw [ContinuousMap.coe_mk]
-    erw [id_app]
-    rw [ContinuousMap.coe_mk]
+    rw [comp_app, ContinuousMap.coe_mk, id_app]
     erw [Subtype.mk_eq_mk]
-    rw [Prod.mk.inj_iff]
-    rw [Subtype.mk_eq_mk]
-    rw [Subtype.ext_iff]
-    rw [and_self_iff]
+    rw [Prod.mk.inj_iff, Subtype.mk_eq_mk, Subtype.ext_iff, and_self_iff]
     convert congr_arg Subtype.val (h.t_inv k i ⟨x, hx'⟩) using 3
     refine Subtype.ext ?_
     exact h.cocycle i j k ⟨x, hx⟩ hx'
@@ -435,9 +425,8 @@ theorem fromOpenSubsetsGlue_injective : Function.Injective (fromOpenSubsetsGlue
   intro x y e
   obtain ⟨i, ⟨x, hx⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x
   obtain ⟨j, ⟨y, hy⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective y
-  -- Porting note: now it is `erw`, it was `rw`
   -- see the porting note on `ι_fromOpenSubsetsGlue`
-  erw [ι_fromOpenSubsetsGlue_apply, ι_fromOpenSubsetsGlue_apply] at e
+  rw [ι_fromOpenSubsetsGlue_apply, ι_fromOpenSubsetsGlue_apply] at e
   change x = y at e
   subst e
   rw [(ofOpenSubsets U).ι_eq_iff_rel]
@@ -461,9 +450,7 @@ theorem fromOpenSubsetsGlue_isOpenMap : IsOpenMap (fromOpenSubsetsGlue U) := by
     apply congr_arg
     exact Set.preimage_image_eq _ (fromOpenSubsetsGlue_injective U)
   · refine ⟨Set.mem_image_of_mem _ hx, ?_⟩
-    -- Porting note: another `rw ↦ erw`
-    -- See above.
-    erw [ι_fromOpenSubsetsGlue_apply]
+    rw [ι_fromOpenSubsetsGlue_apply]
     exact Set.mem_range_self _
 
 theorem fromOpenSubsetsGlue_openEmbedding : OpenEmbedding (fromOpenSubsetsGlue U) :=
@@ -475,9 +462,7 @@ theorem range_fromOpenSubsetsGlue : Set.range (fromOpenSubsetsGlue U) = ⋃ i, (
   constructor
   · rintro ⟨x, rfl⟩
     obtain ⟨i, ⟨x, hx'⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x
-    -- Porting note: another `rw ↦ erw`
-    -- See above
-    erw [ι_fromOpenSubsetsGlue_apply]
+    rw [ι_fromOpenSubsetsGlue_apply]
     exact Set.subset_iUnion _ i hx'
   · rintro ⟨_, ⟨i, rfl⟩, hx⟩
     rename_i x