chore: classify rw to erw porting notes (#11225)

Classifies by adding issue number #11224 to porting notes claiming: 

> change `rw` to `erw`

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -104,7 +104,7 @@ theorem RespectsIso.ofRestrict_morphismRestrict_iff (hP : RingHom.RespectsIso @P
 theorem StableUnderBaseChange.Γ_pullback_fst (hP : StableUnderBaseChange @P) (hP' : RespectsIso @P)
     {X Y S : Scheme} [IsAffine X] [IsAffine Y] [IsAffine S] (f : X ⟶ S) (g : Y ⟶ S)
     (H : P (Scheme.Γ.map g.op)) : P (Scheme.Γ.map (pullback.fst : pullback f g ⟶ _).op) := by
-  -- Porting note: change `rw` to `erw`
+  -- Porting note (#11224): change `rw` to `erw`
   erw [← PreservesPullback.iso_inv_fst AffineScheme.forgetToScheme (AffineScheme.ofHom f)
       (AffineScheme.ofHom g)]
   rw [op_comp, Functor.map_comp, hP'.cancel_right_isIso, AffineScheme.forgetToScheme_map]

Mathlib/AlgebraicGeometry/Pullbacks.lean

@@ -272,7 +272,7 @@ def p1 : (gluing 𝒰 f g).glued ⟶ X := by
   exact fun i => pullback.fst ≫ 𝒰.map i
   rintro ⟨i, j⟩
   change pullback.fst ≫ _ ≫ 𝒰.map i = (_ ≫ _) ≫ _ ≫ 𝒰.map j
-  -- Porting note: change `rw` to `erw`
+  -- Porting note (#11224): change `rw` to `erw`
   erw [pullback.condition]
   rw [← Category.assoc]
   congr 1

Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

@@ -204,7 +204,7 @@ theorem imageBasicOpen_image_preimage :
     delta imageBasicOpen
     rw [preimage_basicOpen f, preimage_basicOpen g]
     dsimp only [Functor.op, unop_op]
-    -- Porting note: change `rw` to `erw`
+    -- Porting note (#11224): change `rw` to `erw`
     erw [← comp_apply, ← SheafedSpace.comp_c_app', ← comp_apply, ← SheafedSpace.comp_c_app',
       SheafedSpace.congr_app (coequalizer.condition f.1 g.1), comp_apply,
       X.toRingedSpace.basicOpen_res]
@@ -220,7 +220,7 @@ theorem imageBasicOpen_image_open :
   erw [← coe_comp]
   rw [PreservesCoequalizer.iso_hom, ι_comp_coequalizerComparison]
   dsimp only [SheafedSpace.forget]
-  -- Porting note: change `rw` to `erw`
+  -- Porting note (#11224): change `rw` to `erw`
   erw [imageBasicOpen_image_preimage]
   exact (imageBasicOpen f g U s).2
 #align algebraic_geometry.LocallyRingedSpace.has_coequalizer.image_basic_open_image_open AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open
@@ -249,7 +249,7 @@ instance coequalizer_π_stalk_isLocalRingHom (x : Y) :
   rw [← isUnit_map_iff ((coequalizer.π f.val g.val : _).c.app _), ← comp_apply,
     NatTrans.naturality, comp_apply, TopCat.Presheaf.pushforwardObj_map, ←
     isUnit_map_iff (Y.presheaf.map (eqToHom hV').op)]
-  -- Porting note: change `rw` to `erw`
+  -- Porting note (#11224): change `rw` to `erw`
   erw [← comp_apply, ← comp_apply, ← Y.presheaf.map_comp]
   convert @RingedSpace.isUnit_res_basicOpen Y.toRingedSpace (unop _)
       (((coequalizer.π f.val g.val).c.app (op U)) s)

Mathlib/Geometry/RingedSpace/OpenImmersion.lean

@@ -1173,7 +1173,7 @@ theorem lift_range (H' : Set.range g.1.base ⊆ Set.range f.1.base) :
       (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _) f g
   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: change `rw` to `erw` on this lemma
+  -- Porting note (#11224): change `rw` to `erw` on this lemma
   erw [TopCat.pullback_fst_range]
   ext
   constructor

Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

@@ -253,7 +253,7 @@ theorem ι_image_preimage_eq (i j : D.J) (U : Opens (D.U i).carrier) :
   dsimp only [Opens.map_coe, IsOpenMap.functor_obj_coe]
   rw [← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) i, ←
     show _ = (𝖣.ι j).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) j]
-  -- Porting note: change `rw` to `erw` on `coe_comp`
+  -- Porting note (#11224): change `rw` to `erw` on `coe_comp`
   erw [coe_comp, coe_comp, coe_comp]
   rw [Set.image_comp, Set.preimage_comp]
   erw [Set.preimage_image_eq]
@@ -474,7 +474,7 @@ theorem π_ιInvApp_π (i j : D.J) (U : Opens (D.U i).carrier) :
   rw [congr_app (D.t_id _), id_c_app]
   simp_rw [Category.assoc]
   rw [← Functor.map_comp_assoc]
-  -- Porting note: change `rw` to `erw`
+  -- Porting note (#11224): change `rw` to `erw`
   erw [IsOpenImmersion.inv_naturality_assoc]
   erw [IsOpenImmersion.app_invApp_assoc]
   iterate 3 rw [← Functor.map_comp_assoc]
@@ -538,7 +538,7 @@ def vPullbackConeIsLimit (i j : D.J) : IsLimit (𝖣.vPullbackCone i j) :=
         replace this := reassoc_of% this
         exact this _
       rw [← Set.image_subset_iff, ← Set.image_univ, ← Set.image_comp, Set.image_univ]
-      -- Porting note: change `rw` to `erw`
+      -- Porting note (#11224): change `rw` to `erw`
       erw [← coe_comp]
       rw [this, coe_comp, ← Set.image_univ, Set.image_comp]
       exact Set.image_subset_range _ _