From dd02f9754573feb004e99cea99d91594f726beea Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 9 Mar 2024 07:27:52 +0000 Subject: [PATCH] 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 | 2 +- Mathlib/AlgebraicGeometry/Pullbacks.lean | 2 +- .../RingedSpace/LocallyRingedSpace/HasColimits.lean | 6 +++--- Mathlib/Geometry/RingedSpace/OpenImmersion.lean | 2 +- Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean | 6 +++--- 5 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean index 187c4de6a78cfd..c977a2a0eeb3f0 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean +++ b/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] diff --git a/Mathlib/AlgebraicGeometry/Pullbacks.lean b/Mathlib/AlgebraicGeometry/Pullbacks.lean index f1e76bada9b980..520511426dd4ab 100644 --- a/Mathlib/AlgebraicGeometry/Pullbacks.lean +++ b/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 diff --git a/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean b/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean index ede8660d54ff61..aa89cc976d2e97 100644 --- a/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean +++ b/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) diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean index 2a3d31eb30690e..afc8e07989f466 100644 --- a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean +++ b/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 diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean index 9f61098ec637ae..ed5711963e82a2 100644 --- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean +++ b/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 _ _