From af3c28c713767e3f24b63a6158488240adef818d Mon Sep 17 00:00:00 2001 From: "Anne C.A. Baanen" Date: Fri, 11 Oct 2024 13:10:09 +0200 Subject: [PATCH] Fixes from the `erw` linter --- Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean | 2 +- Mathlib/CategoryTheory/Shift/Basic.lean | 2 +- Mathlib/Condensed/Discrete/Colimit.lean | 4 ++-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean | 4 ++-- Mathlib/Topology/Order/ScottTopology.lean | 4 ++-- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean b/Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean index cb15f1505053c..abcc9d116cda0 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean @@ -514,7 +514,7 @@ lemma mk_π {X : C} (π : F.obj zero ⟶ X) (h : F.map left ≫ π = F.map right (mk π h).π = π := rfl lemma condition (G : ReflexiveCofork F) : F.map left ≫ G.π = F.map right ≫ G.π := by - erw [Cocone.w G left, Cocone.w G right] + rw [Cocone.w G left, Cocone.w G right] @[simp] lemma app_one_eq_π (G : ReflexiveCofork F) : G.ι.app zero = G.π := rfl diff --git a/Mathlib/CategoryTheory/Shift/Basic.lean b/Mathlib/CategoryTheory/Shift/Basic.lean index 7acb86cbee29d..889c3bf069f82 100644 --- a/Mathlib/CategoryTheory/Shift/Basic.lean +++ b/Mathlib/CategoryTheory/Shift/Basic.lean @@ -519,7 +519,7 @@ lemma shiftFunctorCompIsoId_add'_inv_app : dsimp [shiftFunctorCompIsoId] simp only [Functor.map_comp, Category.assoc] congr 1 - erw [← NatTrans.naturality] + rw [← NatTrans.naturality] dsimp rw [← cancel_mono ((shiftFunctorAdd' C p' p 0 hp).inv.app X), Iso.hom_inv_id_app, Category.assoc, Category.assoc, Category.assoc, Category.assoc, diff --git a/Mathlib/Condensed/Discrete/Colimit.lean b/Mathlib/Condensed/Discrete/Colimit.lean index 75f3c6ee7dfeb..9e6930f3aa849 100644 --- a/Mathlib/Condensed/Discrete/Colimit.lean +++ b/Mathlib/Condensed/Discrete/Colimit.lean @@ -276,7 +276,7 @@ lemma isoLocallyConstantOfIsColimit_inv (X : Profinite.{u}ᵒᵖ ⥤ Type (u+1)) simp only [types_comp_apply, isoFinYoneda_inv_app, counitApp_app] apply presheaf_ext.{u, u+1} (X := X) (Y := X) (f := f) intro x - erw [incl_of_counitAppApp] + rw [incl_of_counitAppApp] simp only [counitAppAppImage, CompHausLike.coe_of] letI : Fintype (fiber.{u, u+1} f x) := Fintype.ofInjective (sigmaIncl.{u, u+1} f x).1 Subtype.val_injective @@ -551,7 +551,7 @@ lemma isoLocallyConstantOfIsColimit_inv (X : LightProfinite.{u}ᵒᵖ ⥤ Type u simp only [types_comp_apply, isoFinYoneda_inv_app, counitApp_app] apply presheaf_ext.{u, u} (X := X) (Y := X) (f := f) intro x - erw [incl_of_counitAppApp] + rw [incl_of_counitAppApp] simp only [counitAppAppImage, CompHausLike.coe_of] letI : Fintype (fiber.{u, u} f x) := Fintype.ofInjective (sigmaIncl.{u, u} f x).1 Subtype.val_injective diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean index 959214c257295..11dbae9b63d30 100644 --- a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean +++ b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean @@ -1120,8 +1120,8 @@ theorem lift_range (H' : Set.range g.base ⊆ Set.range f.base) : have : _ = (pullback.fst f g).base := PreservesPullback.iso_hom_fst (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _) f g - rw [LocallyRingedSpace.comp_base, ← this, ← Category.assoc, coe_comp] - rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ] + rw [LocallyRingedSpace.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 diff --git a/Mathlib/Topology/Order/ScottTopology.lean b/Mathlib/Topology/Order/ScottTopology.lean index 0a203e27ad789..2a58f0caeeb47 100644 --- a/Mathlib/Topology/Order/ScottTopology.lean +++ b/Mathlib/Topology/Order/ScottTopology.lean @@ -177,7 +177,7 @@ variable {α D} lemma isOpen_iff [IsScottHausdorff α D] : IsOpen s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a : α⦄, IsLUB d a → - a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s := by erw [topology_eq_scottHausdorff (α := α) (D := D)]; rfl + a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s := by rw [topology_eq_scottHausdorff (α := α) (D := D)]; rfl lemma dirSupInaccOn_of_isOpen [IsScottHausdorff α D] (h : IsOpen s) : DirSupInaccOn D s := fun d hd₀ hd₁ hd₂ a hda hd₃ ↦ by @@ -241,7 +241,7 @@ lemma topology_eq [IsScott α D] : ‹_› = scott α D := topology_eq_scott variable {α} {D} {s : Set α} {a : α} lemma isOpen_iff_isUpperSet_and_scottHausdorff_open [IsScott α D] : - IsOpen s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s := by erw [topology_eq α D]; rfl + IsOpen s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s := by rw [topology_eq α D]; rfl lemma isOpen_iff_isUpperSet_and_dirSupInaccOn [IsScott α D] : IsOpen s ↔ IsUpperSet s ∧ DirSupInaccOn D s := by