diff --git a/Archive/Sensitivity.lean b/Archive/Sensitivity.lean index 930668edaeaec..50f32a891fcdb 100644 --- a/Archive/Sensitivity.lean +++ b/Archive/Sensitivity.lean @@ -216,7 +216,6 @@ theorem duality (p q : Q n) : ε p (e q) = if p = q then 1 else 0 := by · rw [show p = q from Subsingleton.elim (α := Q 0) p q] dsimp [ε, e] simp - rfl · dsimp [ε, e] cases hp : p 0 <;> cases hq : q 0 all_goals diff --git a/Counterexamples/DirectSumIsInternal.lean b/Counterexamples/DirectSumIsInternal.lean index a980c74170e83..77546ffbf9615 100644 --- a/Counterexamples/DirectSumIsInternal.lean +++ b/Counterexamples/DirectSumIsInternal.lean @@ -88,8 +88,7 @@ theorem withSign.not_injective : -- porting note: `DFinsupp.singleAddHom_apply` doesn't work so we have to unfold dsimp [DirectSum.lof_eq_of, DirectSum.of, DFinsupp.singleAddHom] at h replace h := FunLike.congr_fun h 1 - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [DFinsupp.zero_apply, DFinsupp.add_apply, DFinsupp.single_eq_same, + rw [DFinsupp.zero_apply, DFinsupp.add_apply, DFinsupp.single_eq_same, DFinsupp.single_eq_of_ne UnitsInt.one_ne_neg_one.symm, add_zero, Subtype.ext_iff, Submodule.coe_zero] at h apply zero_ne_one h.symm diff --git a/Counterexamples/Pseudoelement.lean b/Counterexamples/Pseudoelement.lean index 1339b258ac76e..89d30969fc7f5 100644 --- a/Counterexamples/Pseudoelement.lean +++ b/Counterexamples/Pseudoelement.lean @@ -87,15 +87,13 @@ theorem x_not_pseudo_eq : ¬PseudoEqual _ x y := by Preadditive.comp_add] at ha let π₁ := (biprod.fst : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _) have ha₁ := congr_arg π₁ ha - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← CategoryTheory.comp_apply, ← CategoryTheory.comp_apply] at ha₁ + rw [← CategoryTheory.comp_apply, ← CategoryTheory.comp_apply] at ha₁ simp only [BinaryBiproduct.bicone_fst, biprod.lift_fst, CategoryTheory.id_apply, biprod.lift_fst_assoc, Category.id_comp, biprod.lift_snd_assoc, Linear.smul_comp, Preadditive.add_comp, BinaryBicone.inl_fst, BinaryBicone.inr_fst, smul_zero, add_zero] at ha₁ let π₂ := (biprod.snd : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _) have ha₂ := congr_arg π₂ ha - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← CategoryTheory.comp_apply, ← CategoryTheory.comp_apply] at ha₂ + rw [← CategoryTheory.comp_apply, ← CategoryTheory.comp_apply] at ha₂ simp only [BinaryBiproduct.bicone_snd, biprod.lift_snd, CategoryTheory.id_apply, biprod.lift_fst_assoc, Category.id_comp, biprod.lift_snd_assoc, Linear.smul_comp, Preadditive.add_comp, BinaryBicone.inl_snd, BinaryBicone.inr_snd, zero_add, two_smul] at ha₂ diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean index 9c657773c83d6..5cfadcf41987d 100644 --- a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean +++ b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean @@ -749,9 +749,6 @@ def subalgebraMap (e : A ≃ₐ[R] B) (S : Subalgebra R A) : S ≃ₐ[R] S.map e exact e.commutes _ } #align alg_equiv.subalgebra_map AlgEquiv.subalgebraMap --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] AlgEquiv.subalgebraMap_apply_coe AlgEquiv.subalgebraMap_symm_apply_coe - end AlgEquiv namespace Algebra diff --git a/Mathlib/Algebra/Category/AlgebraCat/Basic.lean b/Mathlib/Algebra/Category/AlgebraCat/Basic.lean index 9c910e9de3b6e..5d3915d429dcc 100644 --- a/Mathlib/Algebra/Category/AlgebraCat/Basic.lean +++ b/Mathlib/Algebra/Category/AlgebraCat/Basic.lean @@ -217,14 +217,12 @@ def toAlgEquiv {X Y : AlgebraCat R} (i : X ≅ Y) : X ≃ₐ[R] Y where -- porting note: was `by tidy` change (i.hom ≫ i.inv) x = x simp only [hom_inv_id] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [id_apply] + rw [id_apply] right_inv x := by -- porting note: was `by tidy` change (i.inv ≫ i.hom) x = x simp only [inv_hom_id] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [id_apply] + rw [id_apply] map_add' := i.hom.map_add -- Porting note: was `by tidy` map_mul' := i.hom.map_mul -- Porting note: was `by tidy` commutes' := i.hom.commutes -- Porting note: was `by tidy` diff --git a/Mathlib/Algebra/Category/AlgebraCat/Limits.lean b/Mathlib/Algebra/Category/AlgebraCat/Limits.lean index 3fce38163c59a..7a1c5c0cc541f 100644 --- a/Mathlib/Algebra/Category/AlgebraCat/Limits.lean +++ b/Mathlib/Algebra/Category/AlgebraCat/Limits.lean @@ -104,39 +104,17 @@ def limitConeIsLimit (F : J ⥤ AlgebraCatMax.{v, w} R) : IsLimit (limitCone.{v, · -- Porting note: we could add a custom `ext` lemma here. apply Subtype.ext ext j - simp only [Functor.comp_obj, Functor.mapCone_pt, Functor.mapCone_π_app, - forget_map_eq_coe] - -- This used to be as below but we need `erw` after leanprover/lean4#2644 - -- simp [forget_map_eq_coe, AlgHom.map_one, Functor.mapCone_π_app] - erw [map_one] + simp [forget_map_eq_coe, AlgHom.map_one, Functor.mapCone_π_app] rfl · intro x y apply Subtype.ext ext j - simp only [Functor.comp_obj, Functor.mapCone_pt, Functor.mapCone_π_app, - forget_map_eq_coe] - -- This used to be as below, but we need `erw` after leanprover/lean4#2644 - -- simp [forget_map_eq_coe, AlgHom.map_mul, Functor.mapCone_π_app] - erw [map_mul] + simp [forget_map_eq_coe, AlgHom.map_mul, Functor.mapCone_π_app] rfl - · simp only [Functor.comp_obj, Functor.mapCone_pt, Functor.mapCone_π_app, - forget_map_eq_coe] - -- The below `simp` was enough before leanprover/lean4#2644 - -- simp [forget_map_eq_coe, AlgHom.map_zero, Functor.mapCone_π_app] - apply Subtype.ext - dsimp - funext u - erw [map_zero] + · simp [forget_map_eq_coe, AlgHom.map_zero, Functor.mapCone_π_app] rfl · intro x y - simp only [Functor.comp_obj, Functor.mapCone_pt, Functor.mapCone_π_app, - forget_map_eq_coe] - -- The below `simp` was enough before leanprover/lean4#2644 - -- simp [forget_map_eq_coe, AlgHom.map_add, Functor.mapCone_π_app] - apply Subtype.ext - dsimp - funext u - erw [map_add] + simp [forget_map_eq_coe, AlgHom.map_add, Functor.mapCone_π_app] rfl · intro r apply Subtype.ext diff --git a/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean b/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean index bb93f02710d4a..04d378418981f 100644 --- a/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean +++ b/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean @@ -60,9 +60,7 @@ theorem free_obj_coe {α : Type u} : (free.obj α : Type u) = FreeAbelianGroup rfl #align AddCommGroup.free_obj_coe AddCommGroupCat.free_obj_coe --- This currently can't be a `simp` lemma, --- because `free_obj_coe` will simplify implicit arguments in the LHS. --- (The `simpNF` linter will, correctly, complain.) +@[simp] theorem free_map_coe {α β : Type u} {f : α → β} (x : FreeAbelianGroup α) : (free.map f) x = f <$> x := rfl @@ -104,11 +102,9 @@ def free : Type u ⥤ GroupCat where obj α := of (FreeGroup α) map := FreeGroup.map map_id := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - intros; ext1; erw [←FreeGroup.map.unique] <;> intros <;> rfl + intros; ext1; rw [←FreeGroup.map.unique]; intros; rfl map_comp := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - intros; ext1; erw [←FreeGroup.map.unique] <;> intros <;> rfl + intros; ext1; rw [←FreeGroup.map.unique]; intros; rfl #align Group.free GroupCat.free /-- The free-forgetful adjunction for groups. diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean index 1359ca22fac04..897a305426ab3 100644 --- a/Mathlib/Algebra/Category/GroupCat/Basic.lean +++ b/Mathlib/Algebra/Category/GroupCat/Basic.lean @@ -154,9 +154,6 @@ set_option linter.uppercaseLean3 false in set_option linter.uppercaseLean3 false in #align AddGroup.of_hom_apply AddGroupCat.ofHom_apply --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] AddGroupCat.ofHom_apply GroupCat.ofHom_apply - @[to_additive] instance ofUnique (G : Type*) [Group G] [i : Unique G] : Unique (GroupCat.of G) := i set_option linter.uppercaseLean3 false in diff --git a/Mathlib/Algebra/Category/GroupCat/Biproducts.lean b/Mathlib/Algebra/Category/GroupCat/Biproducts.lean index 71f3eee22a2ae..c4cd1d14149d6 100644 --- a/Mathlib/Algebra/Category/GroupCat/Biproducts.lean +++ b/Mathlib/Algebra/Category/GroupCat/Biproducts.lean @@ -76,9 +76,6 @@ noncomputable def biprodIsoProd (G H : AddCommGroupCat.{u}) : IsLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit G H) (binaryProductLimitCone G H).isLimit #align AddCommGroup.biprod_iso_prod AddCommGroupCat.biprodIsoProd --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] AddCommGroupCat.biprodIsoProd_hom_apply - @[simp, elementwise] theorem biprodIsoProd_inv_comp_fst (G H : AddCommGroupCat.{u}) : (biprodIsoProd G H).inv ≫ biprod.fst = AddMonoidHom.fst G H := @@ -141,9 +138,6 @@ noncomputable def biproductIsoPi (f : J → AddCommGroupCat.{u}) : IsLimit.conePointUniqueUpToIso (biproduct.isLimit f) (productLimitCone f).isLimit #align AddCommGroup.biproduct_iso_pi AddCommGroupCat.biproductIsoPi --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] AddCommGroupCat.biproductIsoPi_hom_apply - @[simp, elementwise] theorem biproductIsoPi_inv_comp_π (f : J → AddCommGroupCat.{u}) (j : J) : (biproductIsoPi f).inv ≫ biproduct.π f j = Pi.evalAddMonoidHom (fun j => f j) j := diff --git a/Mathlib/Algebra/Category/GroupCat/EquivalenceGroupAddGroup.lean b/Mathlib/Algebra/Category/GroupCat/EquivalenceGroupAddGroup.lean index 23eeb82106492..ba869f2f7f4d2 100644 --- a/Mathlib/Algebra/Category/GroupCat/EquivalenceGroupAddGroup.lean +++ b/Mathlib/Algebra/Category/GroupCat/EquivalenceGroupAddGroup.lean @@ -86,12 +86,6 @@ def groupAddGroupEquivalence : GroupCat ≌ AddGroupCat := (NatIso.ofComponents fun X => AddEquiv.toAddGroupCatIso (AddEquiv.additiveMultiplicative X)) #align Group_AddGroup_equivalence groupAddGroupEquivalence --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] groupAddGroupEquivalence_unitIso_hom_app_apply - groupAddGroupEquivalence_counitIso_inv_app_apply - groupAddGroupEquivalence_unitIso_inv_app_apply - groupAddGroupEquivalence_counitIso_hom_app_apply - /-- The equivalence of categories between `CommGroup` and `AddCommGroup`. -/ @[simps!] @@ -100,9 +94,3 @@ def commGroupAddCommGroupEquivalence : CommGroupCat ≌ AddCommGroupCat := (NatIso.ofComponents fun X => MulEquiv.toCommGroupCatIso (MulEquiv.multiplicativeAdditive X)) (NatIso.ofComponents fun X => AddEquiv.toAddCommGroupCatIso (AddEquiv.additiveMultiplicative X)) #align CommGroup_AddCommGroup_equivalence commGroupAddCommGroupEquivalence - --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] commGroupAddCommGroupEquivalence_counitIso_hom_app_apply - commGroupAddCommGroupEquivalence_unitIso_inv_app_apply - commGroupAddCommGroupEquivalence_unitIso_hom_app_apply - commGroupAddCommGroupEquivalence_counitIso_inv_app_apply diff --git a/Mathlib/Algebra/Category/GroupCat/Injective.lean b/Mathlib/Algebra/Category/GroupCat/Injective.lean index b85c442fe6a40..9699262a27f4d 100644 --- a/Mathlib/Algebra/Category/GroupCat/Injective.lean +++ b/Mathlib/Algebra/Category/GroupCat/Injective.lean @@ -133,8 +133,7 @@ variable {a} lemma eq_zero_of_toRatCircle_apply_self (h : toRatCircle ⟨a, Submodule.mem_span_singleton_self a⟩ = 0) : a = 0 := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [toRatCircle, LinearMap.comp_apply, LinearEquiv.coe_toLinearMap, + rw [toRatCircle, LinearMap.comp_apply, LinearEquiv.coe_toLinearMap, equivZModSpanAddOrderOf_apply_self, Submodule.liftQSpanSingleton_apply, LinearMap.toSpanSingleton_one, AddCircle.coe_eq_zero_iff] at h obtain ⟨n, hn⟩ := h diff --git a/Mathlib/Algebra/Category/GroupCat/Limits.lean b/Mathlib/Algebra/Category/GroupCat/Limits.lean index ca8dbab5f1708..ca0312bff1dd4 100644 --- a/Mathlib/Algebra/Category/GroupCat/Limits.lean +++ b/Mathlib/Algebra/Category/GroupCat/Limits.lean @@ -465,8 +465,4 @@ def kernelIsoKerOver {G H : AddCommGroupCat.{u}} (f : G ⟶ H) : set_option linter.uppercaseLean3 false in #align AddCommGroup.kernel_iso_ker_over AddCommGroupCat.kernelIsoKerOver --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] AddCommGroupCat.kernelIsoKerOver_inv_left_apply - AddCommGroupCat.kernelIsoKerOver_hom_left_apply_coe - end AddCommGroupCat diff --git a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean index eb84e96c61313..fdd94f25941f2 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean @@ -75,8 +75,7 @@ def ε : 𝟙_ (ModuleCat.{u} R) ⟶ (free R).obj (𝟙_ (Type u)) := Finsupp.lsingle PUnit.unit #align Module.free.ε ModuleCat.Free.ε --- This lemma has always been bad, but lean4#2644 made `simp` start noticing -@[simp, nolint simpNF] +@[simp] theorem ε_apply (r : R) : ε R r = Finsupp.single PUnit.unit r := rfl #align Module.free.ε_apply ModuleCat.Free.ε_apply @@ -104,10 +103,8 @@ theorem μ_natural {X Y X' Y' : Type u} (f : X ⟶ Y) (g : X' ⟶ Y') : (Finsupp.mapDomain f (Finsupp.single x 1) ⊗ₜ[R] Finsupp.mapDomain g (Finsupp.single x' 1)) _ = (Finsupp.mapDomain (f ⊗ g) (finsuppTensorFinsupp' R X X' (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single x' 1))) _ - - -- extra `rfl` after leanprover/lean4#2466 simp_rw [Finsupp.mapDomain_single, finsuppTensorFinsupp'_single_tmul_single, mul_one, - Finsupp.mapDomain_single, CategoryTheory.tensor_apply]; rfl + Finsupp.mapDomain_single, CategoryTheory.tensor_apply] #align Module.free.μ_natural ModuleCat.Free.μ_natural theorem left_unitality (X : Type u) : @@ -178,9 +175,8 @@ theorem associativity (X Y Z : Type u) : finsuppTensorFinsupp' R X (Y ⊗ Z) (Finsupp.single x 1 ⊗ₜ[R] finsuppTensorFinsupp' R Y Z (Finsupp.single y 1 ⊗ₜ[R] Finsupp.single z 1)) a - -- extra `rfl` after leanprover/lean4#2466 simp_rw [finsuppTensorFinsupp'_single_tmul_single, Finsupp.mapDomain_single, mul_one, - CategoryTheory.associator_hom_apply]; rfl + CategoryTheory.associator_hom_apply] #align Module.free.associativity ModuleCat.Free.associativity -- In fact, it's strong monoidal, but we don't yet have a typeclass for that. @@ -426,4 +422,5 @@ def liftUnique (F : C ⥤ D) (L : Free R C ⥤ D) [L.Additive] [L.Linear R] #align category_theory.Free.lift_unique CategoryTheory.Free.liftUnique end Free + end CategoryTheory diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index be29b07128506..140284c626e1f 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -445,8 +445,7 @@ instance : Module R (mkOfSMul' φ) where given by `R`. -/ abbrev mkOfSMul := ModuleCat.of R (mkOfSMul' φ) --- This lemma has always been bad, but lean4#2644 made `simp` start noticing -@[simp, nolint simpNF] +@[simp] lemma mkOfSMul_smul (r : R) : (mkOfSMul φ).smul r = φ r := rfl end diff --git a/Mathlib/Algebra/Category/ModuleCat/Biproducts.lean b/Mathlib/Algebra/Category/ModuleCat/Biproducts.lean index 75d0a330ccd8a..d9480fd6a8996 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Biproducts.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Biproducts.lean @@ -77,9 +77,6 @@ noncomputable def biprodIsoProd (M N : ModuleCat.{v} R) : IsLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit M N) (binaryProductLimitCone M N).isLimit #align Module.biprod_iso_prod ModuleCat.biprodIsoProd --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] ModuleCat.biprodIsoProd_hom_apply - @[simp, elementwise] theorem biprodIsoProd_inv_comp_fst (M N : ModuleCat.{v} R) : (biprodIsoProd M N).inv ≫ biprod.fst = LinearMap.fst R M N := @@ -141,9 +138,6 @@ noncomputable def biproductIsoPi [Fintype J] (f : J → ModuleCat.{v} R) : IsLimit.conePointUniqueUpToIso (biproduct.isLimit f) (productLimitCone f).isLimit #align Module.biproduct_iso_pi ModuleCat.biproductIsoPi --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] ModuleCat.biproductIsoPi_hom_apply - @[simp, elementwise] theorem biproductIsoPi_inv_comp_π [Fintype J] (f : J → ModuleCat.{v} R) (j : J) : (biproductIsoPi f).inv ≫ biproduct.π f j = (LinearMap.proj j : (∀ j, f j) →ₗ[R] f j) := diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean index 45a6494e386a8..cdf058df4b8ef 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean @@ -156,13 +156,11 @@ variable {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) identity functor. -/ def restrictScalarsId' : ModuleCat.restrictScalars.{v} f ≅ 𝟭 _ := by subst hf; rfl --- This lemma has always been bad, but lean4#2644 made `simp` start noticing -@[simp, nolint simpNF] +@[simp] lemma restrictScalarsId'_inv_apply (M : ModuleCat R) (x : M) : (restrictScalarsId' f hf).inv.app M x = x := by subst hf; rfl --- This lemma has always been bad, but lean4#2644 made `simp` start noticing -@[simp, nolint simpNF] +@[simp] lemma restrictScalarsId'_hom_apply (M : ModuleCat R) (x : M) : (restrictScalarsId' f hf).hom.app M x = x := by subst hf; rfl @@ -184,14 +182,11 @@ composition of the restriction of scalars functors. -/ def restrictScalarsComp' : ModuleCat.restrictScalars.{v} gf ≅ ModuleCat.restrictScalars g ⋙ ModuleCat.restrictScalars f := by subst hgf; rfl - --- This lemma has always been bad, but lean4#2644 made `simp` start noticing -@[simp, nolint simpNF] +@[simp] lemma restrictScalarsComp'_hom_apply (M : ModuleCat R₃) (x : M) : (restrictScalarsComp' f g gf hgf).hom.app M x = x := by subst hgf; rfl --- This lemma has always been bad, but lean4#2644 made `simp` start noticing -@[simp, nolint simpNF] +@[simp] lemma restrictScalarsComp'_inv_apply (M : ModuleCat R₃) (x : M) : (restrictScalarsComp' f g gf hgf).inv.app M x = x := by subst hgf; rfl @@ -748,10 +743,8 @@ def counit : restrictScalars.{max v u₂,u₁,u₂} f ⋙ extendScalars f ⟶ · rw [map_zero, map_zero] · dsimp rw [ModuleCat.coe_comp, ModuleCat.coe_comp,Function.comp,Function.comp, - ExtendScalars.map_tmul, restrictScalars.map_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [Counit.map_apply] - rw [lift.tmul, LinearMap.coe_mk, LinearMap.coe_mk] + ExtendScalars.map_tmul, restrictScalars.map_apply, Counit.map_apply, Counit.map_apply, + lift.tmul, lift.tmul, LinearMap.coe_mk, LinearMap.coe_mk] set s' : S := s' change s' • g y = g (s' • y) rw [map_smul] @@ -779,12 +772,8 @@ def extendRestrictScalarsAdj {R : Type u₁} {S : Type u₂} [CommRing R] [CommR letI m2 : Module R Y := Module.compHom Y f induction' x using TensorProduct.induction_on with s x _ _ _ _ · rw [map_zero, map_zero] - · rw [ExtendRestrictScalarsAdj.homEquiv_symm_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ModuleCat.coe_comp] - rw [Function.comp_apply, ExtendRestrictScalarsAdj.counit_app] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ExtendRestrictScalarsAdj.Counit.map_apply] + · rw [ExtendRestrictScalarsAdj.homEquiv_symm_apply, ModuleCat.coe_comp, Function.comp_apply, + ExtendRestrictScalarsAdj.counit_app, ExtendRestrictScalarsAdj.Counit.map_apply] dsimp rw [TensorProduct.lift.tmul] rfl diff --git a/Mathlib/Algebra/Category/ModuleCat/Colimits.lean b/Mathlib/Algebra/Category/ModuleCat/Colimits.lean index 3ca028fe8d29e..315f16ad418ee 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Colimits.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Colimits.lean @@ -61,8 +61,7 @@ noncomputable def colimitCocone : Cocone F where ι := { app := fun j => homMk (colimit.ι (F ⋙ forget₂ _ AddCommGroupCat) j) (fun r => by dsimp - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [mkOfSMul_smul] + rw [mkOfSMul_smul] simp) naturality := fun i j f => by apply (forget₂ _ AddCommGroupCat).map_injective @@ -78,8 +77,7 @@ noncomputable def isColimitColimitCocone : IsColimit (colimitCocone F) where intro j dsimp rw [colimit.ι_desc_assoc] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [mkOfSMul_smul] + rw [mkOfSMul_smul] dsimp simp only [ι_colimMap_assoc, Functor.comp_obj, forget₂_obj, colimit.ι_desc, Functor.mapCocone_pt, Functor.mapCocone_ι_app, forget₂_map] diff --git a/Mathlib/Algebra/Category/ModuleCat/Kernels.lean b/Mathlib/Algebra/Category/ModuleCat/Kernels.lean index 63cf2bb925072..6f55088b26bd6 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Kernels.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Kernels.lean @@ -39,9 +39,8 @@ def kernelIsLimit : IsLimit (kernelCone f) := -- Porting note: broken dot notation on LinearMap.ker LinearMap.codRestrict (LinearMap.ker f) (Fork.ι s) fun c => LinearMap.mem_ker.2 <| by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← @Function.comp_apply _ _ _ f (Fork.ι s) c, ← coe_comp] - rw [Fork.condition, HasZeroMorphisms.comp_zero (Fork.ι s) N] + rw [← @Function.comp_apply _ _ _ f (Fork.ι s) c, ← coe_comp, Fork.condition, + HasZeroMorphisms.comp_zero (Fork.ι s) N] rfl) (fun s => LinearMap.subtype_comp_codRestrict _ _ _) fun s m h => LinearMap.ext fun x => Subtype.ext_iff_val.2 (by simp [← h]; rfl) diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean index 2e493440e12ca..e6f92a6bde357 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean @@ -277,31 +277,23 @@ instance : MonoidalPreadditive (ModuleCat.{u} R) := by · dsimp only [autoParam]; intros refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] - rw [LinearMap.zero_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidalCategory.hom_apply] - rw [LinearMap.zero_apply, TensorProduct.tmul_zero] + rw [LinearMap.zero_apply, MonoidalCategory.hom_apply, LinearMap.zero_apply, + TensorProduct.tmul_zero] · dsimp only [autoParam]; intros refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] - rw [LinearMap.zero_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidalCategory.hom_apply] - rw [LinearMap.zero_apply, TensorProduct.zero_tmul] + rw [LinearMap.zero_apply, MonoidalCategory.hom_apply, LinearMap.zero_apply, + TensorProduct.zero_tmul] · dsimp only [autoParam]; intros refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] - rw [LinearMap.add_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply] + rw [LinearMap.add_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply] erw [MonoidalCategory.hom_apply] rw [LinearMap.add_apply, TensorProduct.tmul_add] · dsimp only [autoParam]; intros refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] - rw [LinearMap.add_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply] + rw [LinearMap.add_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply] erw [MonoidalCategory.hom_apply] rw [LinearMap.add_apply, TensorProduct.add_tmul] @@ -311,16 +303,12 @@ instance : MonoidalLinear R (ModuleCat.{u} R) := by · dsimp only [autoParam]; intros refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] - rw [LinearMap.smul_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply] - rw [LinearMap.smul_apply, TensorProduct.tmul_smul] + rw [LinearMap.smul_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply, + LinearMap.smul_apply, TensorProduct.tmul_smul] · dsimp only [autoParam]; intros refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] - rw [LinearMap.smul_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply] - rw [LinearMap.smul_apply, TensorProduct.smul_tmul, TensorProduct.tmul_smul] + rw [LinearMap.smul_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply, + LinearMap.smul_apply, TensorProduct.smul_tmul, TensorProduct.tmul_smul] end ModuleCat diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean index a39c08fe1dd57..2490b7793d4f9 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean @@ -34,11 +34,9 @@ def monoidalClosedHomEquiv (M N P : ModuleCat.{u} R) : left_inv f := by apply TensorProduct.ext' intro m n - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [coe_comp] - rw [Function.comp_apply] - -- This used to be `rw` and was longer (?), but we need `erw` after leanprover/lean4#2644 - erw [MonoidalCategory.braiding_hom_apply, TensorProduct.lift.tmul] + rw [coe_comp, Function.comp_apply, MonoidalCategory.braiding_hom_apply, + TensorProduct.lift.tmul, LinearMap.compr₂_apply, + TensorProduct.mk_apply, coe_comp, Function.comp_apply, MonoidalCategory.braiding_hom_apply] right_inv f := rfl set_option linter.uppercaseLean3 false in #align Module.monoidal_closed_hom_equiv ModuleCat.monoidalClosedHomEquiv @@ -66,8 +64,7 @@ open MonoidalCategory -- porting note: `CoeFun` was replaced by `FunLike` -- I can't seem to express the function coercion here without writing `@FunLike.coe`. --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -@[simp, nolint simpNF] +@[simp] theorem monoidalClosed_curry {M N P : ModuleCat.{u} R} (f : M ⊗ N ⟶ P) (x : M) (y : N) : @FunLike.coe _ _ _ LinearMap.instFunLike ((MonoidalClosed.curry f : N →ₗ[R] M →ₗ[R] P) y) x = f (x ⊗ₜ[R] y) := diff --git a/Mathlib/Algebra/Category/ModuleCat/Projective.lean b/Mathlib/Algebra/Category/ModuleCat/Projective.lean index b47176b046c7b..c421b16758cf7 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Projective.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Projective.lean @@ -69,9 +69,7 @@ instance moduleCat_enoughProjectives : EnoughProjectives (ModuleCat.{max u v} R) -- Porting note: simp [Finsupp.total_single] fails but rw succeeds dsimp [Basis.constr] simp only [Finsupp.lmapDomain_id, comp_id] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [Finsupp.total_single] - rw [one_smul] + rw [Finsupp.total_single, one_smul] rfl ⟩) }⟩ set_option linter.uppercaseLean3 false in #align Module.Module_enough_projectives ModuleCat.moduleCat_enoughProjectives diff --git a/Mathlib/Algebra/Category/MonCat/Basic.lean b/Mathlib/Algebra/Category/MonCat/Basic.lean index eaa9e83b2ac5e..824e73b6c424d 100644 --- a/Mathlib/Algebra/Category/MonCat/Basic.lean +++ b/Mathlib/Algebra/Category/MonCat/Basic.lean @@ -403,9 +403,7 @@ add_decl_doc addEquivIsoAddCommMonCatIso instance MonCat.forget_reflects_isos : ReflectsIsomorphisms (forget MonCat.{u}) where reflects {X Y} f _ := by let i := asIso ((forget MonCat).map f) - -- Again a problem that exists already creeps into other things leanprover/lean4#2644 - -- this used to be `by aesop`; see next declaration - let e : X ≃* Y := MulEquiv.mk i.toEquiv (MonoidHom.map_mul (show MonoidHom X Y from f)) + let e : X ≃* Y := MulEquiv.mk i.toEquiv (by aesop) exact IsIso.of_iso e.toMonCatIso set_option linter.uppercaseLean3 false in #align Mon.forget_reflects_isos MonCat.forget_reflects_isos diff --git a/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean b/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean index 1c864dd81b517..eafb4e83165a6 100644 --- a/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean +++ b/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean @@ -312,8 +312,7 @@ def colimitDesc (t : Cocone F) : colimit.{v, u} F ⟶ t.pt where rw [colimit_mul_mk_eq F ⟨i, x⟩ ⟨j, y⟩ (max' i j) (IsFiltered.leftToMax i j) (IsFiltered.rightToMax i j)] dsimp [Types.colimitCoconeIsColimit] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidHom.map_mul] + rw [MonoidHom.map_mul] -- Porting note : `rw` can't see through coercion is actually forgetful functor, -- so can't rewrite `t.w_apply` congr 1 <;> diff --git a/Mathlib/Algebra/Category/Ring/Colimits.lean b/Mathlib/Algebra/Category/Ring/Colimits.lean index f6ee8222759a2..465d879d0be9a 100644 --- a/Mathlib/Algebra/Category/Ring/Colimits.lean +++ b/Mathlib/Algebra/Category/Ring/Colimits.lean @@ -325,16 +325,11 @@ def colimitIsColimit : IsColimit (colimitCocone F) where induction x with | zero => erw [quot_zero, map_zero (f := m), (descMorphism F s).map_zero] | one => erw [quot_one, map_one (f := m), (descMorphism F s).map_one] - -- extra rfl with leanprover/lean4#2644 - | neg x ih => erw [quot_neg, map_neg (f := m), (descMorphism F s).map_neg, ih]; rfl + | neg x ih => erw [quot_neg, map_neg (f := m), (descMorphism F s).map_neg, ih] | of j x => exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x - | add x y ih_x ih_y => - -- extra rfl with leanprover/lean4#2644 - erw [quot_add, map_add (f := m), (descMorphism F s).map_add, ih_x, ih_y]; rfl - | mul x y ih_x ih_y => - -- extra rfl with leanprover/lean4#2644 - erw [quot_mul, map_mul (f := m), (descMorphism F s).map_mul, ih_x, ih_y]; rfl + | add x y ih_x ih_y => erw [quot_add, map_add (f := m), (descMorphism F s).map_add, ih_x, ih_y] + | mul x y ih_x ih_y => erw [quot_mul, map_mul (f := m), (descMorphism F s).map_mul, ih_x, ih_y] #align CommRing.colimits.colimit_is_colimit CommRingCat.Colimits.colimitIsColimit instance hasColimits_commRingCat : HasColimits CommRingCat where diff --git a/Mathlib/Algebra/Category/Ring/Constructions.lean b/Mathlib/Algebra/Category/Ring/Constructions.lean index ff60abacb7ec2..14d2b7e36d3ec 100644 --- a/Mathlib/Algebra/Category/Ring/Constructions.lean +++ b/Mathlib/Algebra/Category/Ring/Constructions.lean @@ -207,8 +207,7 @@ def prodFanIsLimit : IsLimit (prodFan A B) where have eq1 := congr_hom (h ⟨WalkingPair.left⟩) x have eq2 := congr_hom (h ⟨WalkingPair.right⟩) x dsimp at eq1 eq2 - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [←eq1, ←eq2] + rw [←eq1, ←eq2] rfl set_option linter.uppercaseLean3 false in #align CommRing.prod_fan_is_limit CommRingCat.prodFanIsLimit diff --git a/Mathlib/Algebra/DirectSum/Ring.lean b/Mathlib/Algebra/DirectSum/Ring.lean index 52ca29eb70186..b766bd3c65aaf 100644 --- a/Mathlib/Algebra/DirectSum/Ring.lean +++ b/Mathlib/Algebra/DirectSum/Ring.lean @@ -312,10 +312,8 @@ theorem mul_eq_dfinsupp_sum [∀ (i : ι) (x : A i), Decidable (x ≠ 0)] (a a' -- Porting note: I have no idea how the proof from ml3 worked it used to be -- simpa only [mul_hom, to_add_monoid, dfinsupp.lift_add_hom_apply, dfinsupp.sum_add_hom_apply, -- add_monoid_hom.dfinsupp_sum_apply, flip_apply, add_monoid_hom.dfinsupp_sum_add_hom_apply], - rw [mulHom, toAddMonoid, DFinsupp.liftAddHom_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [DFinsupp.sumAddHom_apply] - rw [AddMonoidHom.dfinsupp_sum_apply] + rw [mulHom,toAddMonoid,DFinsupp.liftAddHom_apply,DFinsupp.sumAddHom_apply, + AddMonoidHom.dfinsupp_sum_apply] apply congrArg _ funext x simp_rw [flip_apply] diff --git a/Mathlib/Algebra/Homology/ModuleCat.lean b/Mathlib/Algebra/Homology/ModuleCat.lean index ad46db4390a20..f5cda6cdb2867 100644 --- a/Mathlib/Algebra/Homology/ModuleCat.lean +++ b/Mathlib/Algebra/Homology/ModuleCat.lean @@ -72,12 +72,9 @@ set_option linter.uppercaseLean3 false in @[simp] theorem cyclesMap_toCycles (f : C ⟶ D) {i : ι} (x : LinearMap.ker (C.dFrom i)) : (cyclesMap f i) (toCycles x) = toCycles ⟨f.f i x.1, by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - rw [LinearMap.mem_ker]; erw [Hom.comm_from_apply, x.2, map_zero]⟩ := by + rw [LinearMap.mem_ker, Hom.comm_from_apply, x.2, map_zero]⟩ := by ext - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [cyclesMap_arrow_apply, toKernelSubobject_arrow, toKernelSubobject_arrow] - rfl + rw [cyclesMap_arrow_apply, toKernelSubobject_arrow, toKernelSubobject_arrow] set_option linter.uppercaseLean3 false in #align Module.cycles_map_to_cycles ModuleCat.cyclesMap_toCycles @@ -115,13 +112,9 @@ example (f g : C ⟶ D) (h : Homotopy f g) (i : ι) : erw [map_add, CategoryTheory.Limits.kernelSubobjectMap_arrow_apply, CategoryTheory.Limits.kernelSubobjectMap_arrow_apply, ModuleCat.toKernelSubobject_arrow, imageToKernel_arrow_apply, imageSubobject_arrow_comp_apply] - rw [Hom.sqFrom_left, Hom.sqFrom_left, h.comm i] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [LinearMap.add_apply] - rw [LinearMap.add_apply, prevD_eq_toPrev_dTo, dNext_eq_dFrom_fromNext] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [comp_apply, comp_apply, comp_apply] - erw [x.2, map_zero] + rw [Hom.sqFrom_left, Hom.sqFrom_left, h.comm i, LinearMap.add_apply, + LinearMap.add_apply, prevD_eq_toPrev_dTo, dNext_eq_dFrom_fromNext, comp_apply, comp_apply, + x.2, map_zero] dsimp abel diff --git a/Mathlib/Algebra/Lie/Classical.lean b/Mathlib/Algebra/Lie/Classical.lean index 1bd591a0aaf56..4770de024b1dc 100644 --- a/Mathlib/Algebra/Lie/Classical.lean +++ b/Mathlib/Algebra/Lie/Classical.lean @@ -224,9 +224,8 @@ def soIndefiniteEquiv {i : R} (hi : i * i = -1) : so' p q R ≃ₗ⁅R⁆ so (Su theorem soIndefiniteEquiv_apply {i : R} (hi : i * i = -1) (A : so' p q R) : (soIndefiniteEquiv p q R hi A : Matrix (Sum p q) (Sum p q) R) = (Pso p q R i)⁻¹ * (A : Matrix (Sum p q) (Sum p q) R) * Pso p q R i := by - rw [soIndefiniteEquiv, LieEquiv.trans_apply, LieEquiv.ofEq_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [skewAdjointMatricesLieSubalgebraEquiv_apply] + rw [soIndefiniteEquiv, LieEquiv.trans_apply, LieEquiv.ofEq_apply, + skewAdjointMatricesLieSubalgebraEquiv_apply] #align lie_algebra.orthogonal.so_indefinite_equiv_apply LieAlgebra.Orthogonal.soIndefiniteEquiv_apply /-- A matrix defining a canonical even-rank symmetric bilinear form. diff --git a/Mathlib/Algebra/Lie/DirectSum.lean b/Mathlib/Algebra/Lie/DirectSum.lean index 3f63b8b66dd76..bb2d7f15d5615 100644 --- a/Mathlib/Algebra/Lie/DirectSum.lean +++ b/Mathlib/Algebra/Lie/DirectSum.lean @@ -79,11 +79,7 @@ def lieModuleOf [DecidableEq ι] (j : ι) : M j →ₗ⁅R,L⁆ ⨁ i, M i := refine' DFinsupp.ext fun i => _ -- Porting note: Originally `ext i` by_cases h : j = i · rw [← h]; simp - · -- This used to be the end of the proof before leanprover/lean4#2644 - -- old proof `simp [lof, lsingle, h]` - simp only [lof, lsingle, AddHom.toFun_eq_coe, lie_module_bracket_apply] - erw [AddHom.coe_mk] - simp [h] } + · simp [lof, lsingle, h] } #align direct_sum.lie_module_of DirectSum.lieModuleOf /-- The projection map onto one component, as a morphism of Lie modules. -/ @@ -143,21 +139,8 @@ def lieAlgebraOf [DecidableEq ι] (j : ι) : L j →ₗ⁅R⁆ ⨁ i, L i := map_lie' := fun {x y} => by refine' DFinsupp.ext fun i => _ -- Porting note: Originally `ext i` by_cases h : j = i - · rw [← h] - -- This used to be the end of the proof before leanprover/lean4#2644 - -- with `simp [of, singleAddHom]` - simp only [of, singleAddHom, bracket_apply] - erw [AddHom.coe_mk, single_apply, single_apply] - simp [h] - intros - erw [single_add] - · -- This used to be the end of the proof before leanprover/lean4#2644 - -- with `simp [of, singleAddHom]` - simp only [of, singleAddHom, bracket_apply] - erw [AddHom.coe_mk, single_apply, single_apply] - simp only [h, dite_false, single_apply, lie_self] - intros - erw [single_add] } + · rw [← h]; simp [of, singleAddHom] + · simp [of, singleAddHom, h] } #align direct_sum.lie_algebra_of DirectSum.lieAlgebraOf /-- The projection map onto one component, as a morphism of Lie algebras. -/ @@ -180,11 +163,6 @@ theorem lie_of_of_ne [DecidableEq ι] {i j : ι} (hij : j ≠ i) (x : L i) (y : rw [LieHom.map_lie] simp only [of, singleAddHom, AddMonoidHom.coe_mk, ZeroHom.coe_mk, lieAlgebraComponent_apply, component, lapply, LinearMap.coe_mk, AddHom.coe_mk, single_apply, LieHom.map_zero] - -- The next four lines were not needed before leanprover/lean4#2644 - erw [AddMonoidHom.coe_mk, AddHom.coe_mk, ZeroHom.coe_mk] - rotate_left - intros; erw [single_add] - erw [single_apply, single_apply] by_cases hik : i = k · simp only [dif_neg, not_false_iff, lie_zero, hik.symm, hij] · simp only [dif_neg, not_false_iff, zero_lie, hik] diff --git a/Mathlib/Algebra/Lie/Submodule.lean b/Mathlib/Algebra/Lie/Submodule.lean index 2f836528f6afd..7e53178bec354 100644 --- a/Mathlib/Algebra/Lie/Submodule.lean +++ b/Mathlib/Algebra/Lie/Submodule.lean @@ -1442,8 +1442,7 @@ def LieIdeal.topEquiv : (⊤ : LieIdeal R L) ≃ₗ⁅R⁆ L := LieSubalgebra.topEquiv #align lie_ideal.top_equiv LieIdeal.topEquiv --- This lemma has always been bad, but leanprover/lean4#2644 made `simp` start noticing -@[simp, nolint simpNF] +@[simp] theorem LieIdeal.topEquiv_apply (x : (⊤ : LieIdeal R L)) : LieIdeal.topEquiv x = x := rfl #align lie_ideal.top_equiv_apply LieIdeal.topEquiv_apply @@ -1456,8 +1455,7 @@ def LieModuleEquiv.ofTop : (⊤ : LieSubmodule R L M) ≃ₗ⁅R,L⁆ M := { LinearEquiv.ofTop ⊤ rfl with map_lie' := rfl } --- This lemma has always been bad, but leanprover/lean4#2644 made `simp` start noticing -@[simp, nolint simpNF] lemma LieModuleEquiv.ofTop_apply (x : (⊤ : LieSubmodule R L M)) : +@[simp] lemma LieModuleEquiv.ofTop_apply (x : (⊤ : LieSubmodule R L M)) : LieModuleEquiv.ofTop R L M x = x := rfl diff --git a/Mathlib/Algebra/Lie/UniversalEnveloping.lean b/Mathlib/Algebra/Lie/UniversalEnveloping.lean index 4c994d20a82ad..55c0d8f59acc3 100644 --- a/Mathlib/Algebra/Lie/UniversalEnveloping.lean +++ b/Mathlib/Algebra/Lie/UniversalEnveloping.lean @@ -119,8 +119,7 @@ def lift : (L →ₗ⁅R⁆ A) ≃ (UniversalEnvelopingAlgebra R L →ₐ[R] A) -- RingQuot.liftAlgHom_mkAlgHom_apply] simp only [LieHom.coe_comp, Function.comp_apply, AlgHom.coe_toLieHom, UniversalEnvelopingAlgebra.ι_apply, mkAlgHom] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [RingQuot.liftAlgHom_mkAlgHom_apply] + rw [RingQuot.liftAlgHom_mkAlgHom_apply] simp only [TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap] right_inv F := by apply RingQuot.ringQuot_ext' @@ -130,8 +129,7 @@ def lift : (L →ₗ⁅R⁆ A) ≃ (UniversalEnvelopingAlgebra R L →ₐ[R] A) -- LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_linearMap_comp, -- AlgHom.comp_toLinearMap, Function.comp_apply, AlgHom.toLinearMap_apply, -- RingQuot.liftAlgHom_mkAlgHom_apply, AlgHom.coe_toLieHom, LieHom.coe_mk] - -- extra `rfl` after leanprover/lean4#2644 - simp [mkAlgHom]; rfl + simp [mkAlgHom] #align universal_enveloping_algebra.lift UniversalEnvelopingAlgebra.lift @[simp] diff --git a/Mathlib/Algebra/MonoidAlgebra/Basic.lean b/Mathlib/Algebra/MonoidAlgebra/Basic.lean index 04a4c0c4882a6..412bc9724e3ae 100644 --- a/Mathlib/Algebra/MonoidAlgebra/Basic.lean +++ b/Mathlib/Algebra/MonoidAlgebra/Basic.lean @@ -605,8 +605,7 @@ theorem liftNC_smul [MulOneClass G] {R : Type*} [Semiring R] (f : k →+* R) (g unfold MonoidAlgebra simp only [AddMonoidHom.coe_comp, Function.comp_apply, singleAddHom_apply, smulAddHom_apply, smul_single, smul_eq_mul, AddMonoidHom.coe_mulLeft] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [liftNC_single, liftNC_single]; rw [AddMonoidHom.coe_coe, map_mul, mul_assoc] + rw [liftNC_single, liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc] #align monoid_algebra.lift_nc_smul MonoidAlgebra.liftNC_smul end MiscTheorems @@ -765,9 +764,8 @@ theorem ringHom_ext {R} [Semiring k] [MulOneClass G] [Semiring R] {f g : MonoidA f = g := RingHom.coe_addMonoidHom_injective <| addHom_ext fun a b => by - rw [← single, ← one_mul a, ← mul_one b, ← single_mul_single] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [AddMonoidHom.coe_coe f, AddMonoidHom.coe_coe g]; rw [f.map_mul, g.map_mul, h₁, h_of] + rw [← single, ← one_mul a, ← mul_one b, ← single_mul_single, AddMonoidHom.coe_coe f, + AddMonoidHom.coe_coe g, f.map_mul, g.map_mul, h₁, h_of] #align monoid_algebra.ring_hom_ext MonoidAlgebra.ringHom_ext /-- If two ring homomorphisms from `MonoidAlgebra k G` are equal on all `single a 1` @@ -1115,9 +1113,8 @@ protected noncomputable def opRingEquiv [Monoid G] : { opAddEquiv.symm.trans <| (Finsupp.mapRange.addEquiv (opAddEquiv : k ≃+ kᵐᵒᵖ)).trans <| Finsupp.domCongr opEquiv with map_mul' := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - rw [Equiv.toFun_as_coe, AddEquiv.toEquiv_eq_coe]; erw [AddEquiv.coe_toEquiv] - rw [← AddEquiv.coe_toAddMonoidHom] + rw [Equiv.toFun_as_coe, AddEquiv.toEquiv_eq_coe, AddEquiv.coe_toEquiv, + ← AddEquiv.coe_toAddMonoidHom] refine Iff.mpr (AddMonoidHom.map_mul_iff (R := (MonoidAlgebra k G)ᵐᵒᵖ) (S := MonoidAlgebra kᵐᵒᵖ Gᵐᵒᵖ) _) ?_ -- Porting note: Was `ext`. @@ -1127,12 +1124,9 @@ protected noncomputable def opRingEquiv [Monoid G] : simp only [AddMonoidHom.coe_comp, AddEquiv.coe_toAddMonoidHom, opAddEquiv_apply, Function.comp_apply, singleAddHom_apply, AddMonoidHom.compr₂_apply, AddMonoidHom.coe_mul, AddMonoidHom.coe_mulLeft, AddMonoidHom.compl₂_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply, - AddEquiv.trans_apply, AddEquiv.trans_apply, MulOpposite.opAddEquiv_symm_apply] - rw [MulOpposite.unop_mul (α := MonoidAlgebra k G)] - -- This was not needed before leanprover/lean4#2644 - erw [unop_op, unop_op, single_mul_single] + rw [AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply, + AddEquiv.trans_apply, AddEquiv.trans_apply, + MulOpposite.opAddEquiv_symm_apply, MulOpposite.unop_mul (α := MonoidAlgebra k G)] simp } #align monoid_algebra.op_ring_equiv MonoidAlgebra.opRingEquiv #align monoid_algebra.op_ring_equiv_apply MonoidAlgebra.opRingEquiv_apply @@ -1871,21 +1865,17 @@ protected noncomputable def opRingEquiv [AddCommMonoid G] : { MulOpposite.opAddEquiv.symm.trans (Finsupp.mapRange.addEquiv (MulOpposite.opAddEquiv : k ≃+ kᵐᵒᵖ)) with map_mul' := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - rw [Equiv.toFun_as_coe, AddEquiv.toEquiv_eq_coe]; erw [AddEquiv.coe_toEquiv] - rw [← AddEquiv.coe_toAddMonoidHom] + rw [Equiv.toFun_as_coe, AddEquiv.toEquiv_eq_coe, AddEquiv.coe_toEquiv, + ← AddEquiv.coe_toAddMonoidHom] refine Iff.mpr (AddMonoidHom.map_mul_iff (R := k[G]ᵐᵒᵖ) (S := kᵐᵒᵖ[G]) _) ?_ -- Porting note: Was `ext`. refine AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₁ => AddMonoidHom.ext fun r₁ => AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₂ => AddMonoidHom.ext fun r₂ => ?_ -- Porting note: `reducible` cannot be `local` so proof gets long. dsimp - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply, - MulOpposite.opAddEquiv_symm_apply]; rw [MulOpposite.unop_mul (α := k[G])] + rw [AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply, + MulOpposite.opAddEquiv_symm_apply, MulOpposite.unop_mul (α := k[G])] dsimp - -- This was not needed before leanprover/lean4#2644 - erw [mapRange_single, single_mul_single, mapRange_single, mapRange_single] simp only [mapRange_single, single_mul_single, ← op_mul, add_comm] } #align add_monoid_algebra.op_ring_equiv AddMonoidAlgebra.opRingEquiv #align add_monoid_algebra.op_ring_equiv_apply AddMonoidAlgebra.opRingEquiv_apply diff --git a/Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean b/Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean index 36e0dfb5fb94e..ed79080b7ea24 100644 --- a/Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean +++ b/Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean @@ -144,13 +144,7 @@ theorem toDirectSum_mul [DecidableEq ι] [AddMonoid ι] [Semiring M] (f g : AddM refine Finsupp.addHom_ext' fun yi => AddMonoidHom.ext fun yv => ?_ dsimp only [AddMonoidHom.comp_apply, AddMonoidHom.compl₂_apply, AddMonoidHom.compr₂_apply, AddMonoidHom.mul_apply, Finsupp.singleAddHom_apply] - -- This was not needed before leanprover/lean4#2644 - erw [AddMonoidHom.compl₂_apply] - -- 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, AddMonoidAlgebra.toDirectSum_single] simp only [AddMonoidHom.coe_comp, AddMonoidHom.coe_mul, AddMonoidHom.coe_mk, ZeroHom.coe_mk, diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean index 70b6a3ea4db66..68c6feb989d70 100644 --- a/Mathlib/AlgebraicGeometry/AffineScheme.lean +++ b/Mathlib/AlgebraicGeometry/AffineScheme.lean @@ -268,10 +268,7 @@ theorem isAffineOpen_iff_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : Is fun hU => hU.imageIsOpenImmersion f⟩ · rw [Scheme.comp_val_base, coe_comp, Set.range_comp] dsimp [Opens.inclusion] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ContinuousMap.coe_mk, ContinuousMap.coe_mk] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - rw [Subtype.range_coe]; erw [Subtype.range_coe] + rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Subtype.range_coe, Subtype.range_coe] rfl · infer_instance #align algebraic_geometry.is_affine_open_iff_of_is_open_immersion AlgebraicGeometry.isAffineOpen_iff_of_isOpenImmersion diff --git a/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean b/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean index 3d51aad14857d..047b795306e1d 100644 --- a/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean +++ b/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean @@ -101,9 +101,6 @@ def toΓSpecBase : X.toTopCat ⟶ Spec.topObj (Γ.obj (op X)) where continuous_toFun := X.toΓSpec_continuous #align algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_base AlgebraicGeometry.LocallyRingedSpace.toΓSpecBase --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] AlgebraicGeometry.LocallyRingedSpace.toΓSpecBase_apply - variable (r : Γ.obj (op X)) /-- The preimage in `X` of a basic open in `Spec Γ(X)` (as an open set). -/ @@ -302,17 +299,9 @@ def identityToΓSpec : 𝟭 LocallyRingedSpace.{u} ⟶ Γ.rightOp ⋙ Spec.toLoc --Porting Note: Had to add the next four lines rw [comp_apply, comp_apply] dsimp [toΓSpecBase] - -- The next six lines were `rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk]` before - -- leanprover/lean4#2644 - have : (ContinuousMap.mk (toΓSpecFun Y) (toΓSpec_continuous _)) (f.val.base x) - = toΓSpecFun Y (f.val.base x) := by erw [ContinuousMap.coe_mk]; rfl - erw [this] - have : (ContinuousMap.mk (toΓSpecFun X) (toΓSpec_continuous _)) x - = toΓSpecFun X x := by erw [ContinuousMap.coe_mk] - erw [this] + rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk] dsimp [toΓSpecFun] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← LocalRing.comap_closedPoint (PresheafedSpace.stalkMap f.val x), ← + rw [← LocalRing.comap_closedPoint (PresheafedSpace.stalkMap f.val x), ← PrimeSpectrum.comap_comp_apply, ← PrimeSpectrum.comap_comp_apply] congr 2 exact (PresheafedSpace.stalkMap_germ f.1 ⊤ ⟨x, trivial⟩).symm diff --git a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean index 1bf7e5c231b67..4d13c2e421247 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean @@ -102,8 +102,7 @@ theorem RespectsIso.ofRestrict_morphismRestrict_iff (hP : RingHom.RespectsIso @P rw [← SetLike.coe_subset_coe, Functor.op_obj] dsimp [Opens.inclusion] simp only [Set.image_univ, Set.image_subset_iff, Subtype.range_val] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ContinuousMap.coe_mk, Subtype.range_val, ContinuousMap.coe_mk, ContinuousMap.coe_mk, + rw [ContinuousMap.coe_mk, Subtype.range_val, ContinuousMap.coe_mk, ContinuousMap.coe_mk, Subtype.range_val] rfl have i1 := AlgebraicGeometry.Γ_restrict_isLocalization Y r diff --git a/Mathlib/AlgebraicGeometry/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/OpenImmersion.lean index 9cd63bc1cec9e..f1f04750d7650 100644 --- a/Mathlib/AlgebraicGeometry/OpenImmersion.lean +++ b/Mathlib/AlgebraicGeometry/OpenImmersion.lean @@ -722,9 +722,7 @@ def Scheme.restrictFunctor : Opens X ⥤ Over X where Over.homMk (IsOpenImmersion.lift (X.ofRestrict _) (X.ofRestrict _) <| by dsimp [ofRestrict, LocallyRingedSpace.ofRestrict, Opens.inclusion] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ContinuousMap.coe_mk, ContinuousMap.coe_mk] - rw [Subtype.range_val, Subtype.range_val] + rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Subtype.range_val, Subtype.range_val] exact i.le) (IsOpenImmersion.lift_fac _ _ _) map_id U := by @@ -749,8 +747,7 @@ def Scheme.restrictFunctor : Opens X ⥤ Over X where ((X.restrictFunctor.map i).left) = IsOpenImmersion.lift (X.ofRestrict V.openEmbedding) (X.ofRestrict U.openEmbedding) (by dsimp [ofRestrict, LocallyRingedSpace.ofRestrict, Opens.inclusion] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ContinuousMap.coe_mk, ContinuousMap.coe_mk]; rw [Subtype.range_val, Subtype.range_val] + rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Subtype.range_val, Subtype.range_val] exact i.le) := rfl -- Porting note : the `by ...` used to be automatically done by unification magic @@ -759,8 +756,7 @@ theorem Scheme.restrictFunctor_map_ofRestrict {U V : Opens X} (i : U ⟶ V) : (X.restrictFunctor.map i).1 ≫ X.ofRestrict _ = X.ofRestrict _ := IsOpenImmersion.lift_fac _ _ (by dsimp [ofRestrict, LocallyRingedSpace.ofRestrict, Opens.inclusion] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ContinuousMap.coe_mk, ContinuousMap.coe_mk]; rw [Subtype.range_val, Subtype.range_val] + rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Subtype.range_val, Subtype.range_val] exact i.le) #align algebraic_geometry.Scheme.restrict_functor_map_ofRestrict AlgebraicGeometry.Scheme.restrictFunctor_map_ofRestrict @@ -822,11 +818,9 @@ noncomputable abbrev Scheme.restrictMapIso {X Y : Scheme} (f : X ⟶ Y) [IsIso f (H := PresheafedSpace.IsOpenImmersion.comp (hf := inferInstance) (hg := inferInstance)) (Y.ofRestrict _) _ dsimp [Opens.inclusion] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - rw [coe_comp, Set.range_comp]; erw [ContinuousMap.coe_mk, ContinuousMap.coe_mk] + rw [coe_comp, Set.range_comp, ContinuousMap.coe_mk, ContinuousMap.coe_mk] dsimp - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - rw [Subtype.range_val]; erw [Subtype.range_coe] + rw [Subtype.range_val, Subtype.range_coe] refine' @Set.image_preimage_eq _ _ f.1.base U.1 _ rw [← TopCat.epi_iff_surjective] infer_instance @@ -922,8 +916,7 @@ def pullbackRestrictIsoRestrict {X Y : Scheme} (f : X ⟶ Y) (U : Opens Y) : refine' IsOpenImmersion.isoOfRangeEq pullback.fst (X.ofRestrict _) _ rw [IsOpenImmersion.range_pullback_fst_of_right] dsimp [Opens.inclusion] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ContinuousMap.coe_mk, ContinuousMap.coe_mk]; rw [Subtype.range_val]; erw [Subtype.range_coe] + rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Subtype.range_val, Subtype.range_coe] rfl #align algebraic_geometry.pullback_restrict_iso_restrict AlgebraicGeometry.pullbackRestrictIsoRestrict @@ -1129,9 +1122,8 @@ def morphismRestrictRestrictBasicOpen {X Y : Scheme} (f : X ⟶ Y) (U : Opens Y) rw [eqToHom_op, eqToHom_op, eqToHom_map, eqToHom_trans] erw [← e] ext1; dsimp [Opens.map, Opens.inclusion] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]; erw [ContinuousMap.coe_mk] - rw [Subtype.range_val] + rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left, ContinuousMap.coe_mk, + Subtype.range_val] exact Y.basicOpen_le r #align algebraic_geometry.morphism_restrict_restrict_basic_open AlgebraicGeometry.morphismRestrictRestrictBasicOpen diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean index 6ab842327e12b..67692b738bf6f 100644 --- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean +++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean @@ -211,10 +211,6 @@ def structurePresheafInCommRing : Presheaf CommRingCat (ProjectiveSpectrum.top set_option linter.uppercaseLean3 false in #align algebraic_geometry.projective_spectrum.structure_sheaf.structure_presheaf_in_CommRing AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] - AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_map_apply - /-- Some glue, verifying that that structure presheaf valued in `CommRing` agrees with the `Type` valued structure presheaf.-/ def structurePresheafCompForget : diff --git a/Mathlib/AlgebraicGeometry/Spec.lean b/Mathlib/AlgebraicGeometry/Spec.lean index 1b4a6ebf121ec..a0667b2551d27 100644 --- a/Mathlib/AlgebraicGeometry/Spec.lean +++ b/Mathlib/AlgebraicGeometry/Spec.lean @@ -241,8 +241,7 @@ theorem localRingHom_comp_stalkIso {R S : CommRingCat} (f : R ⟶ S) (p : PrimeS (stalkIso R (PrimeSpectrum.comap f p)).eq_inv_comp.mp <| (stalkIso S p).comp_inv_eq.mpr <| Localization.localRingHom_unique _ _ _ _ fun x => by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - rw [stalkIso_hom, stalkIso_inv]; erw [comp_apply, comp_apply]; rw [localizationToStalk_of] + rw [stalkIso_hom, stalkIso_inv, comp_apply, comp_apply, localizationToStalk_of] erw [stalkMap_toStalk_apply f p x, stalkToFiberRingHom_toStalk] set_option linter.uppercaseLean3 false in #align algebraic_geometry.local_ring_hom_comp_stalk_iso AlgebraicGeometry.localRingHom_comp_stalkIso @@ -309,9 +308,6 @@ def toSpecΓ (R : CommRingCat) : R ⟶ Γ.obj (op (Spec.toLocallyRingedSpace.obj set_option linter.uppercaseLean3 false in #align algebraic_geometry.to_Spec_Γ AlgebraicGeometry.toSpecΓ --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] AlgebraicGeometry.toSpecΓ_apply_coe - instance isIso_toSpecΓ (R : CommRingCat) : IsIso (toSpecΓ R) := by cases R; apply StructureSheaf.isIso_to_global set_option linter.uppercaseLean3 false in diff --git a/Mathlib/AlgebraicGeometry/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/StructureSheaf.lean index 357835cb569f5..8ceadffc4a48d 100644 --- a/Mathlib/AlgebraicGeometry/StructureSheaf.lean +++ b/Mathlib/AlgebraicGeometry/StructureSheaf.lean @@ -247,9 +247,6 @@ def structurePresheafInCommRing : Presheaf CommRingCat (PrimeSpectrum.Top R) whe set_option linter.uppercaseLean3 false in #align algebraic_geometry.structure_presheaf_in_CommRing AlgebraicGeometry.structurePresheafInCommRing --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] AlgebraicGeometry.structurePresheafInCommRing_map_apply - /-- Some glue, verifying that that structure presheaf valued in `CommRingCat` agrees with the `Type` valued structure presheaf. -/ @@ -593,9 +590,8 @@ def stalkIso (x : PrimeSpectrum.Top R) : (RingHom.comp (stalkToFiberRingHom R x) (localizationToStalk R x)) (RingHom.id (Localization.AtPrime _)) <| by ext f - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - rw [RingHom.comp_apply, RingHom.comp_apply]; erw [localizationToStalk_of, - stalkToFiberRingHom_toStalk]; rw [RingHom.comp_apply, RingHom.id_apply] + rw [RingHom.comp_apply, RingHom.comp_apply, localizationToStalk_of, + stalkToFiberRingHom_toStalk, RingHom.comp_apply, RingHom.id_apply] #align algebraic_geometry.structure_sheaf.stalk_iso AlgebraicGeometry.StructureSheaf.stalkIso instance (x : PrimeSpectrum R) : IsIso (stalkToFiberRingHom R x) := @@ -628,8 +624,7 @@ theorem toBasicOpen_mk' (s f : R) (g : Submonoid.powers s) : toBasicOpen R s (IsLocalization.mk' (Localization.Away s) f g) = const R f g (PrimeSpectrum.basicOpen s) fun x hx => Submonoid.powers_subset hx g.2 := (IsLocalization.lift_mk'_spec _ _ _ _).2 <| by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [toOpen_eq_const, toOpen_eq_const]; rw [const_mul_cancel'] + rw [toOpen_eq_const, toOpen_eq_const, const_mul_cancel'] #align algebraic_geometry.structure_sheaf.to_basic_open_mk' AlgebraicGeometry.StructureSheaf.toBasicOpen_mk' @[simp] @@ -1013,9 +1008,6 @@ def globalSectionsIso : CommRingCat.of R ≅ (structureSheaf R).1.obj (op ⊤) : asIso (toOpen R ⊤) #align algebraic_geometry.structure_sheaf.global_sections_iso AlgebraicGeometry.StructureSheaf.globalSectionsIso --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom_apply_coe - @[simp] theorem globalSectionsIso_hom (R : CommRingCat) : (globalSectionsIso R).hom = toOpen R ⊤ := rfl diff --git a/Mathlib/AlgebraicTopology/CechNerve.lean b/Mathlib/AlgebraicTopology/CechNerve.lean index 4323adcd7ff9c..8545d54209844 100644 --- a/Mathlib/AlgebraicTopology/CechNerve.lean +++ b/Mathlib/AlgebraicTopology/CechNerve.lean @@ -180,14 +180,7 @@ abbrev cechNerveAdjunction : (Augmented.toArrow : _ ⥤ Arrow C) ⊣ augmentedCe Adjunction.mkOfHomEquiv { homEquiv := cechNerveEquiv homEquiv_naturality_left_symm := by dsimp [cechNerveEquiv]; aesop_cat - homEquiv_naturality_right := by - dsimp [cechNerveEquiv] - -- The next three lines were not needed before leanprover/lean4#2644 - intro X Y Y' f g - change equivalenceLeftToRight X Y' (f ≫ g) = - equivalenceLeftToRight X Y f ≫ augmentedCechNerve.map g - aesop_cat - } + homEquiv_naturality_right := by dsimp [cechNerveEquiv]; aesop_cat } #align category_theory.simplicial_object.cech_nerve_adjunction CategoryTheory.SimplicialObject.cechNerveAdjunction end SimplicialObject diff --git a/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean b/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean index 98223d3233c1b..e546e922140aa 100644 --- a/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean +++ b/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean @@ -324,10 +324,8 @@ def fundamentalGroupoidFunctor : TopCat ⥤ CategoryTheory.Grpd where map := fun {X Y} p => by exact Path.Homotopic.Quotient.mapFn p f map_id := fun X => rfl map_comp := fun {x y z} p q => by - refine Quotient.inductionOn₂ p q fun a b => ?_ - simp only [comp_eq, ← Path.Homotopic.map_lift, ← Path.Homotopic.comp_lift, Path.map_trans] - -- This was not needed before leanprover/lean4#2644 - erw [ ← Path.Homotopic.comp_lift]; rfl} + refine' Quotient.inductionOn₂ p q fun a b => _ + simp only [comp_eq, ← Path.Homotopic.map_lift, ← Path.Homotopic.comp_lift, Path.map_trans] } map_id X := by simp only change _ = (⟨_, _, _⟩ : FundamentalGroupoid X ⥤ FundamentalGroupoid X) diff --git a/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean b/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean index 912fd846ce418..5257616193dec 100644 --- a/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean +++ b/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean @@ -142,8 +142,7 @@ def uliftMap : C(TopCat.of (ULift.{u} I × X), Y) := H.continuous.comp ((continuous_induced_dom.comp continuous_fst).prod_mk continuous_snd)⟩ #align continuous_map.homotopy.ulift_map ContinuousMap.Homotopy.uliftMap --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[simp, nolint simpNF] +@[simp] theorem ulift_apply (i : ULift.{u} I) (x : X) : H.uliftMap (i, x) = H (i.down, x) := rfl #align continuous_map.homotopy.ulift_apply ContinuousMap.Homotopy.ulift_apply @@ -172,8 +171,7 @@ theorem apply_zero_path : (πₘ f).map p = hcast (H.apply_zero x₀).symm ≫ hcast (H.apply_zero x₁) := Quotient.inductionOn p fun p' => by apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p') - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [Path.prod_coe]; simp_rw [ulift_apply]; simp + rw [Path.prod_coe]; simp_rw [ulift_apply]; simp #align continuous_map.homotopy.apply_zero_path ContinuousMap.Homotopy.apply_zero_path /-- Proof that `g(p) = H(1 ⟶ 1, p)`, with the appropriate casts -/ @@ -182,8 +180,7 @@ theorem apply_one_path : (πₘ g).map p = hcast (H.apply_one x₀).symm ≫ hcast (H.apply_one x₁) := Quotient.inductionOn p fun p' => by apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p') - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [Path.prod_coe]; simp_rw [ulift_apply]; simp + rw [Path.prod_coe]; simp_rw [ulift_apply]; simp #align continuous_map.homotopy.apply_one_path ContinuousMap.Homotopy.apply_one_path /-- Proof that `H.evalAt x = H(0 ⟶ 1, x ⟶ x)`, with the appropriate casts -/ diff --git a/Mathlib/AlgebraicTopology/SimplexCategory.lean b/Mathlib/AlgebraicTopology/SimplexCategory.lean index 30a4f2f05d1d5..d4fcdd3079f30 100644 --- a/Mathlib/AlgebraicTopology/SimplexCategory.lean +++ b/Mathlib/AlgebraicTopology/SimplexCategory.lean @@ -523,13 +523,9 @@ instance {n : ℕ} {i : Fin (n + 1)} : Epi (σ i) := by simp only [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk] by_cases b ≤ i · use b - -- This was not needed before leanprover/lean4#2644 - dsimp rw [Fin.predAbove_below i b (by simpa only [Fin.coe_eq_castSucc] using h)] simp only [len_mk, Fin.coe_eq_castSucc, Fin.castPred_castSucc] · use b.succ - -- This was not needed before leanprover/lean4#2644 - dsimp rw [Fin.predAbove_above i b.succ _, Fin.pred_succ] rw [not_le] at h rw [Fin.lt_iff_val_lt_val] at h ⊢ @@ -603,9 +599,7 @@ theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : mk simp only [Hom.toOrderHom_mk, Function.comp_apply, OrderHom.comp_coe, Hom.comp, smallCategory_comp, σ, mkHom, OrderHom.coe_mk] by_cases h' : x ≤ Fin.castSucc i - · -- This was not needed before leanprover/lean4#2644 - dsimp - rw [Fin.predAbove_below i x h'] + · rw [Fin.predAbove_below i x h'] have eq := Fin.castSucc_castPred (gt_of_gt_of_ge (Fin.castSucc_lt_last i) h') dsimp [δ] erw [Fin.succAbove_below i.succ x.castPred _] @@ -616,12 +610,10 @@ theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : mk let y := x.pred <| by rintro (rfl : x = 0); simp at h' have hy : x = y.succ := (Fin.succ_pred x _).symm rw [hy] at h' ⊢ - -- This was not needed before leanprover/lean4#2644 - conv_rhs => dsimp rw [Fin.predAbove_above i y.succ h', Fin.pred_succ] by_cases h'' : y = i · rw [h''] - refine hi.symm.trans ?_ + refine' hi.symm.trans _ congr 1 dsimp [δ] erw [Fin.succAbove_below i.succ] @@ -679,10 +671,7 @@ theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ smallCategory_comp] by_cases h' : θ.toOrderHom x ≤ i · simp only [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk] - -- This was not needed before leanprover/lean4#2644 - dsimp - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [Fin.predAbove_below (Fin.castPred i) (θ.toOrderHom x) + rw [Fin.predAbove_below (Fin.castPred i) (θ.toOrderHom x) (by simpa [Fin.castSucc_castPred h] using h')] dsimp [δ] erw [Fin.succAbove_below i] @@ -694,16 +683,11 @@ theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ rw [Fin.castSucc_castPred] apply lt_of_le_of_lt h' h · simp only [not_le] at h' - -- The next three tactics used to be a simp only call before leanprover/lean4#2644 - rw [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk, OrderHom.coe_mk] - erw [OrderHom.coe_mk] - erw [Fin.predAbove_above (Fin.castPred i) (θ.toOrderHom x) + simp only [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk, + Fin.predAbove_above (Fin.castPred i) (θ.toOrderHom x) (by simpa only [Fin.castSucc_castPred h] using h')] dsimp [δ] - rw [Fin.succAbove_above i _] - -- This was not needed before leanprover/lean4#2644 - conv_rhs => dsimp - erw [Fin.succ_pred] + erw [Fin.succAbove_above i _, Fin.succ_pred] simpa only [Fin.le_iff_val_le_val, Fin.coe_castSucc, Fin.coe_pred] using Nat.le_pred_of_lt (Fin.lt_iff_val_lt_val.mp h') · obtain rfl := le_antisymm (Fin.le_last i) (not_lt.mp h) diff --git a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean index c82c145c8499c..32db1cfc671fc 100644 --- a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean +++ b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean @@ -101,9 +101,7 @@ def toTop : SimplexCategory ⥤ TopCat where apply toTopObj.ext funext i dsimp - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - rw [CategoryTheory.comp_apply]; erw [ContinuousMap.coe_mk, - ContinuousMap.coe_mk, ContinuousMap.coe_mk] + rw [CategoryTheory.comp_apply, ContinuousMap.coe_mk, ContinuousMap.coe_mk, ContinuousMap.coe_mk] simp only [coe_toTopMap] erw [← Finset.sum_biUnion] · apply Finset.sum_congr @@ -121,7 +119,4 @@ def toTop : SimplexCategory ⥤ TopCat where set_option linter.uppercaseLean3 false in #align simplex_category.to_Top SimplexCategory.toTop --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] SimplexCategory.toTop_map_apply - end SimplexCategory diff --git a/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean b/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean index be45dcb7de0a1..724c1c321d32a 100644 --- a/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean +++ b/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Doll -/ import Mathlib.Analysis.InnerProductSpace.Adjoint +import Mathlib.Analysis.InnerProductSpace.ProdL2 import Mathlib.Topology.Algebra.Module.LinearPMap import Mathlib.Topology.Algebra.Module.Basic @@ -27,6 +28,8 @@ We will develop the basics of the theory of unbounded operators on Hilbert space * `LinearPMap.IsFormalAdjoint.le_adjoint`: Every formal adjoint is contained in the adjoint * `ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense`: The adjoint on `ContinuousLinearMap` and `LinearPMap` coincide. +* `LinearPMap.adjoint_isClosed`: The adjoint is a closed operator. +* `IsSelfAdjoint.isClosed`: Every self-adjoint operator is closed. ## Notation @@ -51,7 +54,7 @@ Unbounded operators, closed operators noncomputable section -open IsROrC +open IsROrC LinearPMap open scoped ComplexConjugate Classical @@ -268,3 +271,93 @@ theorem _root_.IsSelfAdjoint.dense_domain (hA : IsSelfAdjoint A) : Dense (A.doma end LinearPMap end Star + +/-! ### The graph of the adjoint -/ + +namespace Submodule + +/-- The adjoint of a submodule + +Note that the adjoint is taken with respect to the L^2 inner product on `E × F`, which is defined +as `WithLp 2 (E × F)`. -/ +protected noncomputable +def adjoint (g : Submodule 𝕜 (E × F)) : Submodule 𝕜 (F × E) := + (g.map <| (LinearEquiv.skewSwap 𝕜 F E).symm.trans + (WithLp.linearEquiv 2 𝕜 (F × E)).symm).orthogonal.map (WithLp.linearEquiv 2 𝕜 (F × E)) + +@[simp] +theorem mem_adjoint_iff (g : Submodule 𝕜 (E × F)) (x : F × E) : + x ∈ g.adjoint ↔ + ∀ a b, (a, b) ∈ g → inner (𝕜 := 𝕜) b x.fst - inner a x.snd = 0 := by + simp only [Submodule.adjoint, Submodule.mem_map, Submodule.mem_orthogonal, LinearMap.coe_comp, + LinearEquiv.coe_coe, WithLp.linearEquiv_symm_apply, Function.comp_apply, + LinearEquiv.skewSwap_symm_apply, Prod.exists, WithLp.prod_inner_apply, forall_exists_index, + and_imp, WithLp.linearEquiv_apply] + constructor + · rintro ⟨y, h1, h2⟩ a b hab + rw [← h2, WithLp.equiv_fst, WithLp.equiv_snd] + specialize h1 (b, -a) a b hab rfl + simp only [inner_neg_left, ← sub_eq_add_neg] at h1 + exact h1 + · intro h + refine ⟨x, ?_, rfl⟩ + intro u a b hab hu + simp [← hu, ← sub_eq_add_neg, h a b hab] + +variable {T : E →ₗ.[𝕜] F} [CompleteSpace E] + +theorem _root_.LinearPMap.adjoint_graph_eq_graph_adjoint (hT : Dense (T.domain : Set E)) : + T†.graph = T.graph.adjoint := by + ext x + simp only [mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left, mem_adjoint_iff, + forall_exists_index, forall_apply_eq_imp_iff'] + constructor + · rintro ⟨hx, h⟩ a ha + rw [← h, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩, sub_self] + · intro h + simp_rw [sub_eq_zero] at h + have hx : x.fst ∈ T†.domain + · apply mem_adjoint_domain_of_exists + use x.snd + rintro ⟨a, ha⟩ + rw [← inner_conj_symm, ← h a ha, inner_conj_symm] + use hx + apply hT.eq_of_inner_right + rintro ⟨a, ha⟩ + rw [← h a ha, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩] + +@[simp] +theorem _root_.LinearPMap.graph_adjoint_toLinearPMap_eq_adjoint (hT : Dense (T.domain : Set E)) : + T.graph.adjoint.toLinearPMap = T† := by + apply eq_of_eq_graph + rw [adjoint_graph_eq_graph_adjoint hT] + apply Submodule.toLinearPMap_graph_eq + intro x hx hx' + simp only [mem_adjoint_iff, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left, + forall_exists_index, forall_apply_eq_imp_iff', hx', inner_zero_right, zero_sub, + neg_eq_zero] at hx + apply hT.eq_zero_of_inner_right + rintro ⟨a, ha⟩ + exact hx a ha + +end Submodule + +/-! ### Closedness -/ + +namespace LinearPMap + +variable {T : E →ₗ.[𝕜] F} [CompleteSpace E] + +theorem adjoint_isClosed (hT : Dense (T.domain : Set E)) : + T†.IsClosed := by + rw [IsClosed, adjoint_graph_eq_graph_adjoint hT, Submodule.adjoint] + simp only [Submodule.map_coe, WithLp.linearEquiv_apply] + rw [Equiv.image_eq_preimage] + exact (Submodule.isClosed_orthogonal _).preimage (WithLp.prod_continuous_equiv_symm _ _ _) + +/-- Every self-adjoint `LinearPMap` is closed. -/ +theorem _root_.IsSelfAdjoint.isClosed {A : E →ₗ.[𝕜] E} (hA : IsSelfAdjoint A) : A.IsClosed := by + rw [← isSelfAdjoint_def.mp hA] + exact adjoint_isClosed hA.dense_domain + +end LinearPMap diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean index 231d4368e6437..3684a6d67c745 100644 --- a/Mathlib/Analysis/InnerProductSpace/PiL2.lean +++ b/Mathlib/Analysis/InnerProductSpace/PiL2.lean @@ -422,9 +422,8 @@ protected theorem coe_toBasis_repr (b : OrthonormalBasis ι 𝕜 E) : @[simp] protected theorem coe_toBasis_repr_apply (b : OrthonormalBasis ι 𝕜 E) (x : E) (i : ι) : b.toBasis.repr x i = b.repr x i := by - rw [← Basis.equivFun_apply, OrthonormalBasis.coe_toBasis_repr]; - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [LinearIsometryEquiv.coe_toLinearEquiv] + rw [← Basis.equivFun_apply, OrthonormalBasis.coe_toBasis_repr, + LinearIsometryEquiv.coe_toLinearEquiv] #align orthonormal_basis.coe_to_basis_repr_apply OrthonormalBasis.coe_toBasis_repr_apply protected theorem sum_repr (b : OrthonormalBasis ι 𝕜 E) (x : E) : ∑ i, b.repr x i • b i = x := by diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index 24026b008f81b..35349905d6386 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -1337,8 +1337,7 @@ theorem OrthogonalFamily.projection_directSum_coeAddHom [DecidableEq ι] {V : ι · simp · simp_rw [DirectSum.coeAddMonoidHom_of, DirectSum.of] -- porting note: was in the previous `simp_rw`, no longer works - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [DFinsupp.singleAddHom_apply] + rw [DFinsupp.singleAddHom_apply] obtain rfl | hij := Decidable.eq_or_ne i j · rw [orthogonalProjection_mem_subspace_eq_self, DFinsupp.single_eq_same] · rw [orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, @@ -1363,9 +1362,8 @@ def OrthogonalFamily.decomposition [DecidableEq ι] [Fintype ι] {V : ι → Sub left_inv x := by dsimp only letI := fun i => Classical.decEq (V i) - rw [DirectSum.coeAddMonoidHom, DirectSum.toAddMonoid, DFinsupp.liftAddHom_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [DFinsupp.sumAddHom_apply]; rw [DFinsupp.sum_eq_sum_fintype] + rw [DirectSum.coeAddMonoidHom, DirectSum.toAddMonoid, DFinsupp.liftAddHom_apply, + DFinsupp.sumAddHom_apply, DFinsupp.sum_eq_sum_fintype] · simp_rw [Equiv.apply_symm_apply, AddSubmonoidClass.coe_subtype] exact hV.sum_projection_of_mem_iSup _ ((h.ge : _) Submodule.mem_top) · intro i diff --git a/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean b/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean index 628a23e7cc11f..d3096da393de8 100644 --- a/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean +++ b/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean @@ -122,8 +122,7 @@ theorem iso_isometry_of_normNoninc {V W : SemiNormedGroupCat} (i : V ≅ W) (h1 intro v apply le_antisymm (h1 v) calc - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - ‖v‖ = ‖i.inv (i.hom v)‖ := by erw [Iso.hom_inv_id_apply] + ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [Iso.hom_inv_id_apply] _ ≤ ‖i.hom v‖ := h2 _ #align SemiNormedGroup.iso_isometry_of_norm_noninc SemiNormedGroupCat.iso_isometry_of_normNoninc @@ -259,8 +258,7 @@ theorem iso_isometry {V W : SemiNormedGroupCat₁} (i : V ≅ W) : Isometry i.ho intro v apply le_antisymm (i.hom.2 v) calc - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - ‖v‖ = ‖i.inv (i.hom v)‖ := by erw [Iso.hom_inv_id_apply] + ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [Iso.hom_inv_id_apply] _ ≤ ‖i.hom v‖ := i.inv.2 _ #align SemiNormedGroup₁.iso_isometry SemiNormedGroupCat₁.iso_isometry diff --git a/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat/Completion.lean b/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat/Completion.lean index b01c04c436c95..1861b38f695ec 100644 --- a/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat/Completion.lean +++ b/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat/Completion.lean @@ -63,9 +63,6 @@ def completion.incl {V : SemiNormedGroupCat} : V ⟶ completion.obj V where bound' := ⟨1, fun v => by simp⟩ #align SemiNormedGroup.Completion.incl SemiNormedGroupCat.completion.incl --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] SemiNormedGroupCat.completion.incl_apply - theorem completion.norm_incl_eq {V : SemiNormedGroupCat} {v : V} : ‖completion.incl v‖ = ‖v‖ := UniformSpace.Completion.norm_coe _ #align SemiNormedGroup.Completion.norm_incl_eq SemiNormedGroupCat.completion.norm_incl_eq @@ -104,8 +101,7 @@ instance : Preadditive SemiNormedGroupCat.{u} where -- Porting note: failing simps probably due to instance synthesis issues with concrete -- cats; see the gymnastics below for what used to be -- simp only [add_apply, comp_apply. map_add] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - rw [NormedAddGroupHom.add_apply]; erw [CategoryTheory.comp_apply, CategoryTheory.comp_apply, + rw [NormedAddGroupHom.add_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply, @NormedAddGroupHom.add_apply _ _ (_) (_)] convert map_add g (f x) (f' x) comp_add := by @@ -113,11 +109,8 @@ instance : Preadditive SemiNormedGroupCat.{u} where -- Porting note: failing simps probably due to instance synthesis issues with concrete -- cats; see the gymnastics below for what used to be -- simp only [add_apply, comp_apply. map_add] - rw [NormedAddGroupHom.add_apply] - -- This used to be a single `rw`, but we need `erw` after leanprover/lean4#2644 - erw [CategoryTheory.comp_apply, CategoryTheory.comp_apply, + rw [NormedAddGroupHom.add_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply, @NormedAddGroupHom.add_apply _ _ (_) (_)] - rfl instance : Functor.Additive completion where map_add := NormedAddGroupHom.completion_add _ _ @@ -143,3 +136,4 @@ theorem completion.lift_unique {V W : SemiNormedGroupCat} [CompleteSpace W] [Sep #align SemiNormedGroup.Completion.lift_unique SemiNormedGroupCat.completion.lift_unique end SemiNormedGroupCat + diff --git a/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat/Kernels.lean b/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat/Kernels.lean index ef56e75c0d415..6298046e4f262 100644 --- a/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat/Kernels.lean +++ b/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat/Kernels.lean @@ -45,8 +45,7 @@ def cokernelCocone {X Y : SemiNormedGroupCat₁.{u}} (f : X ⟶ Y) : Cofork f 0 -- simp only [comp_apply, Limits.zero_comp, NormedAddGroupHom.zero_apply, -- SemiNormedGroupCat₁.mkHom_apply, SemiNormedGroupCat₁.zero_apply, -- ← NormedAddGroupHom.mem_ker, f.1.range.ker_normedMk, f.1.mem_range] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [Limits.zero_comp, comp_apply, SemiNormedGroupCat₁.mkHom_apply, + rw [Limits.zero_comp, comp_apply, SemiNormedGroupCat₁.mkHom_apply, SemiNormedGroupCat₁.zero_apply, ← NormedAddGroupHom.mem_ker, f.1.range.ker_normedMk, f.1.mem_range] use x @@ -63,8 +62,6 @@ def cokernelLift {X Y : SemiNormedGroupCat₁.{u}} (f : X ⟶ Y) (s : CokernelCo rintro _ ⟨b, rfl⟩ change (f ≫ s.π) b = 0 simp - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [zero_apply] -- The lift has norm at most one: exact NormedAddGroupHom.lift_normNoninc _ _ _ s.π.2 set_option linter.uppercaseLean3 false in @@ -81,9 +78,7 @@ instance : HasCokernels SemiNormedGroupCat₁.{u} where apply NormedAddGroupHom.lift_mk f.1.range rintro _ ⟨b, rfl⟩ change (f ≫ s.π) b = 0 - simp - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [zero_apply]) + simp) fun s m w => Subtype.eq (NormedAddGroupHom.lift_unique f.1.range _ _ _ (congr_arg Subtype.val w : _)) } @@ -152,19 +147,16 @@ noncomputable def cokernelCocone {X Y : SemiNormedGroupCat.{u}} (f : X ⟶ Y) : Cofork f 0 := @Cofork.ofπ _ _ _ _ _ _ (SemiNormedGroupCat.of (Y ⧸ NormedAddGroupHom.range f)) f.range.normedMk (by - ext a + ext simp only [comp_apply, Limits.zero_comp] -- porting note: `simp` not firing on the below - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [comp_apply, NormedAddGroupHom.zero_apply] + rw [comp_apply, NormedAddGroupHom.zero_apply] -- porting note: Lean 3 didn't need this instance letI : SeminormedAddCommGroup ((forget SemiNormedGroupCat).obj Y) := (inferInstance : SeminormedAddCommGroup Y) -- porting note: again simp doesn't seem to be firing in the below line - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ ←NormedAddGroupHom.mem_ker, f.range.ker_normedMk, f.mem_range] - -- This used to be `simp only [exists_apply_eq_apply]` before leanprover/lean4#2644 - convert exists_apply_eq_apply f a) + rw [ ←NormedAddGroupHom.mem_ker, f.range.ker_normedMk, f.mem_range] + simp only [exists_apply_eq_apply]) set_option linter.uppercaseLean3 false in #align SemiNormedGroup.cokernel_cocone SemiNormedGroupCat.cokernelCocone @@ -176,9 +168,7 @@ def cokernelLift {X Y : SemiNormedGroupCat.{u}} (f : X ⟶ Y) (s : CokernelCofor (by rintro _ ⟨b, rfl⟩ change (f ≫ s.π) b = 0 - simp - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [zero_apply]) + simp) set_option linter.uppercaseLean3 false in #align SemiNormedGroup.cokernel_lift SemiNormedGroupCat.cokernelLift @@ -192,9 +182,7 @@ def isColimitCokernelCocone {X Y : SemiNormedGroupCat.{u}} (f : X ⟶ Y) : apply NormedAddGroupHom.lift_mk f.range rintro _ ⟨b, rfl⟩ change (f ≫ s.π) b = 0 - simp - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [zero_apply]) + simp) fun s m w => NormedAddGroupHom.lift_unique f.range _ _ _ w set_option linter.uppercaseLean3 false in #align SemiNormedGroup.is_colimit_cokernel_cocone SemiNormedGroupCat.isColimitCokernelCocone diff --git a/Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean b/Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean index 9b38946336ad8..c66d614d34c63 100644 --- a/Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean +++ b/Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean @@ -81,12 +81,10 @@ theorem exists_extension_norm_eq (p : Subspace 𝕜 F) (f : p →L[𝕜] 𝕜) : -- It is an extension of `f`. have h : ∀ x : p, g.extendTo𝕜 x = f x := by intro x - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ContinuousLinearMap.extendTo𝕜_apply, ← Submodule.coe_smul, hextends, hextends] + rw [ContinuousLinearMap.extendTo𝕜_apply, ← Submodule.coe_smul, hextends, hextends] have : (fr x : 𝕜) - I * ↑(fr (I • x)) = (re (f x) : 𝕜) - (I : 𝕜) * re (f ((I : 𝕜) • x)) := by rfl - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [this] + rw [this] apply ext · simp only [add_zero, Algebra.id.smul_eq_mul, I_re, ofReal_im, AddMonoidHom.map_add, zero_sub, I_im', zero_mul, ofReal_re, eq_self_iff_true, sub_zero, mul_neg, ofReal_neg, diff --git a/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean b/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean index dc75e127f400d..57881e086b159 100644 --- a/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean +++ b/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean @@ -484,14 +484,12 @@ theorem ModuleCat.eq_range_of_pseudoequal {R : Type*} [CommRing R] {G : ModuleCa · obtain ⟨a', ha'⟩ := ha obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective p).1 hp a' refine' ⟨q a'', _⟩ - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← LinearMap.comp_apply, ← ModuleCat.comp_def, ← H, - ModuleCat.comp_def, LinearMap.comp_apply, ha'', ha'] + rw [← LinearMap.comp_apply, ← ModuleCat.comp_def, ← H, ModuleCat.comp_def, LinearMap.comp_apply, + ha'', ha'] · obtain ⟨a', ha'⟩ := ha obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective q).1 hq a' refine' ⟨p a'', _⟩ - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← LinearMap.comp_apply, ← ModuleCat.comp_def, H, ModuleCat.comp_def, LinearMap.comp_apply, + rw [← LinearMap.comp_apply, ← ModuleCat.comp_def, H, ModuleCat.comp_def, LinearMap.comp_apply, ha'', ha'] set_option linter.uppercaseLean3 false in #align category_theory.abelian.pseudoelement.Module.eq_range_of_pseudoequal CategoryTheory.Abelian.Pseudoelement.ModuleCat.eq_range_of_pseudoequal diff --git a/Mathlib/CategoryTheory/Adjunction/Comma.lean b/Mathlib/CategoryTheory/Adjunction/Comma.lean index bc0600229872b..b6abb6ce167ee 100644 --- a/Mathlib/CategoryTheory/Adjunction/Comma.lean +++ b/Mathlib/CategoryTheory/Adjunction/Comma.lean @@ -147,8 +147,7 @@ def mkInitialOfLeftAdjoint (h : F ⊣ G) (A : C) : uniq s m _ := by apply StructuredArrow.ext dsimp - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [Equiv.eq_symm_apply, Adjunction.homEquiv_unit] + rw [Equiv.eq_symm_apply, Adjunction.homEquiv_unit] apply StructuredArrow.w m #align category_theory.mk_initial_of_left_adjoint CategoryTheory.mkInitialOfLeftAdjoint diff --git a/Mathlib/CategoryTheory/Adjunction/Evaluation.lean b/Mathlib/CategoryTheory/Adjunction/Evaluation.lean index c29c77ce3dc11..0143fe17f0749 100644 --- a/Mathlib/CategoryTheory/Adjunction/Evaluation.lean +++ b/Mathlib/CategoryTheory/Adjunction/Evaluation.lean @@ -69,9 +69,7 @@ def evaluationAdjunctionRight (c : C) : evaluationLeftAdjoint D c ⊣ (evaluatio Discrete.functor_obj, Cofan.mk_pt, Discrete.natTrans_app, Category.id_comp] right_inv := fun f => by dsimp - simp } - -- This used to be automatic before leanprover/lean4#2644 - homEquiv_naturality_right := by intros; dsimp; simp } + simp } } #align category_theory.evaluation_adjunction_right CategoryTheory.evaluationAdjunctionRight instance evaluationIsRightAdjoint (c : C) : IsRightAdjoint ((evaluation _ D).obj c) := diff --git a/Mathlib/CategoryTheory/Adjunction/Lifting.lean b/Mathlib/CategoryTheory/Adjunction/Lifting.lean index ecc1fff51c132..98d231b478812 100644 --- a/Mathlib/CategoryTheory/Adjunction/Lifting.lean +++ b/Mathlib/CategoryTheory/Adjunction/Lifting.lean @@ -160,12 +160,10 @@ noncomputable def constructLeftAdjoint [∀ X : B, RegularEpi (adj₁.counit.app rw [constructLeftAdjointEquiv_apply, constructLeftAdjointEquiv_apply, Equiv.symm_apply_eq, Subtype.ext_iff] dsimp - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [Cofork.IsColimit.homIso_natural, Cofork.IsColimit.homIso_natural] + rw [Cofork.IsColimit.homIso_natural, Cofork.IsColimit.homIso_natural] erw [adj₂.homEquiv_naturality_right] simp_rw [Functor.comp_map] - -- This used to be `simp`, but we need `aesop_cat` after leanprover/lean4#2644 - aesop_cat + simp #align category_theory.lift_adjoint.construct_left_adjoint CategoryTheory.LiftAdjoint.constructLeftAdjoint end LiftAdjoint diff --git a/Mathlib/CategoryTheory/Closed/Cartesian.lean b/Mathlib/CategoryTheory/Closed/Cartesian.lean index 754756e8c33ec..3405b77ed296e 100644 --- a/Mathlib/CategoryTheory/Closed/Cartesian.lean +++ b/Mathlib/CategoryTheory/Closed/Cartesian.lean @@ -111,11 +111,9 @@ abbrev coev : 𝟭 C ⟶ prod.functor.obj A ⋙ exp A := -- porting note: notation fails to elaborate with `quotPrecheck` on. set_option quotPrecheck false in -/-- Morphisms obtained using an exponentiable object. -/ notation:20 A " ⟹ " B:19 => (exp A).obj B open Lean PrettyPrinter.Delaborator SubExpr in -/-- Delaborator for `Prefunctor.obj` -/ @[delab app.Prefunctor.obj] def delabPrefunctorObjExp : Delab := do let e ← getExpr @@ -132,7 +130,6 @@ def delabPrefunctorObjExp : Delab := do -- porting note: notation fails to elaborate with `quotPrecheck` on. set_option quotPrecheck false in -/-- Morphisms from an exponentiable object. -/ notation:30 B " ^^ " A:30 => (exp A).obj B @[simp, reassoc] @@ -165,14 +162,12 @@ def uncurry : (Y ⟶ A ⟹ X) → (A ⨯ Y ⟶ X) := ((exp.adjunction A).homEquiv _ _).symm #align category_theory.cartesian_closed.uncurry CategoryTheory.CartesianClosed.uncurry --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[simp, nolint simpNF] +@[simp] theorem homEquiv_apply_eq (f : A ⨯ Y ⟶ X) : (exp.adjunction A).homEquiv _ _ f = curry f := rfl #align category_theory.cartesian_closed.hom_equiv_apply_eq CategoryTheory.CartesianClosed.homEquiv_apply_eq --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[simp, nolint simpNF] +@[simp] theorem homEquiv_symm_apply_eq (f : Y ⟶ A ⟹ X) : ((exp.adjunction A).homEquiv _ _).symm f = uncurry f := rfl @@ -439,6 +434,4 @@ def cartesianClosedOfEquiv (e : C ≌ D) [h : CartesianClosed C] : CartesianClos end Functor -attribute [nolint simpNF] CategoryTheory.CartesianClosed.homEquiv_apply_eq - CategoryTheory.CartesianClosed.homEquiv_symm_apply_eq end CategoryTheory diff --git a/Mathlib/CategoryTheory/Closed/FunctorCategory.lean b/Mathlib/CategoryTheory/Closed/FunctorCategory.lean index 11c268d6f8716..080bb6fcc057e 100644 --- a/Mathlib/CategoryTheory/Closed/FunctorCategory.lean +++ b/Mathlib/CategoryTheory/Closed/FunctorCategory.lean @@ -78,10 +78,6 @@ instance monoidalClosed : MonoidalClosed (D ⥤ C) where closed := by infer_instance #align category_theory.functor.monoidal_closed CategoryTheory.Functor.monoidalClosed --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] Functor.monoidalClosed_closed_isAdj_adj_homEquiv_apply_app - Functor.monoidalClosed_closed_isAdj_adj_homEquiv_symm_apply_app - theorem ihom_map (F : D ⥤ C) {G H : D ⥤ C} (f : G ⟶ H) : (ihom F).map f = (closedIhom F).map f := rfl #align category_theory.functor.ihom_map CategoryTheory.Functor.ihom_map diff --git a/Mathlib/CategoryTheory/Closed/Monoidal.lean b/Mathlib/CategoryTheory/Closed/Monoidal.lean index 1736ee80b1017..cd43bacb12d95 100644 --- a/Mathlib/CategoryTheory/Closed/Monoidal.lean +++ b/Mathlib/CategoryTheory/Closed/Monoidal.lean @@ -73,11 +73,7 @@ def unitClosed : Closed (𝟙_ C) where right_inv := by aesop_cat } homEquiv_naturality_left_symm := fun f g => by dsimp - rw [leftUnitor_naturality_assoc] - -- This used to be automatic before leanprover/lean4#2644 - homEquiv_naturality_right := by -- aesop failure - dsimp - simp }} + rw [leftUnitor_naturality_assoc] } } #align category_theory.unit_closed CategoryTheory.unitClosed variable (A B : C) {X X' Y Y' Z : C} @@ -165,14 +161,12 @@ def uncurry : (Y ⟶ A ⟶[C] X) → (A ⊗ Y ⟶ X) := ((ihom.adjunction A).homEquiv _ _).symm #align category_theory.monoidal_closed.uncurry CategoryTheory.MonoidalClosed.uncurry --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[simp, nolint simpNF] +@[simp] theorem homEquiv_apply_eq (f : A ⊗ Y ⟶ X) : (ihom.adjunction A).homEquiv _ _ f = curry f := rfl #align category_theory.monoidal_closed.hom_equiv_apply_eq CategoryTheory.MonoidalClosed.homEquiv_apply_eq --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[simp, nolint simpNF] +@[simp] theorem homEquiv_symm_apply_eq (f : Y ⟶ A ⟶[C] X) : ((ihom.adjunction A).homEquiv _ _).symm f = uncurry f := rfl @@ -349,6 +343,5 @@ theorem ofEquiv_uncurry_def (F : MonoidalFunctor C D) [IsEquivalence F.toFunctor end OfEquiv end MonoidalClosed -attribute [nolint simpNF] CategoryTheory.MonoidalClosed.homEquiv_apply_eq - CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq + end CategoryTheory diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean index ad52486fbe107..2e7c9f02f2863 100644 --- a/Mathlib/CategoryTheory/Limits/HasLimits.lean +++ b/Mathlib/CategoryTheory/Limits/HasLimits.lean @@ -582,13 +582,6 @@ def constLimAdj : (const J : C ⥤ J ⥤ C) ⊣ lim where right_inv := by aesop_cat } unit := { app := fun c => limit.lift _ ⟨_, 𝟙 _⟩ } counit := { app := fun g => { app := limit.π _ } } - -- This used to be automatic before leanprover/lean4#2644 - homEquiv_unit := by - -- Sad that aesop can no longer do this! - intros - dsimp - ext - simp #align category_theory.limits.const_lim_adj CategoryTheory.Limits.constLimAdj instance : IsRightAdjoint (lim : (J ⥤ C) ⥤ C) := diff --git a/Mathlib/CategoryTheory/Limits/KanExtension.lean b/Mathlib/CategoryTheory/Limits/KanExtension.lean index 9f0254ec8e02e..df8a4517ab0c3 100644 --- a/Mathlib/CategoryTheory/Limits/KanExtension.lean +++ b/Mathlib/CategoryTheory/Limits/KanExtension.lean @@ -324,12 +324,6 @@ def equiv (F : S ⥤ D) [I : ∀ x, HasColimit (diagram ι F x)] (G : L ⥤ D) : set_option linter.uppercaseLean3 false in #align category_theory.Lan.equiv CategoryTheory.Lan.equiv --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] CategoryTheory.Ran.equiv_symm_apply_app - CategoryTheory.Ran.equiv_apply_app - CategoryTheory.Lan.equiv_symm_apply_app - CategoryTheory.Lan.equiv_apply_app - end Lan /-- The left Kan extension of a functor. -/ @@ -338,10 +332,7 @@ def lan [∀ X, HasColimitsOfShape (CostructuredArrow ι X) D] : (S ⥤ D) ⥤ L Adjunction.leftAdjointOfEquiv (fun F G => Lan.equiv ι F G) (by { intros X' X Y f g ext - simp [Lan.equiv] - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [Equiv.coe_fn_mk, Equiv.coe_fn_mk] - simp }) + simp [Lan.equiv] }) set_option linter.uppercaseLean3 false in #align category_theory.Lan CategoryTheory.lan diff --git a/Mathlib/CategoryTheory/Limits/Over.lean b/Mathlib/CategoryTheory/Limits/Over.lean index 3c2f3e5bbe47f..9a0f31cc78816 100644 --- a/Mathlib/CategoryTheory/Limits/Over.lean +++ b/Mathlib/CategoryTheory/Limits/Over.lean @@ -108,10 +108,7 @@ def mapPullbackAdj {A B : C} (f : A ⟶ B) : Over.map f ⊣ pullback f := simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app] · dsimp simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, ← Over.w Y ] - rfl } - -- This used to be automatic before leanprover/lean4#2644 - homEquiv_naturality_right := by intros; dsimp; congr 1; aesop_cat - } + rfl } } #align category_theory.over.map_pullback_adj CategoryTheory.Over.mapPullbackAdj /-- pullback (𝟙 A) : over A ⥤ over A is the identity functor. -/ diff --git a/Mathlib/CategoryTheory/Limits/Presheaf.lean b/Mathlib/CategoryTheory/Limits/Presheaf.lean index deb4c3082d6ca..55eba11d794c0 100644 --- a/Mathlib/CategoryTheory/Limits/Presheaf.lean +++ b/Mathlib/CategoryTheory/Limits/Presheaf.lean @@ -459,8 +459,7 @@ def isColimitTautologicalCocone : IsColimit (tautologicalCocone P) where intros X Y f ext t dsimp - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [yonedaEquiv_naturality', yonedaEquiv_symm_map] + rw [yonedaEquiv_naturality', yonedaEquiv_symm_map] simpa using (s.ι.naturality (CostructuredArrow.homMk' (CostructuredArrow.mk (yonedaEquiv.symm t)) f.unop)).symm fac := by @@ -469,16 +468,14 @@ def isColimitTautologicalCocone : IsColimit (tautologicalCocone P) where apply yonedaEquiv.injective rw [yonedaEquiv_comp] dsimp only - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [Equiv.symm_apply_apply] + rw [Equiv.symm_apply_apply] rfl uniq := by intro s j h ext V x obtain ⟨t, rfl⟩ := yonedaEquiv.surjective x dsimp - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [Equiv.symm_apply_apply, ← yonedaEquiv_comp'] + rw [Equiv.symm_apply_apply, ← yonedaEquiv_comp'] exact congr_arg _ (h (CostructuredArrow.mk t)) end ArbitraryUniverses diff --git a/Mathlib/CategoryTheory/Monad/Algebra.lean b/Mathlib/CategoryTheory/Monad/Algebra.lean index fba647a384c94..8de366a3fd4da 100644 --- a/Mathlib/CategoryTheory/Monad/Algebra.lean +++ b/Mathlib/CategoryTheory/Monad/Algebra.lean @@ -199,14 +199,7 @@ def adj : T.free ⊣ T.forget := right_inv := fun f => by dsimp only [forget_obj] rw [← T.η.naturality_assoc, Y.unit] - apply Category.comp_id }, - -- This used to be automatic before leanprover/lean4#2644 - homEquiv_naturality_right := by - intros - -- This doesn't look good: - simp - dsimp - simp } + apply Category.comp_id } } #align category_theory.monad.adj CategoryTheory.Monad.adj /-- Given an algebra morphism whose carrier part is an isomorphism, we get an algebra isomorphism. diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean index 2a4ff22829aa8..fdb60c911a3aa 100644 --- a/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean +++ b/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean @@ -115,8 +115,7 @@ def inverseObj (A : AlgebraCat.{u} R) : Mon_ (ModuleCat.{u} R) where one_mul := by -- Porting note : `ext` did not pick up `TensorProduct.ext` refine TensorProduct.ext <| LinearMap.ext_ring <| LinearMap.ext fun x => ?_ - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [compr₂_apply, compr₂_apply, CategoryTheory.comp_apply] + rw [compr₂_apply, compr₂_apply, CategoryTheory.comp_apply] -- Porting note : this `dsimp` does nothing -- dsimp [AlgebraCat.id_apply, TensorProduct.mk_apply, Algebra.linearMap_apply, -- LinearMap.compr₂_apply, Function.comp_apply, RingHom.map_one, @@ -134,8 +133,7 @@ def inverseObj (A : AlgebraCat.{u} R) : Mon_ (ModuleCat.{u} R) where -- AlgebraCat.coe_comp] -- Porting note : because `dsimp` is not effective, `rw` needs to be changed to `erw` erw [compr₂_apply, compr₂_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [CategoryTheory.comp_apply] + rw [CategoryTheory.comp_apply] erw [LinearMap.mul'_apply, ModuleCat.MonoidalCategory.rightUnitor_hom_apply, ← Algebra.commutes, ← Algebra.smul_def] rw [id_apply] @@ -148,9 +146,7 @@ def inverseObj (A : AlgebraCat.{u} R) : Mon_ (ModuleCat.{u} R) where -- Function.comp_apply, ModuleCat.MonoidalCategory.hom_apply, AlgebraCat.coe_comp, -- MonoidalCategory.associator_hom_apply] -- Porting note : because `dsimp` is not effective, `rw` needs to be changed to `erw` - rw [compr₂_apply, compr₂_apply, compr₂_apply, compr₂_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [CategoryTheory.comp_apply, + rw [compr₂_apply, compr₂_apply, compr₂_apply, compr₂_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply] erw [LinearMap.mul'_apply, LinearMap.mul'_apply] rw [id_apply, TensorProduct.mk_apply] @@ -229,9 +225,6 @@ def monModuleEquivalenceAlgebra : Mon_ (ModuleCat.{u} R) ≌ AlgebraCat R where (by intros; rfl) #align Module.Mon_Module_equivalence_Algebra ModuleCat.monModuleEquivalenceAlgebra --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] ModuleCat.MonModuleEquivalenceAlgebra.functor_map_apply - /-- The equivalence `Mon_ (ModuleCat R) ≌ AlgebraCat R` is naturally compatible with the forgetful functors to `ModuleCat R`. -/ diff --git a/Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean b/Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean index 50e54f27e52e2..652f7bd57e5f0 100644 --- a/Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean +++ b/Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean @@ -95,10 +95,6 @@ def preadditiveCoyoneda : Cᵒᵖ ⥤ C ⥤ AddCommGroupCat.{v} where map_comp f g := by ext; dsimp; simp #align category_theory.preadditive_coyoneda CategoryTheory.preadditiveCoyoneda --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] CategoryTheory.preadditiveYoneda_map_app_apply - CategoryTheory.preadditiveCoyoneda_map_app_apply - instance additive_yonedaObj (X : C) : Functor.Additive (preadditiveYonedaObj X) where #align category_theory.additive_yoneda_obj CategoryTheory.additive_yonedaObj diff --git a/Mathlib/CategoryTheory/Sites/Adjunction.lean b/Mathlib/CategoryTheory/Sites/Adjunction.lean index b4cca1d1eddef..db6baaf90d080 100644 --- a/Mathlib/CategoryTheory/Sites/Adjunction.lean +++ b/Mathlib/CategoryTheory/Sites/Adjunction.lean @@ -76,15 +76,10 @@ def composeEquiv (adj : G ⊣ F) (X : Sheaf J E) (Y : Sheaf J D) : intro γ ext1 dsimp - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [J.toSheafify_sheafifyLift, Equiv.apply_symm_apply] } + rw [J.toSheafify_sheafifyLift, Equiv.apply_symm_apply] } set_option linter.uppercaseLean3 false in #align category_theory.Sheaf.compose_equiv CategoryTheory.Sheaf.composeEquiv --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] CategoryTheory.Sheaf.composeEquiv_apply_val - CategoryTheory.Sheaf.composeEquiv_symm_apply_val - /-- An adjunction `adj : G ⊣ F` with `F : D ⥤ E` and `G : E ⥤ D` induces an adjunction between `Sheaf J D` and `Sheaf J E`, in contexts where one can sheafify `D`-valued presheaves, and `F` preserves the correct limits. -/ diff --git a/Mathlib/CategoryTheory/Sites/Sheaf.lean b/Mathlib/CategoryTheory/Sites/Sheaf.lean index 4d74aeb5e8f58..34168550a2fff 100644 --- a/Mathlib/CategoryTheory/Sites/Sheaf.lean +++ b/Mathlib/CategoryTheory/Sites/Sheaf.lean @@ -107,10 +107,6 @@ def conesEquivSieveCompatibleFamily : right_inv x := rfl #align category_theory.presheaf.cones_equiv_sieve_compatible_family CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily_apply_coe - CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily_symm_apply_app - variable {P S E} {x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows} (hx : SieveCompatible x) /-- The cone corresponding to a sieve_compatible family of elements, dot notation enabled. -/ diff --git a/Mathlib/CategoryTheory/Subobject/Comma.lean b/Mathlib/CategoryTheory/Subobject/Comma.lean index f135acf6e2b5d..5b054bda3782f 100644 --- a/Mathlib/CategoryTheory/Subobject/Comma.lean +++ b/Mathlib/CategoryTheory/Subobject/Comma.lean @@ -114,10 +114,6 @@ def subobjectEquiv [HasLimits C] [PreservesLimits T] (A : StructuredArrow S T) : exact congr_arg CommaMorphism.right (Subobject.ofMkLEMk_comp h) #align category_theory.structured_arrow.subobject_equiv CategoryTheory.StructuredArrow.subobjectEquiv --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] CategoryTheory.StructuredArrow.subobjectEquiv_symm_apply - CategoryTheory.StructuredArrow.subobjectEquiv_apply_coe - /-- If `C` is well-powered and complete and `T` preserves limits, then `StructuredArrow S T` is well-powered. -/ instance wellPowered_structuredArrow [WellPowered C] [HasLimits C] [PreservesLimits T] : diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean index 8b7fe98e0e6e0..0edf01903304a 100644 --- a/Mathlib/CategoryTheory/Yoneda.lean +++ b/Mathlib/CategoryTheory/Yoneda.lean @@ -429,8 +429,7 @@ lemma yonedaEquiv_comp' {X : Cᵒᵖ} {F G : Cᵒᵖ ⥤ Type v₁} (α : yoneda yonedaEquiv (α ≫ β) = β.app X (yonedaEquiv α) := rfl --- This lemma has always been bad, but leanprover/lean4#2644 made `simp` start noticing -@[simp, nolint simpNF] +@[simp] lemma yonedaEquiv_yoneda_map {X Y : C} (f : X ⟶ Y) : yonedaEquiv (yoneda.map f) = f := by rw [yonedaEquiv_apply] simp diff --git a/Mathlib/Combinatorics/Quiver/Covering.lean b/Mathlib/Combinatorics/Quiver/Covering.lean index 5bfe7069fd6b4..701b5aae1e526 100644 --- a/Mathlib/Combinatorics/Quiver/Covering.lean +++ b/Mathlib/Combinatorics/Quiver/Covering.lean @@ -158,8 +158,7 @@ theorem Prefunctor.symmetrifyStar (u : U) : φ.symmetrify.star u = (Quiver.symmetrifyStar _).symm ∘ Sum.map (φ.star u) (φ.costar u) ∘ Quiver.symmetrifyStar u := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [Equiv.eq_symm_comp] + rw [Equiv.eq_symm_comp] ext ⟨v, f | g⟩ <;> -- Porting note: was `simp [Quiver.symmetrifyStar]` simp only [Quiver.symmetrifyStar, Function.comp_apply] <;> @@ -171,8 +170,7 @@ protected theorem Prefunctor.symmetrifyCostar (u : U) : φ.symmetrify.costar u = (Quiver.symmetrifyCostar _).symm ∘ Sum.map (φ.costar u) (φ.star u) ∘ Quiver.symmetrifyCostar u := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [Equiv.eq_symm_comp] + rw [Equiv.eq_symm_comp] ext ⟨v, f | g⟩ <;> -- Porting note: was `simp [Quiver.symmetrifyCostar]` simp only [Quiver.symmetrifyCostar, Function.comp_apply] <;> @@ -185,8 +183,8 @@ protected theorem Prefunctor.IsCovering.symmetrify (hφ : φ.IsCovering) : refine' ⟨fun u => _, fun u => _⟩ <;> -- Porting note: was -- simp [φ.symmetrifyStar, φ.symmetrifyCostar, hφ.star_bijective u, hφ.costar_bijective u] - simp only [φ.symmetrifyStar, φ.symmetrifyCostar] <;> - erw [EquivLike.comp_bijective, EquivLike.bijective_comp] <;> + simp only [φ.symmetrifyStar, φ.symmetrifyCostar, EquivLike.comp_bijective] <;> + erw [EquivLike.bijective_comp] <;> simp [hφ.star_bijective u, hφ.costar_bijective u] #align prefunctor.is_covering.symmetrify Prefunctor.IsCovering.symmetrify diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean index 9f3142135f53b..e6ffd41157830 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Clique.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Clique.lean @@ -175,9 +175,6 @@ theorem not_cliqueFree_of_top_embedding {n : ℕ} (f : (⊤ : SimpleGraph (Fin n obtain ⟨w', rfl⟩ := hw simp only [coe_sort_coe, RelEmbedding.coe_toEmbedding, comap_Adj, Function.Embedding.coe_subtype, f.map_adj_iff, top_adj, ne_eq, Subtype.mk.injEq, RelEmbedding.inj] - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [Function.Embedding.coe_subtype, f.map_adj_iff] - simp #align simple_graph.not_clique_free_of_top_embedding SimpleGraph.not_cliqueFree_of_top_embedding /-- An embedding of a complete graph that witnesses the fact that the graph is not clique-free. -/ diff --git a/Mathlib/Control/Fold.lean b/Mathlib/Control/Fold.lean index e30d6b1ab5f57..c22ce5bfa25e1 100644 --- a/Mathlib/Control/Fold.lean +++ b/Mathlib/Control/Fold.lean @@ -319,7 +319,6 @@ theorem foldlm.ofFreeMonoid_comp_of {m} [Monad m] [LawfulMonad m] (f : α → β foldlM.ofFreeMonoid f ∘ FreeMonoid.of = foldlM.mk ∘ flip f := by ext1 x simp [(· ∘ ·), foldlM.ofFreeMonoid, foldlM.mk, flip] - rfl #align traversable.mfoldl.of_free_monoid_comp_of Traversable.foldlm.ofFreeMonoid_comp_of @[simp] diff --git a/Mathlib/Data/Matrix/Reflection.lean b/Mathlib/Data/Matrix/Reflection.lean index 24e37c30ed5e0..c3e362e20aeea 100644 --- a/Mathlib/Data/Matrix/Reflection.lean +++ b/Mathlib/Data/Matrix/Reflection.lean @@ -230,9 +230,7 @@ example (A : Matrix (Fin 2) (Fin 2) α) : ``` -/ theorem etaExpand_eq {m n} (A : Matrix (Fin m) (Fin n) α) : etaExpand A = A := by - simp_rw [etaExpand, FinVec.etaExpand_eq, Matrix.of] - -- This to be in the above `simp_rw` before leanprover/lean4#2644 - erw [Equiv.refl_apply] + simp_rw [etaExpand, FinVec.etaExpand_eq, Matrix.of, Equiv.refl_apply] #align matrix.eta_expand_eq Matrix.etaExpand_eq example (A : Matrix (Fin 2) (Fin 2) α) : A = !![A 0 0, A 0 1; A 1 0, A 1 1] := diff --git a/Mathlib/Data/MvPolynomial/Rename.lean b/Mathlib/Data/MvPolynomial/Rename.lean index e978c9dabbc4d..d16ddf46015ca 100644 --- a/Mathlib/Data/MvPolynomial/Rename.lean +++ b/Mathlib/Data/MvPolynomial/Rename.lean @@ -260,11 +260,9 @@ theorem exists_finset_rename₂ (p₁ p₂ : MvPolynomial σ R) : use rename (Set.inclusion <| s₁.subset_union_left s₂) q₁ use rename (Set.inclusion <| s₁.subset_union_right s₂) q₂ constructor -- porting note: was `<;> simp <;> rfl` but Lean couldn't infer the arguments - · -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [rename_rename (Set.inclusion <| s₁.subset_union_left s₂)] + · rw [rename_rename (Set.inclusion <| s₁.subset_union_left s₂)] rfl - · -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [rename_rename (Set.inclusion <| s₁.subset_union_right s₂)] + · rw [rename_rename (Set.inclusion <| s₁.subset_union_right s₂)] rfl #align mv_polynomial.exists_finset_rename₂ MvPolynomial.exists_finset_rename₂ diff --git a/Mathlib/FieldTheory/AbelRuffini.lean b/Mathlib/FieldTheory/AbelRuffini.lean index 06e87f0bf8535..967e8afc11c59 100644 --- a/Mathlib/FieldTheory/AbelRuffini.lean +++ b/Mathlib/FieldTheory/AbelRuffini.lean @@ -363,9 +363,7 @@ theorem induction2 {α β γ : solvableByRad F E} (hγ : γ ∈ F⟮α, β⟯) ( simp only [map_zero, _root_.map_eq_zero] -- Porting note: end of the proof was `exact minpoly.aeval F γ`. apply Subtype.val_injective - -- This used to be `simp`, but we need `erw` and `simp` after leanprover/lean4#2644 - erw [Polynomial.aeval_subalgebra_coe (minpoly F γ)] - simp + simp [Polynomial.aeval_subalgebra_coe (minpoly F γ)] rw [P, key] refine' gal_isSolvable_of_splits ⟨Normal.splits _ (f ⟨γ, hγ⟩)⟩ (gal_mul_isSolvable hα hβ) apply SplittingField.instNormal diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean index d9b118c78b134..dd89da22da0c4 100644 --- a/Mathlib/FieldTheory/Adjoin.lean +++ b/Mathlib/FieldTheory/Adjoin.lean @@ -829,12 +829,10 @@ noncomputable def adjoinRootEquivAdjoin (h : IsIntegral F α) : refine' Subfield.closure_le.mpr (Set.union_subset (fun x hx => _) _) · obtain ⟨y, hy⟩ := hx refine' ⟨y, _⟩ - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [RingHom.comp_apply, AdjoinRoot.lift_of (aeval_gen_minpoly F α)] + rw [RingHom.comp_apply, AdjoinRoot.lift_of (aeval_gen_minpoly F α)] exact hy · refine' Set.singleton_subset_iff.mpr ⟨AdjoinRoot.root (minpoly F α), _⟩ - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [RingHom.comp_apply, AdjoinRoot.lift_root (aeval_gen_minpoly F α)] + rw [RingHom.comp_apply, AdjoinRoot.lift_root (aeval_gen_minpoly F α)] rfl) #align intermediate_field.adjoin_root_equiv_adjoin IntermediateField.adjoinRootEquivAdjoin @@ -862,8 +860,7 @@ noncomputable def adjoin.powerBasis {x : L} (hx : IsIntegral K x) : PowerBasis K dim := (minpoly K x).natDegree basis := powerBasisAux hx basis_eq_pow i := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [powerBasisAux, Basis.map_apply, PowerBasis.basis_eq_pow, AlgEquiv.toLinearEquiv_apply, + rw [powerBasisAux, Basis.map_apply, PowerBasis.basis_eq_pow, AlgEquiv.toLinearEquiv_apply, AlgEquiv.map_pow, AdjoinRoot.powerBasis_gen, adjoinRootEquivAdjoin_apply_root] #align intermediate_field.adjoin.power_basis IntermediateField.adjoin.powerBasis diff --git a/Mathlib/FieldTheory/IntermediateField.lean b/Mathlib/FieldTheory/IntermediateField.lean index abcfccec06d2b..4cb3045cf00e6 100644 --- a/Mathlib/FieldTheory/IntermediateField.lean +++ b/Mathlib/FieldTheory/IntermediateField.lean @@ -436,15 +436,13 @@ def intermediateFieldMap (e : L ≃ₐ[K] L') (E : IntermediateField K L) : E /- We manually add these two simp lemmas because `@[simps]` before `intermediate_field_map` led to a timeout. -/ --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[simp, nolint simpNF] +@[simp] theorem intermediateFieldMap_apply_coe (e : L ≃ₐ[K] L') (E : IntermediateField K L) (a : E) : ↑(intermediateFieldMap e E a) = e a := rfl #align intermediate_field.intermediate_field_map_apply_coe IntermediateField.intermediateFieldMap_apply_coe --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[simp, nolint simpNF] +@[simp] theorem intermediateFieldMap_symm_apply_coe (e : L ≃ₐ[K] L') (E : IntermediateField K L) (a : E.map e.toAlgHom) : ↑((intermediateFieldMap e E).symm a) = e.symm a := rfl diff --git a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean index e78cfb4934d3c..a5e508c67d692 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean @@ -151,8 +151,7 @@ theorem AdjoinMonic.isIntegral (z : AdjoinMonic k) : IsIntegral k z := by theorem AdjoinMonic.exists_root {f : k[X]} (hfm : f.Monic) (hfi : Irreducible f) : ∃ x : AdjoinMonic k, f.eval₂ (toAdjoinMonic k) x = 0 := ⟨Ideal.Quotient.mk _ <| X (⟨f, hfm, hfi⟩ : MonicIrreducible k), by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [toAdjoinMonic, ← hom_eval₂, Ideal.Quotient.eq_zero_iff_mem] + rw [toAdjoinMonic, ← hom_eval₂, Ideal.Quotient.eq_zero_iff_mem] exact le_maxIdeal k (Ideal.subset_span <| ⟨_, rfl⟩)⟩ #align algebraic_closure.adjoin_monic.exists_root AlgebraicClosure.AdjoinMonic.exists_root diff --git a/Mathlib/FieldTheory/SplittingField/Construction.lean b/Mathlib/FieldTheory/SplittingField/Construction.lean index 72269157add18..56f3aa2437e21 100644 --- a/Mathlib/FieldTheory/SplittingField/Construction.lean +++ b/Mathlib/FieldTheory/SplittingField/Construction.lean @@ -202,8 +202,7 @@ theorem adjoin_rootSet (n : ℕ) : have hmf0 : map (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0 := map_ne_zero hfn0 rw [rootSet_def, aroots_def] rw [algebraMap_succ, ←map_map, ←X_sub_C_mul_removeFactor _ hndf, Polynomial.map_mul] at hmf0 ⊢ - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [roots_mul hmf0, Polynomial.map_sub, map_X, map_C, roots_X_sub_C, Multiset.toFinset_add, + rw [roots_mul hmf0, Polynomial.map_sub, map_X, map_C, roots_X_sub_C, Multiset.toFinset_add, Finset.coe_union, Multiset.toFinset_singleton, Finset.coe_singleton, Algebra.adjoin_union_eq_adjoin_adjoin, ← Set.image_singleton, Algebra.adjoin_algebraMap K (SplittingFieldAux n f.removeFactor), diff --git a/Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean b/Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean index 4aef737c883f1..555afeac294cc 100644 --- a/Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean +++ b/Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean @@ -251,8 +251,7 @@ theorem evalAt_mul : evalAt (g * h) X = 𝒅ₕ (L_apply I g h) (evalAt h X) := apply_fdifferential] -- Porting note: more agressive here erw [LinearMap.comp_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [apply_fdifferential, ← apply_hfdifferential, left_invariant] + rw [apply_fdifferential, ← apply_hfdifferential, left_invariant] #align left_invariant_derivation.eval_at_mul LeftInvariantDerivation.evalAt_mul theorem comp_L : (X f).comp (𝑳 I g) = X (f.comp (𝑳 I g)) := by diff --git a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean index 44477b6d96ce0..a2aecb6c2fd72 100644 --- a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean +++ b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean @@ -328,7 +328,6 @@ theorem ContMDiffOn.contMDiffOn_tangentMapWithin_aux {f : H → H'} {s : Set H} refine C.congr fun p hp => ?_ simp only [mfld_simps] at hp simp only [mfderivWithin, hf.mdifferentiableOn one_le_n _ hp.2, hp.1, if_pos, mfld_simps] - rfl have D : ContDiffOn 𝕜 m (fun x => fderivWithin 𝕜 (I' ∘ f ∘ I.symm) (I.symm ⁻¹' s ∩ range I) x) (range I ∩ I.symm ⁻¹' s) := by diff --git a/Mathlib/Geometry/Manifold/MFDeriv.lean b/Mathlib/Geometry/Manifold/MFDeriv.lean index a8b7558207449..3bdb3618fa746 100644 --- a/Mathlib/Geometry/Manifold/MFDeriv.lean +++ b/Mathlib/Geometry/Manifold/MFDeriv.lean @@ -901,8 +901,7 @@ theorem tangentMapWithin_congr (h : ∀ x ∈ s, f x = f₁ x) (p : TangentBundl (hs : UniqueMDiffWithinAt I s p.1) : tangentMapWithin I I' f s p = tangentMapWithin I I' f₁ s p := by refine TotalSpace.ext _ _ (h p.1 hp) ?_ - -- This used to be `simp only`, but we need `erw` after leanprover/lean4#2644 - rw [tangentMapWithin, h p.1 hp, tangentMapWithin, mfderivWithin_congr hs h (h _ hp)] + simp only [tangentMapWithin, h p.1 hp, mfderivWithin_congr hs h (h _ hp), HEq.refl] #align tangent_map_within_congr tangentMapWithin_congr theorem Filter.EventuallyEq.mfderiv_eq (hL : f₁ =ᶠ[𝓝 x] f) : diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean index 9bc2b4f1470c1..a9019797d531d 100644 --- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean +++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean @@ -195,10 +195,8 @@ 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 => ?_⟩ rw [←comp_apply, ←comp_base, D.t_inv, id_base, id_apply] diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean index 13de784ede750..c0950949ca21d 100644 --- a/Mathlib/GroupTheory/Complement.lean +++ b/Mathlib/GroupTheory/Complement.lean @@ -363,11 +363,9 @@ theorem equiv_fst_eq_iff_leftCosetEquivalence {g₁ g₂ : G} : exact Subtype.property _ · intro h apply (mem_leftTransversals_iff_existsUnique_inv_mul_mem.1 hSK g₁).unique - · -- This used to be `simp [...]` before leanprover/lean4#2644 - rw [equiv_fst_eq_mul_inv]; simp + · simp [equiv_fst_eq_mul_inv] · rw [SetLike.mem_coe, ← mul_mem_cancel_right h] - -- This used to be `simp [...]` before leanprover/lean4#2644 - rw [equiv_fst_eq_mul_inv]; simp [equiv_fst_eq_mul_inv, ← mul_assoc] + simp [equiv_fst_eq_mul_inv, ← mul_assoc] theorem equiv_snd_eq_iff_rightCosetEquivalence {g₁ g₂ : G} : (hHT.equiv g₁).snd = (hHT.equiv g₂).snd ↔ RightCosetEquivalence H g₁ g₂ := by @@ -379,21 +377,17 @@ theorem equiv_snd_eq_iff_rightCosetEquivalence {g₁ g₂ : G} : exact Subtype.property _ · intro h apply (mem_rightTransversals_iff_existsUnique_mul_inv_mem.1 hHT g₁).unique - · -- This used to be `simp [...]` before leanprover/lean4#2644 - rw [equiv_snd_eq_inv_mul]; simp + · simp [equiv_snd_eq_inv_mul] · rw [SetLike.mem_coe, ← mul_mem_cancel_left h] - -- This used to be `simp [...]` before leanprover/lean4#2644 - rw [equiv_snd_eq_inv_mul, mul_assoc]; simp + simp [equiv_snd_eq_inv_mul, mul_assoc] theorem leftCosetEquivalence_equiv_fst (g : G) : LeftCosetEquivalence K g ((hSK.equiv g).fst : G) := by - -- This used to be `simp [...]` before leanprover/lean4#2644 - rw [equiv_fst_eq_mul_inv]; simp [LeftCosetEquivalence, leftCoset_eq_iff] + simp [LeftCosetEquivalence, leftCoset_eq_iff, equiv_fst_eq_mul_inv] theorem rightCosetEquivalence_equiv_snd (g : G) : RightCosetEquivalence H g ((hHT.equiv g).snd : G) := by - -- This used to be `simp [...]` before leanprover/lean4#2644 - rw [RightCosetEquivalence, rightCoset_eq_iff, equiv_snd_eq_inv_mul]; simp + simp [RightCosetEquivalence, rightCoset_eq_iff, equiv_snd_eq_inv_mul] theorem equiv_fst_eq_self_of_mem_of_one_mem {g : G} (h1 : 1 ∈ T) (hg : g ∈ S) : (hST.equiv g).fst = ⟨g, hg⟩ := by @@ -417,8 +411,7 @@ theorem equiv_fst_eq_one_of_mem_of_one_mem {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) ext rw [equiv_fst_eq_mul_inv, equiv_snd_eq_self_of_mem_of_one_mem _ h1 hg, mul_inv_self] --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[simp, nolint simpNF] +@[simp] theorem equiv_mul_right (g : G) (k : K) : hSK.equiv (g * k) = ((hSK.equiv g).fst, (hSK.equiv g).snd * k) := by have : (hSK.equiv (g * k)).fst = (hSK.equiv g).fst := @@ -432,8 +425,7 @@ theorem equiv_mul_right_of_mem {g k : G} (h : k ∈ K) : hSK.equiv (g * k) = ((hSK.equiv g).fst, (hSK.equiv g).snd * ⟨k, h⟩) := equiv_mul_right _ g ⟨k, h⟩ --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[simp, nolint simpNF] +@[simp] theorem equiv_mul_left (h : H) (g : G) : hHT.equiv (h * g) = (h * (hHT.equiv g).fst, (hHT.equiv g).snd) := by have : (hHT.equiv (h * g)).snd = (hHT.equiv g).snd := diff --git a/Mathlib/GroupTheory/CoprodI.lean b/Mathlib/GroupTheory/CoprodI.lean index ac75b3951fe14..319192fe4b843 100644 --- a/Mathlib/GroupTheory/CoprodI.lean +++ b/Mathlib/GroupTheory/CoprodI.lean @@ -140,9 +140,8 @@ variable {N : Type*} [Monoid N] theorem ext_hom (f g : CoprodI M →* N) (h : ∀ i, f.comp (of : M i →* _) = g.comp of) : f = g := (MonoidHom.cancel_right Con.mk'_surjective).mp <| FreeMonoid.hom_eq fun ⟨i, x⟩ => by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidHom.comp_apply, MonoidHom.comp_apply, ← of_apply, ← MonoidHom.comp_apply, ← - MonoidHom.comp_apply, h]; rfl + rw [MonoidHom.comp_apply, MonoidHom.comp_apply, ← of_apply, ← MonoidHom.comp_apply, ← + MonoidHom.comp_apply, h] #align free_product.ext_hom Monoid.CoprodI.ext_hom /-- A map out of the free product corresponds to a family of maps out of the summands. This is the @@ -164,8 +163,7 @@ def lift : (∀ i, M i →* N) ≃ (CoprodI M →* N) where left_inv := by intro fi ext i x - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidHom.comp_apply, of_apply, Con.lift_mk', FreeMonoid.lift_eval_of] + rw [MonoidHom.comp_apply, of_apply, Con.lift_mk', FreeMonoid.lift_eval_of] right_inv := by intro f ext i x diff --git a/Mathlib/GroupTheory/HNNExtension.lean b/Mathlib/GroupTheory/HNNExtension.lean index 8446973475287..762088c7e5cbc 100644 --- a/Mathlib/GroupTheory/HNNExtension.lean +++ b/Mathlib/GroupTheory/HNNExtension.lean @@ -164,8 +164,7 @@ theorem toSubgroupEquiv_neg_one : toSubgroupEquiv φ (-1) = φ.symm := rfl theorem toSubgroupEquiv_neg_apply (u : ℤˣ) (a : toSubgroup A B u) : (toSubgroupEquiv φ (-u) (toSubgroupEquiv φ u a) : G) = a := by rcases Int.units_eq_one_or u with rfl | rfl - · -- This used to be `simp` before leanprover/lean4#2644 - simp; erw [MulEquiv.symm_apply_apply] + · simp · simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, SetLike.coe_eq_coe] exact φ.apply_symm_apply a @@ -422,9 +421,6 @@ theorem unitsSMul_neg (u : ℤˣ) (w : NormalWord d) : unfold unitsSMul simp only [dif_neg hncan] simp [unitsSMulWithCancel, unitsSMulGroup, (d.compl u).equiv_snd_eq_inv_mul] - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [(d.compl u).equiv_snd_eq_inv_mul] - simp · have hcan2 : Cancels u w := not_not.1 (mt (unitsSMul_cancels_iff _ _ _).2 hcan) unfold unitsSMul at hcan ⊢ simp only [dif_pos hcan2] at hcan ⊢ @@ -437,18 +433,8 @@ theorem unitsSMul_neg (u : ℤˣ) (w : NormalWord d) : have : ((d.compl (-u)).equiv w.head).1 = 1 := (d.compl (-u)).equiv_fst_eq_one_of_mem_of_one_mem _ h1 apply NormalWord.ext - · -- This used to `simp [this]` before leanprover/lean4#2644 - dsimp - conv_lhs => erw [IsComplement.equiv_mul_left] - rw [map_mul, Submonoid.coe_mul, toSubgroupEquiv_neg_apply, this] - simp - · -- The next two lines were not needed before leanprover/lean4#2644 - dsimp - conv_lhs => erw [IsComplement.equiv_mul_left] - simp [mul_assoc, Units.ext_iff, (d.compl (-u)).equiv_snd_eq_inv_mul, this] - -- The next two lines were not needed before leanprover/lean4#2644 - erw [(d.compl (-u)).equiv_snd_eq_inv_mul, this] - simp + · simp [this] + · simp [mul_assoc, Units.ext_iff, (d.compl (-u)).equiv_snd_eq_inv_mul, this] /-- the equivalence given by multiplication on the left by `t` -/ @[simps] @@ -472,12 +458,6 @@ theorem unitsSMul_one_group_smul (g : A) (w : NormalWord d) : rfl · rw [dif_neg (mt this.1 hcan), dif_neg hcan] simp [← mul_smul, mul_assoc, unitsSMulGroup] - -- This used to be the end of the proof before leanprover/lean4#2644 - dsimp - congr 1 - conv_lhs => erw [IsComplement.equiv_mul_left] - simp - conv_lhs => erw [IsComplement.equiv_mul_left] noncomputable instance : MulAction (HNNExtension G A B φ) (NormalWord d) := MulAction.ofEndHom <| (MulAction.toEndHom (M := Equiv.Perm (NormalWord d))).comp @@ -522,19 +502,10 @@ theorem prod_unitsSMul (u : ℤˣ) (w : NormalWord d) : rcases Int.units_eq_one_or u with (rfl | rfl) · simp [equiv_eq_conj, mul_assoc] · simp [equiv_symm_eq_conj, mul_assoc] - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [equiv_symm_eq_conj] - simp [equiv_symm_eq_conj, mul_assoc] · simp [unitsSMulGroup] rcases Int.units_eq_one_or u with (rfl | rfl) · simp [equiv_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul] - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [(d.compl _).equiv_snd_eq_inv_mul] - simp [equiv_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul] · simp [equiv_symm_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul] - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [equiv_symm_eq_conj, (d.compl _).equiv_snd_eq_inv_mul] - simp [equiv_symm_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul] @[simp] theorem prod_empty : (empty : NormalWord d).prod φ = 1 := by @@ -560,16 +531,9 @@ theorem prod_smul_empty (w : NormalWord d) : rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul, of_smul_eq_smul, unitsSMul] rw [dif_neg (not_cancels_of_cons_hyp u w h2)] - -- The next 3 lines were a single `simp [...]` before leanprover/lean4#2644 - simp only [unitsSMulGroup] - simp_rw [SetLike.coe_sort_coe] - erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1] + simp [unitsSMulGroup, (d.compl u).equiv_snd_eq_inv_mul, mul_assoc, + (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1] ext <;> simp - -- The next 4 were not needed before leanprover/lean4#2644 - · erw [(d.compl _).equiv_snd_eq_inv_mul] - simp_rw [SetLike.coe_sort_coe] - erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1] - simp variable (d) /-- The equivalence between elements of the HNN extension and words in normal form. -/ diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean index 1ef45de91fc62..09683079c500f 100644 --- a/Mathlib/GroupTheory/OrderOfElement.lean +++ b/Mathlib/GroupTheory/OrderOfElement.lean @@ -749,16 +749,14 @@ noncomputable def finEquivPowers [Finite G] (x : G) : #align fin_equiv_powers finEquivPowers #align fin_equiv_multiples finEquivMultiples --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[to_additive (attr := simp, nolint simpNF) finEquivMultiples_apply] +@[to_additive (attr := simp) finEquivMultiples_apply] theorem finEquivPowers_apply [Finite G] {x : G} {n : Fin (orderOf x)} : finEquivPowers x n = ⟨x ^ (n : ℕ), n, rfl⟩ := rfl #align fin_equiv_powers_apply finEquivPowers_apply #align fin_equiv_multiples_apply finEquivMultiples_apply --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[to_additive (attr := simp, nolint simpNF) finEquivMultiples_symm_apply] +@[to_additive (attr := simp) finEquivMultiples_symm_apply] theorem finEquivPowers_symm_apply [Finite G] (x : G) (n : ℕ) {hn : ∃ m : ℕ, x ^ m = x ^ n} : (finEquivPowers x).symm ⟨x ^ n, hn⟩ = ⟨n % orderOf x, Nat.mod_lt _ (orderOf_pos x)⟩ := by rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, pow_eq_mod_orderOf, Fin.val_mk] @@ -879,16 +877,14 @@ noncomputable def finEquivZpowers [Finite G] (x : G) : #align fin_equiv_zpowers finEquivZpowers #align fin_equiv_zmultiples finEquivZmultiples --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[to_additive (attr := simp, nolint simpNF) finEquivZmultiples_apply] +@[to_additive (attr := simp) finEquivZmultiples_apply] theorem finEquivZpowers_apply [Finite G] {n : Fin (orderOf x)} : finEquivZpowers x n = ⟨x ^ (n : ℕ), n, zpow_ofNat x n⟩ := rfl #align fin_equiv_zpowers_apply finEquivZpowers_apply #align fin_equiv_zmultiples_apply finEquivZmultiples_apply --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[to_additive (attr := simp, nolint simpNF) finEquivZmultiples_symm_apply] +@[to_additive (attr := simp) finEquivZmultiples_symm_apply] theorem finEquivZpowers_symm_apply [Finite G] (x : G) (n : ℕ) {hn : ∃ m : ℤ, x ^ m = x ^ n} : (finEquivZpowers x).symm ⟨x ^ n, hn⟩ = ⟨n % orderOf x, Nat.mod_lt _ (orderOf_pos x)⟩ := by rw [finEquivZpowers, Equiv.symm_trans_apply] diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean index 8bcf5f3ecf5ee..2a4a6dfb4a0a2 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean @@ -870,9 +870,6 @@ theorem IsCycleOn.pow_apply_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ (hf.isCycle_subtypePerm hs).pow_eq_one_iff' (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)] simp - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [subtypePerm_apply] - simp #align equiv.perm.is_cycle_on.pow_apply_eq Equiv.Perm.IsCycleOn.pow_apply_eq theorem IsCycleOn.zpow_apply_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) : @@ -1739,11 +1736,10 @@ theorem IsCycle.isConj (hσ : IsCycle σ) (hτ : IsCycle τ) (h : σ.support.car Eq.trans _ (congr rfl (congr rfl (congr rfl (congr rfl (hσ.zpowersEquivSupport_symm_apply n).symm)))) apply (congr rfl (congr rfl (congr rfl (hσ.zpowersEquivSupport_symm_apply (n + 1))))).trans _ - -- This used to be a `simp only` before leanprover/lean4#2644 - erw [zpowersEquivZpowers_apply, zpowersEquivZpowers_apply] + simp only [Ne.def, IsCycle.zpowersEquivSupport_apply, Subtype.coe_mk, + zpowersEquivZpowers_apply] dsimp - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [pow_succ, Perm.mul_apply] + rw [pow_succ, Perm.mul_apply] #align equiv.perm.is_cycle.is_conj Equiv.Perm.IsCycle.isConj theorem IsCycle.isConj_iff (hσ : IsCycle σ) (hτ : IsCycle τ) : diff --git a/Mathlib/GroupTheory/Perm/Sign.lean b/Mathlib/GroupTheory/Perm/Sign.lean index 3f978f28abe58..bd849bee13872 100644 --- a/Mathlib/GroupTheory/Perm/Sign.lean +++ b/Mathlib/GroupTheory/Perm/Sign.lean @@ -160,9 +160,7 @@ theorem mem_sumCongrHom_range_of_perm_mapsTo_inl {m n : Type*} [Finite m] [Finit cases' x with a b · rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm, apply_ofInjective_symm Sum.inl_injective] - rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [subtypePerm_apply] + rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk, subtypePerm_apply] · rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm, apply_ofInjective_symm Sum.inr_injective] erw [subtypePerm_apply] diff --git a/Mathlib/Lean/Expr/Basic.lean b/Mathlib/Lean/Expr/Basic.lean index 204d1d9b95819..865a92233df8f 100644 --- a/Mathlib/Lean/Expr/Basic.lean +++ b/Mathlib/Lean/Expr/Basic.lean @@ -115,6 +115,17 @@ def isBlackListed {m} [Monad m] [MonadEnv m] (declName : Name) : m Bool := do end Name +namespace NameSet + +/-- The union of two `NameSet`s. -/ +def append (s t : NameSet) : NameSet := + s.mergeBy (fun _ _ _ => .unit) t + +instance : Append NameSet where + append := NameSet.append + +end NameSet + namespace ConstantInfo /-- Checks whether this `ConstantInfo` is a definition, -/ @@ -194,6 +205,10 @@ def bvarIdx? : Expr → Option Nat def getAppFnArgs (e : Expr) : Name × Array Expr := withApp e λ e a => (e.constName, a) +/-- Like `Expr.getUsedConstants`, but produce a `NameSet`. -/ +def getUsedConstants' (e : Expr) : NameSet := + e.foldConsts {} fun c cs => cs.insert c + /-- Turn an expression that is a natural number literal into a natural number. -/ def natLit! : Expr → Nat | lit (Literal.natVal v) => v @@ -471,6 +486,13 @@ def rewriteType (e eq : Expr) : MetaM Expr := do end Expr +/-- Return all names appearing in the type or value of a `ConstantInfo`. -/ +def ConstantInfo.getUsedConstants (c : ConstantInfo) : NameSet := + let tc := c.type.getUsedConstants' + match c.value? with + | none => tc + | some v => tc ++ v.getUsedConstants' + /-- Get the projections that are projections to parent structures. Similar to `getParentStructures`, except that this returns the (last component of the) projection names instead of the parent names. -/ @@ -498,7 +520,7 @@ def Name.requiredModules (n : Name) : CoreM NameSet := do let env ← getEnv let mut requiredModules : NameSet := {} let ci ← getConstInfo n - for n in ci.getUsedConstantsAsSet do + for n in ci.getUsedConstants do match env.getModuleFor? n with | some m => if ¬ (`Init).isPrefixOf m then @@ -516,7 +538,7 @@ def Environment.requiredModules (env : Environment) : NameSet := Id.run do let localConstantInfos := env.constants.map₂ let mut requiredModules : NameSet := {} for (_, ci) in localConstantInfos do - for n in ci.getUsedConstantsAsSet do + for n in ci.getUsedConstants do match env.getModuleFor? n with | some m => if ¬ (`Init).isPrefixOf m then diff --git a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean index 3b32e603f4928..7fbbf1a6fc131 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean @@ -402,8 +402,7 @@ theorem AffineEquiv.affineIndependent_iff {p : ι → P} (e : P ≃ᵃ[k] P₂) theorem AffineEquiv.affineIndependent_set_of_eq_iff {s : Set P} (e : P ≃ᵃ[k] P₂) : AffineIndependent k ((↑) : e '' s → P₂) ↔ AffineIndependent k ((↑) : s → P) := by have : e ∘ ((↑) : s → P) = ((↑) : e '' s → P₂) ∘ (e : P ≃ P₂).image s := rfl - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← e.affineIndependent_iff, this, affineIndependent_equiv] + rw [← e.affineIndependent_iff, this, affineIndependent_equiv] #align affine_equiv.affine_independent_set_of_eq_iff AffineEquiv.affineIndependent_set_of_eq_iff end Composition diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean index 813ad22b15c42..b9f148c68103f 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean @@ -410,10 +410,8 @@ protected def equiv : CliffordAlgebra (0 : QuadraticForm R R) ≃ₐ[R] R[ε] := AlgEquiv.ofAlgHom (CliffordAlgebra.lift (0 : QuadraticForm R R) ⟨inrHom R _, fun m => inr_mul_inr _ m m⟩) (DualNumber.lift ⟨ι (R := R) _ 1, ι_mul_ι (1 : R) 1⟩) - -- This used to be a single `simp` before leanprover/lean4#2644 - (by ext : 1; simp; erw [lift_ι_apply]; simp) - -- This used to be a single `simp` before leanprover/lean4#2644 - (by ext : 2; simp; erw [lift_ι_apply]; simp) + (by ext : 1; simp) + (by ext : 2; simp) #align clifford_algebra_dual_number.equiv CliffordAlgebraDualNumber.equiv @[simp] diff --git a/Mathlib/LinearAlgebra/DFinsupp.lean b/Mathlib/LinearAlgebra/DFinsupp.lean index d61b12907a3ed..bb2d862ec22a6 100644 --- a/Mathlib/LinearAlgebra/DFinsupp.lean +++ b/Mathlib/LinearAlgebra/DFinsupp.lean @@ -81,8 +81,7 @@ def lapply (i : ι) : (Π₀ i, M i) →ₗ[R] M i where map_smul' c f := smul_apply c f i #align dfinsupp.lapply DFinsupp.lapply --- This lemma has always been bad, but the linter only noticed after lean4#2644. -@[simp, nolint simpNF] +@[simp] theorem lmk_apply (s : Finset ι) (x) : (lmk s : _ →ₗ[R] Π₀ i, M i) x = mk s x := rfl #align dfinsupp.lmk_apply DFinsupp.lmk_apply diff --git a/Mathlib/LinearAlgebra/Finrank.lean b/Mathlib/LinearAlgebra/Finrank.lean index b06a9e20c8194..9bce6bfdd4970 100644 --- a/Mathlib/LinearAlgebra/Finrank.lean +++ b/Mathlib/LinearAlgebra/Finrank.lean @@ -503,9 +503,6 @@ noncomputable def finsetBasisOfTopLeSpanOfCardEqFinrank {s : Finset V} (_root_.trans (Fintype.card_coe _) card_eq) #align finset_basis_of_top_le_span_of_card_eq_finrank finsetBasisOfTopLeSpanOfCardEqFinrank --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply - /-- A set of `finrank K V` vectors forms a basis if they span the whole space. -/ @[simps! repr_apply] noncomputable def setBasisOfTopLeSpanOfCardEqFinrank {s : Set V} [Fintype s] diff --git a/Mathlib/LinearAlgebra/FreeModule/Norm.lean b/Mathlib/LinearAlgebra/FreeModule/Norm.lean index 1cb4e970068f2..f7e9b0ff73d33 100644 --- a/Mathlib/LinearAlgebra/FreeModule/Norm.lean +++ b/Mathlib/LinearAlgebra/FreeModule/Norm.lean @@ -44,8 +44,7 @@ theorem associated_norm_prod_smith [Fintype ι] (b : Basis ι R S) {f : S} (hf : Finsupp.single_eq_pi_single, Matrix.diagonal_mulVec_single, Pi.single_apply, ite_smul, zero_smul, Finset.sum_ite_eq', mul_one, if_pos (Finset.mem_univ _), b'.equiv_apply] change _ = f * _ - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [mul_comm, ← smul_eq_mul, LinearEquiv.restrictScalars_apply, LinearEquiv.coord_apply_smul, + rw [mul_comm, ← smul_eq_mul, LinearEquiv.restrictScalars_apply, LinearEquiv.coord_apply_smul, Ideal.selfBasis_def] rfl #align associated_norm_prod_smith associated_norm_prod_smith diff --git a/Mathlib/LinearAlgebra/Isomorphisms.lean b/Mathlib/LinearAlgebra/Isomorphisms.lean index 026ccc892bcf7..ffd4f3fabb0ea 100644 --- a/Mathlib/LinearAlgebra/Isomorphisms.lean +++ b/Mathlib/LinearAlgebra/Isomorphisms.lean @@ -113,8 +113,7 @@ theorem coe_quotientInfToSupQuotient (p p' : Submodule R M) : rfl #align linear_map.coe_quotient_inf_to_sup_quotient LinearMap.coe_quotientInfToSupQuotient --- This lemma was always bad, but the linter only noticed after lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem quotientInfEquivSupQuotient_apply_mk (p p' : Submodule R M) (x : p) : let map := ofLe (le_sup_left : p ≤ p ⊔ p') quotientInfEquivSupQuotient p p' (Submodule.Quotient.mk x) = diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean index a3b16d0d5b2bf..9dd5df3d4a6da 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean @@ -367,19 +367,10 @@ def liftAux (φ : MultilinearMap R s E) : (⨂[R] i, s i) →+ E := theorem liftAux_tprod (φ : MultilinearMap R s E) (f : ∀ i, s i) : liftAux φ (tprod R f) = φ f := by simp only [liftAux, liftAddHom, tprod_eq_tprodCoeff_one, tprodCoeff, AddCon.coe_mk'] - -- The end of this proof was very different before leanprover/lean4#2644: - -- rw [FreeAddMonoid.of, FreeAddMonoid.ofList, Equiv.refl_apply, AddCon.lift_coe] - -- dsimp [FreeAddMonoid.lift, FreeAddMonoid.sumAux] - -- show _ • _ = _ - -- rw [one_smul] - erw [AddCon.lift_coe] - erw [FreeAddMonoid.of] - dsimp [FreeAddMonoid.ofList] - rw [← one_smul R (φ f)] - erw [Equiv.refl_apply] - convert one_smul R (φ f) - simp - + rw [FreeAddMonoid.of, FreeAddMonoid.ofList, Equiv.refl_apply, AddCon.lift_coe] + dsimp [FreeAddMonoid.lift, FreeAddMonoid.sumAux] + show _ • _ = _ + rw [one_smul] #align pi_tensor_product.lift_aux_tprod PiTensorProduct.liftAux_tprod theorem liftAux_tprodCoeff (φ : MultilinearMap R s E) (z : R) (f : ∀ i, s i) : diff --git a/Mathlib/LinearAlgebra/Prod.lean b/Mathlib/LinearAlgebra/Prod.lean index 6ab253a8fab25..5723fe3f2b504 100644 --- a/Mathlib/LinearAlgebra/Prod.lean +++ b/Mathlib/LinearAlgebra/Prod.lean @@ -759,6 +759,36 @@ theorem snd_comp_prodComm : end prodComm +section SkewSwap + +variable (R M N) +variable [Semiring R] +variable [AddCommGroup M] [AddCommGroup N] +variable [Module R M] [Module R N] + +/-- The map `(x, y) ↦ (-y, x)` as a linear equivalence. -/ +protected def skewSwap : (M × N) ≃ₗ[R] (N × M) where + toFun x := (-x.2, x.1) + invFun x := (x.2, -x.1) + map_add' _ _ := by + simp [add_comm] + map_smul' _ _ := by + simp + left_inv _ := by + simp + right_inv _ := by + simp + +variable {R M N} + +@[simp] +theorem skewSwap_apply (x : M × N) : LinearEquiv.skewSwap R M N x = (-x.2, x.1) := rfl + +@[simp] +theorem skewSwap_symm_apply (x : N × M) : (LinearEquiv.skewSwap R M N).symm x = (x.2, -x.1) := rfl + +end SkewSwap + section variable (R M M₂ M₃ M₄) diff --git a/Mathlib/ModelTheory/DirectLimit.lean b/Mathlib/ModelTheory/DirectLimit.lean index 5fe6ab3e0e90c..e34a6080c8399 100644 --- a/Mathlib/ModelTheory/DirectLimit.lean +++ b/Mathlib/ModelTheory/DirectLimit.lean @@ -65,10 +65,8 @@ theorem coe_natLERec (m n : ℕ) (h : m ≤ n) : obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h ext x induction' k with k ih - · -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [natLERec, Nat.leRecOn_self, Embedding.refl_apply, Nat.leRecOn_self] - · -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec, + · rw [natLERec, Nat.leRecOn_self, Embedding.refl_apply, Nat.leRecOn_self] + · rw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec, Embedding.comp_apply, ih] #align first_order.language.directed_system.coe_nat_le_rec FirstOrder.Language.DirectedSystem.coe_natLERec diff --git a/Mathlib/ModelTheory/Fraisse.lean b/Mathlib/ModelTheory/Fraisse.lean index 9a21e7f2f8fd8..d63111cee36cd 100644 --- a/Mathlib/ModelTheory/Fraisse.lean +++ b/Mathlib/ModelTheory/Fraisse.lean @@ -300,10 +300,6 @@ theorem IsUltrahomogeneous.amalgamation_age (h : L.IsUltrahomogeneous M) : erw [Substructure.coe_inclusion, Substructure.coe_inclusion] simp only [Embedding.comp_apply, Equiv.coe_toEmbedding, Set.coe_inclusion, Embedding.equivRange_apply, hgn] - -- This used to be `simp only [...]` before leanprover/lean4#2644 - erw [Embedding.comp_apply, Equiv.coe_toEmbedding, - Embedding.equivRange_apply] - simp #align first_order.language.is_ultrahomogeneous.amalgamation_age FirstOrder.Language.IsUltrahomogeneous.amalgamation_age theorem IsUltrahomogeneous.age_isFraisse [Countable M] (h : L.IsUltrahomogeneous M) : diff --git a/Mathlib/ModelTheory/Semantics.lean b/Mathlib/ModelTheory/Semantics.lean index 51e70d70bc6da..471bdb46d177b 100644 --- a/Mathlib/ModelTheory/Semantics.lean +++ b/Mathlib/ModelTheory/Semantics.lean @@ -476,13 +476,11 @@ theorem realize_constantsVarsEquiv [L[[α]].Structure M] [(lhomWithConstants L {n} {φ : L[[α]].BoundedFormula β n} {v : β → M} {xs : Fin n → M} : (constantsVarsEquiv φ).Realize (Sum.elim (fun a => ↑(L.con a)) v) xs ↔ φ.Realize v xs := by refine' realize_mapTermRel_id (fun n t xs => realize_constantsVarsEquivLeft) fun n R xs => _ - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← (lhomWithConstants L α).map_onRelation + rw [← (lhomWithConstants L α).map_onRelation (Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n) R) xs] rcongr cases' R with R R - · -- This used to be `simp` before leanprover/lean4#2644 - simp; erw [Equiv.sumEmpty_apply_inl] + · simp · exact isEmptyElim R #align first_order.language.bounded_formula.realize_constants_vars_equiv FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv diff --git a/Mathlib/Order/Category/PartOrd.lean b/Mathlib/Order/Category/PartOrd.lean index 63a31d86123ce..2e3417621f204 100644 --- a/Mathlib/Order/Category/PartOrd.lean +++ b/Mathlib/Order/Category/PartOrd.lean @@ -146,6 +146,3 @@ def preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd : (fun _ => OrderHom.ext _ _ <| funext fun x => Quotient.inductionOn' x fun _ => rfl) set_option linter.uppercaseLean3 false in #align Preord_to_PartOrd_comp_to_dual_iso_to_dual_comp_Preord_to_PartOrd preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd - --- This lemma was always bad, but the linter only noticed after lean4#2644 -attribute [nolint simpNF] preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_coe diff --git a/Mathlib/Order/InitialSeg.lean b/Mathlib/Order/InitialSeg.lean index 67a77c84ab0bf..4b77aefec8f68 100644 --- a/Mathlib/Order/InitialSeg.lean +++ b/Mathlib/Order/InitialSeg.lean @@ -382,8 +382,7 @@ def ofElement {α : Type*} (r : α → α → Prop) (a : α) : Subrel r { b | r ⟨Subrel.relEmbedding _ _, a, fun _ => ⟨fun h => ⟨⟨_, h⟩, rfl⟩, fun ⟨⟨_, h⟩, rfl⟩ => h⟩⟩ #align principal_seg.of_element PrincipalSeg.ofElement --- This lemma was always bad, but the linter only noticed after lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem ofElement_apply {α : Type*} (r : α → α → Prop) (a : α) (b) : ofElement r a b = b.1 := rfl #align principal_seg.of_element_apply PrincipalSeg.ofElement_apply @@ -401,17 +400,12 @@ noncomputable def subrelIso (f : r ≺i s) : Subrel s {b | s b f.top} ≃r r := (funext fun _ ↦ propext f.down.symm))), map_rel_iff' := f.map_rel_iff } --- This lemma was always bad, but the linter only noticed after lean4#2644 -attribute [nolint simpNF] PrincipalSeg.subrelIso_symm_apply - --- This lemma was always bad, but the linter only noticed after lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem apply_subrelIso (f : r ≺i s) (b : {b | s b f.top}) : f (f.subrelIso b) = b := Equiv.apply_ofInjective_symm f.injective _ --- This lemma was always bad, but the linter only noticed after lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem subrelIso_apply (f : r ≺i s) (a : α) : f.subrelIso ⟨f a, f.down.mpr ⟨a, rfl⟩⟩ = a := Equiv.ofInjective_symm_apply f.injective _ @@ -573,5 +567,3 @@ theorem collapse_apply [IsWellOrder β s] (f : r ↪r s) (a) : collapse f a = (c #align rel_embedding.collapse_apply RelEmbedding.collapse_apply end RelEmbedding -attribute [nolint simpNF] PrincipalSeg.ofElement_apply PrincipalSeg.subrelIso_symm_apply - PrincipalSeg.apply_subrelIso PrincipalSeg.subrelIso_apply diff --git a/Mathlib/Order/LocallyFinite.lean b/Mathlib/Order/LocallyFinite.lean index b5c6794182c66..88697fca0d655 100644 --- a/Mathlib/Order/LocallyFinite.lean +++ b/Mathlib/Order/LocallyFinite.lean @@ -1085,9 +1085,7 @@ instance locallyFiniteOrder : LocallyFiniteOrder (WithTop α) where not_exists, not_and, and_imp, Embedding.some, forall_const] | (a : α), (b : α), (x : α) => by simp only [some, le_eq_subset, Embedding.some, mem_map, mem_Icc, Embedding.coeFn_mk, - some_le_some] - -- This used to be in the above `simp` before leanprover/lean4#2644 - erw [aux] + some_le_some, aux] finset_mem_Ico a b x := match a, b, x with | ⊤, b, x => iff_of_false (not_mem_empty _) fun h => not_top_lt <| h.1.trans_lt h.2 @@ -1095,40 +1093,23 @@ instance locallyFiniteOrder : LocallyFiniteOrder (WithTop α) where | (a : α), ⊤, (x : α) => by simp only [some, Embedding.some, mem_map, mem_Ici, Embedding.coeFn_mk, some_le_some, aux, top, some_lt_none, and_true] - -- This used to be in the above `simp` before leanprover/lean4#2644 - erw [aux] | (a : α), (b : α), ⊤ => by simp [some, Embedding.some] | (a : α), (b : α), (x : α) => by simp [some, Embedding.some, aux] - -- This used to be in the above `simp` before - -- leanprover/lean4#2644 - erw [aux] finset_mem_Ioc a b x := match a, b, x with | ⊤, b, x => iff_of_false (not_mem_empty _) fun h => not_top_lt <| h.1.trans_le h.2 | (a : α), ⊤, ⊤ => by simp [some, insertNone, top] | (a : α), ⊤, (x : α) => by simp [some, Embedding.some, insertNone, aux] - -- This used to be in the above `simp` before - -- leanprover/lean4#2644 - erw [aux] | (a : α), (b : α), ⊤ => by simp [some, Embedding.some, insertNone] | (a : α), (b : α), (x : α) => by simp [some, Embedding.some, insertNone, aux] - -- This used to be in the above `simp` before - -- leanprover/lean4#2644 - erw [aux] finset_mem_Ioo a b x := match a, b, x with | ⊤, b, x => iff_of_false (not_mem_empty _) fun h => not_top_lt <| h.1.trans h.2 | (a : α), ⊤, ⊤ => by simp [some, Embedding.some, insertNone] | (a : α), ⊤, (x : α) => by simp [some, Embedding.some, insertNone, aux, top] - -- This used to be in the above `simp` before - -- leanprover/lean4#2644 - erw [aux] | (a : α), (b : α), ⊤ => by simp [some, Embedding.some, insertNone] | (a : α), (b : α), (x : α) => by simp [some, Embedding.some, insertNone, aux] - -- This used to be in the above `simp` before - -- leanprover/lean4#2644 - erw [aux] variable (a b : α) diff --git a/Mathlib/RepresentationTheory/Action.lean b/Mathlib/RepresentationTheory/Action.lean index 58279e05a4fd3..5666b97b845b6 100644 --- a/Mathlib/RepresentationTheory/Action.lean +++ b/Mathlib/RepresentationTheory/Action.lean @@ -78,9 +78,6 @@ def ρAut {G : GroupCat.{u}} (A : Action V (MonCat.of G)) : G ⟶ GroupCat.of (A set_option linter.uppercaseLean3 false in #align Action.ρ_Aut Action.ρAut --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] Action.ρAut_apply_inv Action.ρAut_apply_hom - variable (G : MonCat.{u}) section @@ -741,15 +738,13 @@ theorem leftDual_v [LeftRigidCategory V] : (ᘁX).V = ᘁX.V := set_option linter.uppercaseLean3 false in #align Action.left_dual_V Action.leftDual_v --- This lemma was always bad, but the linter only noticed after lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem rightDual_ρ [RightRigidCategory V] (h : H) : Xᘁ.ρ h = (X.ρ (h⁻¹ : H))ᘁ := by rw [← SingleObj.inv_as_inv]; rfl set_option linter.uppercaseLean3 false in #align Action.right_dual_ρ Action.rightDual_ρ --- This lemma was always bad, but the linter only noticed after lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem leftDual_ρ [LeftRigidCategory V] (h : H) : (ᘁX).ρ h = ᘁX.ρ (h⁻¹ : H) := by rw [← SingleObj.inv_as_inv]; rfl set_option linter.uppercaseLean3 false in @@ -906,8 +901,7 @@ noncomputable def leftRegularTensorIso (G : Type u) [Group G] (X : Action (Type refine' Prod.ext rfl _ erw [tensor_rho, tensor_rho] dsimp - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [leftRegular_ρ_apply] + rw [leftRegular_ρ_apply] erw [map_mul] rfl } hom_inv_id := by diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean b/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean index 6f52e4933c859..58411e2378df1 100644 --- a/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean +++ b/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean @@ -117,6 +117,7 @@ def d [Monoid G] (n : ℕ) (A : Rep k G) : ((Fin n → G) → A) →ₗ[k] (Fin variable [Group G] (n) (A : Rep k G) /- Porting note: linter says the statement doesn't typecheck, so we add `@[nolint checkType]` -/ +set_option maxHeartbeats 700000 in /-- The theorem that our isomorphism `Fun(Gⁿ, A) ≅ Hom(k[Gⁿ⁺¹], A)` (where the righthand side is morphisms in `Rep k G`) commutes with the differentials in the complex of inhomogeneous cochains and the homogeneous `linearYonedaObjResolution`. -/ @@ -147,14 +148,12 @@ 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 - erw [diagonalHomEquiv_apply, Action.comp_hom, ModuleCat.comp_def, LinearMap.comp_apply, + rw [diagonalHomEquiv_apply, Action.comp_hom, ModuleCat.comp_def, LinearMap.comp_apply, Resolution.d_eq] erw [Resolution.d_of (Fin.partialProd g)] rw [map_sum] simp only [←Finsupp.smul_single_one _ ((-1 : k) ^ _)] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [d_apply, @Fin.sum_univ_succ _ _ (n + 1), Fin.val_zero, pow_zero, one_smul, + rw [d_apply, @Fin.sum_univ_succ _ _ (n + 1), Fin.val_zero, pow_zero, one_smul, Fin.succAbove_zero, diagonalHomEquiv_symm_apply f (Fin.partialProd g ∘ @Fin.succ (n + 1))] simp_rw [Function.comp_apply, Fin.partialProd_succ, Fin.castSucc_zero, Fin.partialProd_zero, one_mul] @@ -162,8 +161,7 @@ and the homogeneous `linearYonedaObjResolution`. -/ · have := Fin.partialProd_right_inv g (Fin.castSucc x) simp only [mul_inv_rev, Fin.castSucc_fin_succ] at this ⊢ rw [mul_assoc, ← mul_assoc _ _ (g x.succ), this, inv_mul_cancel_left] - · -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [map_smul, diagonalHomEquiv_symm_partialProd_succ, Fin.val_succ] + · rw [map_smul, diagonalHomEquiv_symm_partialProd_succ, Fin.val_succ] #align inhomogeneous_cochains.d_eq InhomogeneousCochains.d_eq end InhomogeneousCochains @@ -174,6 +172,7 @@ variable [Group G] (n) (A : Rep k G) open InhomogeneousCochains +set_option maxHeartbeats 2400000 in /-- Given a `k`-linear `G`-representation `A`, this is the complex of inhomogeneous cochains $$0 \to \mathrm{Fun}(G^0, A) \to \mathrm{Fun}(G^1, A) \to \mathrm{Fun}(G^2, A) \to \dots$$ which calculates the group cohomology of `A`. -/ @@ -200,6 +199,7 @@ noncomputable abbrev inhomogeneousCochains : CochainComplex (ModuleCat k) ℕ := exact map_zero _ #align group_cohomology.inhomogeneous_cochains GroupCohomology.inhomogeneousCochains +set_option maxHeartbeats 2000000 in /-- Given a `k`-linear `G`-representation `A`, the complex of inhomogeneous cochains is isomorphic to `Hom(P, A)`, where `P` is the standard resolution of `k` as a trivial `G`-representation. -/ def inhomogeneousCochainsIso : inhomogeneousCochains A ≅ linearYonedaObjResolution A := by @@ -222,6 +222,7 @@ def groupCohomology [Group G] (A : Rep k G) (n : ℕ) : ModuleCat k := (inhomogeneousCochains A).homology n #align group_cohomology groupCohomology +set_option maxHeartbeats 3200000 in /-- The `n`th group cohomology of a `k`-linear `G`-representation `A` is isomorphic to `Extⁿ(k, A)` (taken in `Rep k G`), where `k` is a trivial `k`-linear `G`-representation. -/ def groupCohomologyIsoExt [Group G] (A : Rep k G) (n : ℕ) : diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean index 8df4bc2679aa2..e667965a2b897 100644 --- a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean +++ b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean @@ -189,8 +189,7 @@ theorem diagonalSucc_hom_single (f : Gⁿ⁺¹) (a : k) : ((inv ((linearization k G).μ (Action.leftRegular G) { V := Fin n → G, ρ := 1 })).hom ((lmapDomain k k (actionDiagonalSucc G n).hom.hom) (single f a))) = _ simp only [CategoryTheory.Functor.map_id, linearization_μ_inv_hom] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [lmapDomain_apply, mapDomain_single, LinearEquiv.coe_toLinearMap, finsuppTensorFinsupp', + rw [lmapDomain_apply, mapDomain_single, LinearEquiv.coe_toLinearMap, finsuppTensorFinsupp', LinearEquiv.trans_symm, LinearEquiv.trans_apply, lcongr_symm, Equiv.refl_symm] erw [lcongr_single] rw [TensorProduct.lid_symm_apply, actionDiagonalSucc_hom_apply, finsuppTensorFinsupp_symm_single] @@ -228,14 +227,10 @@ theorem diagonalSucc_inv_single_left (g : G) (f : Gⁿ →₀ k) (r : k) : simp only [lift_apply, smul_single', mul_one, TensorProduct.tmul_add, map_add, 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 - erw [map_zero] + · rw [TensorProduct.tmul_zero, map_zero, map_zero] · intro _ _ _ _ _ hx - rw [TensorProduct.tmul_add, map_add]; erw [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 - erw [diagonalSucc_inv_single_single] + rw [TensorProduct.tmul_add, map_add, map_add, hx] + simp_rw [lift_apply, smul_single, smul_eq_mul, diagonalSucc_inv_single_single] rw [sum_single_index, mul_comm] · rw [zero_mul, single_zero] #align group_cohomology.resolution.diagonal_succ_inv_single_left GroupCohomology.Resolution.diagonalSucc_inv_single_left @@ -249,14 +244,10 @@ 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 - erw [map_zero] + · rw [TensorProduct.zero_tmul, map_zero, map_zero] · intro _ _ _ _ _ hx - rw [TensorProduct.add_tmul, map_add]; erw [map_add, hx] - simp_rw [lift_apply, smul_single'] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [diagonalSucc_inv_single_single] + rw [TensorProduct.add_tmul, map_add, map_add, hx] + simp_rw [lift_apply, smul_single', diagonalSucc_inv_single_single] rw [sum_single_index] · rw [zero_mul, single_zero] #align group_cohomology.resolution.diagonal_succ_inv_single_right GroupCohomology.Resolution.diagonalSucc_inv_single_right @@ -276,8 +267,7 @@ 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 - erw [RingHom.id_apply, LinearEquiv.toFun_eq_coe, ← LinearEquiv.map_smul] + rw [RingHom.id_apply, LinearEquiv.toFun_eq_coe, ← LinearEquiv.map_smul] congr 1 /- Porting note: broken proof was refine' x.induction_on _ (fun x y => _) fun y z hy hz => _ @@ -375,11 +365,9 @@ 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 - erw [ModuleCat.coe_comp] + 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] + rw [diagonalSucc_hom_single] erw [TensorProduct.uncurry_apply, Finsupp.lift_apply, Finsupp.sum_single_index] simp only [one_smul] erw [Representation.linHom_apply] diff --git a/Mathlib/RepresentationTheory/Rep.lean b/Mathlib/RepresentationTheory/Rep.lean index aa7180b06b714..bdf15d017f757 100644 --- a/Mathlib/RepresentationTheory/Rep.lean +++ b/Mathlib/RepresentationTheory/Rep.lean @@ -231,8 +231,7 @@ theorem linearization_ε_hom : (linearization k G).ε.hom = Finsupp.lsingle PUni set_option linter.uppercaseLean3 false in #align Rep.linearization_ε_hom Rep.linearization_ε_hom --- This was always a bad simp lemma, but the linter did not notice until lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem linearization_ε_inv_hom_apply (r : k) : (inv (linearization k G).ε).hom (Finsupp.single PUnit.unit r) = r := IsIso.hom_inv_id_apply (linearization k G).ε r @@ -300,8 +299,7 @@ set_option linter.uppercaseLean3 false in theorem leftRegularHom_apply {A : Rep k G} (x : A) : (leftRegularHom A x).hom (Finsupp.single 1 1) = x := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [leftRegularHom_hom, Finsupp.lift_apply, Finsupp.sum_single_index, one_smul, + rw [leftRegularHom_hom, Finsupp.lift_apply, Finsupp.sum_single_index, one_smul, A.ρ.map_one, LinearMap.one_apply] · rw [zero_smul] set_option linter.uppercaseLean3 false in @@ -330,8 +328,6 @@ noncomputable def leftRegularHomEquiv (A : Rep k G) : (Rep.ofMulAction k G G ⟶ rw [Finsupp.sum_single_index, ←this, of_ρ_apply] erw [Representation.ofMulAction_single x (1 : G) (1 : k)] simp only [one_smul, smul_eq_mul, mul_one] - · -- This goal didn't exist before leanprover/lean4#2644 - rfl · rw [zero_smul] right_inv x := leftRegularHom_apply x set_option linter.uppercaseLean3 false in @@ -339,8 +335,7 @@ set_option linter.uppercaseLean3 false in theorem leftRegularHomEquiv_symm_single {A : Rep k G} (x : A) (g : G) : ((leftRegularHomEquiv A).symm x).hom (Finsupp.single g 1) = A.ρ g x := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [leftRegularHomEquiv_symm_apply, leftRegularHom_hom, Finsupp.lift_apply, + rw [leftRegularHomEquiv_symm_apply, leftRegularHom_hom, Finsupp.lift_apply, Finsupp.sum_single_index, one_smul] · rw [zero_smul] set_option linter.uppercaseLean3 false in @@ -400,12 +395,8 @@ def homEquiv (A B C : Rep k G) : (A ⊗ B ⟶ C) ≃ (B ⟶ (Rep.ihom A).obj C) hom_comm_apply f g y, Rep.ihom_obj_ρ_apply, LinearMap.comp_apply, ρ_inv_self_apply] -/ change TensorProduct.uncurry k _ _ _ f.hom.flip (A.ρ g x ⊗ₜ[k] B.ρ g y) = C.ρ g (TensorProduct.uncurry k _ _ _ f.hom.flip (x ⊗ₜ[k] y)) - -- The next 3 tactics used to be `rw` before leanprover/lean4#2644 - erw [TensorProduct.uncurry_apply, LinearMap.flip_apply, hom_comm_apply, - Rep.ihom_obj_ρ_apply, - LinearMap.comp_apply, LinearMap.comp_apply] --, ρ_inv_self_apply (A := C)] - dsimp - erw [ρ_inv_self_apply] + rw [TensorProduct.uncurry_apply, LinearMap.flip_apply, hom_comm_apply, Rep.ihom_obj_ρ_apply, + LinearMap.comp_apply, LinearMap.comp_apply, ρ_inv_self_apply] rfl} left_inv f := Action.Hom.ext _ _ (TensorProduct.ext' fun _ _ => rfl) right_inv f := by ext; rfl @@ -503,16 +494,14 @@ theorem MonoidalClosed.linearHomEquivComm_hom (f : A ⊗ B ⟶ C) : set_option linter.uppercaseLean3 false in #align Rep.monoidal_closed.linear_hom_equiv_comm_hom Rep.MonoidalClosed.linearHomEquivComm_hom --- This was always a bad simp lemma, but the linter did not notice until lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem MonoidalClosed.linearHomEquiv_symm_hom (f : B ⟶ A ⟶[Rep k G] C) : ((MonoidalClosed.linearHomEquiv A B C).symm f).hom = TensorProduct.uncurry k A B C f.hom.flip := rfl set_option linter.uppercaseLean3 false in #align Rep.monoidal_closed.linear_hom_equiv_symm_hom Rep.MonoidalClosed.linearHomEquiv_symm_hom --- This was always a bad simp lemma, but the linter did not notice until lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem MonoidalClosed.linearHomEquivComm_symm_hom (f : A ⟶ B ⟶[Rep k G] C) : ((MonoidalClosed.linearHomEquivComm A B C).symm f).hom = TensorProduct.uncurry k A B C f.hom := @@ -672,9 +661,9 @@ def unitIso (V : Rep k G) : V ≅ (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgeb /- Porting note: rest of broken proof was simp only [Representation.asModuleEquiv_symm_map_smul, RestrictScalars.addEquiv_symm_map_algebraMap_smul] -/ - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [AddEquiv.coe_toEquiv, AddEquiv.trans_apply, - Representation.asModuleEquiv_symm_map_smul] + rw [AddEquiv.coe_toEquiv, AddEquiv.trans_apply, + Representation.asModuleEquiv_symm_map_smul, + RestrictScalars.addEquiv_symm_map_algebraMap_smul] rfl }) fun g => by ext; apply unit_iso_comm set_option linter.uppercaseLean3 false in diff --git a/Mathlib/RingTheory/ClassGroup.lean b/Mathlib/RingTheory/ClassGroup.lean index 767581952d7c8..7b31e1b20d6be 100644 --- a/Mathlib/RingTheory/ClassGroup.lean +++ b/Mathlib/RingTheory/ClassGroup.lean @@ -115,10 +115,8 @@ noncomputable def ClassGroup.mk : (FractionalIdeal R⁰ K)ˣ →* ClassGroup R : -- Can't be `@[simp]` because it can't figure out the quotient relation. theorem ClassGroup.Quot_mk_eq_mk (I : (FractionalIdeal R⁰ (FractionRing R))ˣ) : Quot.mk _ I = ClassGroup.mk I := by - rw [ClassGroup.mk, canonicalEquiv_self, RingEquiv.coe_monoidHom_refl, Units.map_id] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidHom.comp_apply] - rw [MonoidHom.id_apply, QuotientGroup.mk'_apply] + rw [ClassGroup.mk, canonicalEquiv_self, RingEquiv.coe_monoidHom_refl, Units.map_id, + MonoidHom.comp_apply, MonoidHom.id_apply, QuotientGroup.mk'_apply] rfl theorem ClassGroup.mk_eq_mk {I J : (FractionalIdeal R⁰ <| FractionRing R)ˣ} : @@ -215,8 +213,7 @@ theorem ClassGroup.equiv_mk (K' : Type*) [Field K'] [Algebra R K'] [IsFractionRi (I : (FractionalIdeal R⁰ K)ˣ) : ClassGroup.equiv K' (ClassGroup.mk I) = QuotientGroup.mk' _ (Units.mapEquiv (↑(FractionalIdeal.canonicalEquiv R⁰ K K')) I) := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ClassGroup.equiv, ClassGroup.mk, MonoidHom.comp_apply, QuotientGroup.congr_mk'] + rw [ClassGroup.equiv, ClassGroup.mk, MonoidHom.comp_apply, QuotientGroup.congr_mk'] congr rw [← Units.eq_iff, Units.coe_mapEquiv, Units.coe_mapEquiv, Units.coe_map] exact FractionalIdeal.canonicalEquiv_canonicalEquiv _ _ _ _ _ @@ -227,10 +224,8 @@ theorem ClassGroup.mk_canonicalEquiv (K' : Type*) [Field K'] [Algebra R K'] [IsF (I : (FractionalIdeal R⁰ K)ˣ) : ClassGroup.mk (Units.map (↑(canonicalEquiv R⁰ K K')) I : (FractionalIdeal R⁰ K')ˣ) = ClassGroup.mk I := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ClassGroup.mk, MonoidHom.comp_apply, ← MonoidHom.comp_apply (Units.map _), - ← Units.map_comp, ← RingEquiv.coe_monoidHom_trans, - FractionalIdeal.canonicalEquiv_trans_canonicalEquiv] + rw [ClassGroup.mk, MonoidHom.comp_apply, ← MonoidHom.comp_apply (Units.map _), ← Units.map_comp, ← + RingEquiv.coe_monoidHom_trans, FractionalIdeal.canonicalEquiv_trans_canonicalEquiv] rfl #align class_group.mk_canonical_equiv ClassGroup.mk_canonicalEquiv diff --git a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean index cf8881473e997..bf509d779f584 100644 --- a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean +++ b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean @@ -429,8 +429,7 @@ instance : Algebra R (v.adicCompletionIntegers K) where refine' ValuationSubring.mul_mem _ _ _ _ x.2 --Porting note: added instance letI : Valued K ℤₘ₀ := adicValued v - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [mem_adicCompletionIntegers, h, Valued.valuedCompletion_apply] + rw [mem_adicCompletionIntegers, h, Valued.valuedCompletion_apply] exact v.valuation_le_one _⟩ toFun r := ⟨(algebraMap R K r : adicCompletion K v), by @@ -439,8 +438,7 @@ instance : Algebra R (v.adicCompletionIntegers K) where --Porting note: rest of proof was `simpa only -- [mem_adicCompletionIntegers, Valued.valuedCompletion_apply] using -- v.valuation_le_one _ - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [mem_adicCompletionIntegers, Valued.valuedCompletion_apply] + rw [mem_adicCompletionIntegers, Valued.valuedCompletion_apply] exact v.valuation_le_one _⟩ map_one' := by simp only [map_one]; rfl map_mul' x y := by diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal.lean b/Mathlib/RingTheory/DedekindDomain/Ideal.lean index 4026ecc90a541..200ebb17ce769 100644 --- a/Mathlib/RingTheory/DedekindDomain/Ideal.lean +++ b/Mathlib/RingTheory/DedekindDomain/Ideal.lean @@ -1156,10 +1156,7 @@ def normalizedFactorsEquivOfQuotEquiv (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors f.symm hI j.prop⟩ left_inv := fun ⟨j, hj⟩ => by simp - right_inv := fun ⟨j, hj⟩ => by - simp - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [OrderIso.apply_symm_apply] + right_inv := fun ⟨j, hj⟩ => by simp #align normalized_factors_equiv_of_quot_equiv normalizedFactorsEquivOfQuotEquiv @[simp] diff --git a/Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean b/Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean index ea260bf6c23b4..127c8fbdc1cbb 100644 --- a/Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean +++ b/Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean @@ -149,8 +149,7 @@ def valuationOfNeZeroMod (n : ℕ) : (K/n) →* Multiplicative (ZMod n) := @[simp] theorem valuation_of_unit_mod_eq (n : ℕ) (x : Rˣ) : v.valuationOfNeZeroMod n (Units.map (algebraMap R K : R →* K) x : K/n) = 1 := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [valuationOfNeZeroMod, MonoidHom.comp_apply, ← QuotientGroup.coe_mk', + rw [valuationOfNeZeroMod, MonoidHom.comp_apply, ← QuotientGroup.coe_mk', QuotientGroup.map_mk' (G := Kˣ) (N := MonoidHom.range (powMonoidHom n)), valuation_of_unit_eq, QuotientGroup.mk_one, map_one] #align is_dedekind_domain.height_one_spectrum.valuation_of_unit_mod_eq IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq diff --git a/Mathlib/RingTheory/Etale.lean b/Mathlib/RingTheory/Etale.lean index 50cfa6c3c6bc8..45fdea5251f37 100644 --- a/Mathlib/RingTheory/Etale.lean +++ b/Mathlib/RingTheory/Etale.lean @@ -193,8 +193,7 @@ theorem FormallySmooth.liftOfSurjective_apply [FormallySmooth R A] (f : A →ₐ g (FormallySmooth.liftOfSurjective f g hg hg' x) = f x := by apply (Ideal.quotientKerAlgEquivOfSurjective hg).symm.injective change _ = ((Ideal.quotientKerAlgEquivOfSurjective hg).symm.toAlgHom.comp f) x - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← FormallySmooth.mk_lift _ hg' + rw [← FormallySmooth.mk_lift _ hg' ((Ideal.quotientKerAlgEquivOfSurjective hg).symm.toAlgHom.comp f)] apply (Ideal.quotientKerAlgEquivOfSurjective hg).injective rw [AlgEquiv.apply_symm_apply, Ideal.quotientKerAlgEquivOfSurjective, diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index c02ecbec56b1b..f8d0c1a105f3e 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/Mathlib/RingTheory/Ideal/Operations.lean @@ -2018,9 +2018,6 @@ theorem basisSpanSingleton_apply (b : Basis ι R S) {x : S} (hx : x ≠ 0) (i : simp only [basisSpanSingleton, Basis.map_apply, LinearEquiv.trans_apply, Submodule.restrictScalarsEquiv_apply, LinearEquiv.ofInjective_apply, LinearEquiv.coe_ofEq_apply, LinearEquiv.restrictScalars_apply, Algebra.coe_lmul_eq_mul, LinearMap.mul_apply'] - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [LinearEquiv.coe_ofEq_apply, LinearEquiv.ofInjective_apply, Algebra.coe_lmul_eq_mul, - LinearMap.mul_apply'] #align ideal.basis_span_singleton_apply Ideal.basisSpanSingleton_apply @[simp] diff --git a/Mathlib/RingTheory/Ideal/QuotientOperations.lean b/Mathlib/RingTheory/Ideal/QuotientOperations.lean index 4f8bb42d92710..fe58b743f0b19 100644 --- a/Mathlib/RingTheory/Ideal/QuotientOperations.lean +++ b/Mathlib/RingTheory/Ideal/QuotientOperations.lean @@ -394,8 +394,7 @@ def kerLiftAlg (f : A →ₐ[R₁] B) : A ⧸ (RingHom.ker f.toRingHom) →ₐ[R #align ideal.ker_lift_alg Ideal.kerLiftAlg -- Porting note: changed from f.toRingHom to f on LHS since f.toRingHom = f is in simp --- This lemma was always bad, but the linter only noticed after lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem kerLiftAlg_mk (f : A →ₐ[R₁] B) (a : A) : kerLiftAlg f (Quotient.mk (RingHom.ker f) a) = f a := by rfl @@ -428,16 +427,14 @@ def quotientKerAlgEquivOfRightInverse {f : A →ₐ[R₁] B} {g : B → A} kerLiftAlg f with } #align ideal.quotient_ker_alg_equiv_of_right_inverse Ideal.quotientKerAlgEquivOfRightInverse --- This lemma was always bad, but the linter only noticed after lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem quotientKerAlgEquivOfRightInverse.apply {f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g f) (x : A ⧸ (RingHom.ker f.toRingHom)) : quotientKerAlgEquivOfRightInverse hf x = kerLiftAlg f x := rfl #align ideal.quotient_ker_alg_equiv_of_right_inverse.apply Ideal.quotientKerAlgEquivOfRightInverse.apply --- This lemma was always bad, but the linter only noticed after lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem QuotientKerAlgEquivOfRightInverseSymm.apply {f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g f) (x : B) : (quotientKerAlgEquivOfRightInverse hf).symm x = Quotient.mkₐ R₁ (RingHom.ker f.toRingHom) (g x) := diff --git a/Mathlib/RingTheory/Kaehler.lean b/Mathlib/RingTheory/Kaehler.lean index 1c811437c9aca..93bbf22df7bbb 100644 --- a/Mathlib/RingTheory/Kaehler.lean +++ b/Mathlib/RingTheory/Kaehler.lean @@ -214,8 +214,7 @@ def KaehlerDifferential.D : Derivation R S (Ω[S⁄R]) := leibniz' := fun a b => by have : LinearMap.CompatibleSMul { x // x ∈ ideal R S } (Ω[S⁄R]) S (S ⊗[R] S) := inferInstance dsimp [KaehlerDifferential.DLinearMap_apply, - Ideal.toCotangent_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← LinearMap.map_smul_of_tower (M₂ := Ω[S⁄R]), + rw [← LinearMap.map_smul_of_tower (M₂ := Ω[S⁄R]), ← LinearMap.map_smul_of_tower (M₂ := Ω[S⁄R]), ← map_add, Ideal.toCotangent_eq, pow_two] convert Submodule.mul_mem_mul (KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R a : _) (KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R b : _) using 1 diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean index 5ec72e9de9fe3..8cb30845374cc 100644 --- a/Mathlib/RingTheory/LaurentSeries.lean +++ b/Mathlib/RingTheory/LaurentSeries.lean @@ -161,11 +161,9 @@ instance of_powerSeries_localization [CommRing R] : intro m have h := hc (m + n) simp only at h - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [LinearMap.map_zero, PowerSeries.X_pow_eq, PowerSeries.monomial, + rwa [LinearMap.map_zero, PowerSeries.X_pow_eq, PowerSeries.monomial, add_comm m, PowerSeries.coeff, Finsupp.single_add, MvPowerSeries.coeff_add_monomial_mul, one_mul] at h - assumption #align laurent_series.of_power_series_localization LaurentSeries.of_powerSeries_localization -- Porting note: this instance is needed diff --git a/Mathlib/RingTheory/Norm.lean b/Mathlib/RingTheory/Norm.lean index 0a2728768e0bb..f74b2a6bae513 100644 --- a/Mathlib/RingTheory/Norm.lean +++ b/Mathlib/RingTheory/Norm.lean @@ -205,8 +205,7 @@ theorem norm_eq_norm_adjoin [FiniteDimensional K L] [IsSeparable K L] (x : L) : letI := isSeparable_tower_top_of_isSeparable K K⟮x⟯ L let pbL := Field.powerBasisOfFiniteOfSeparable K⟮x⟯ L let pbx := IntermediateField.adjoin.powerBasis (IsSeparable.isIntegral K x) - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← AdjoinSimple.algebraMap_gen K x, norm_eq_matrix_det (pbx.basis.smul pbL.basis) _, + rw [← AdjoinSimple.algebraMap_gen K x, norm_eq_matrix_det (pbx.basis.smul pbL.basis) _, smul_leftMulMatrix_algebraMap, det_blockDiagonal, norm_eq_matrix_det pbx.basis] simp only [Finset.card_fin, Finset.prod_const] congr diff --git a/Mathlib/RingTheory/PowerSeries/Basic.lean b/Mathlib/RingTheory/PowerSeries/Basic.lean index 1c42b834f9cf8..a0e3be13b4f44 100644 --- a/Mathlib/RingTheory/PowerSeries/Basic.lean +++ b/Mathlib/RingTheory/PowerSeries/Basic.lean @@ -150,11 +150,9 @@ theorem monomial_def [DecidableEq σ] (n : σ →₀ ℕ) : theorem coeff_monomial [DecidableEq σ] (m n : σ →₀ ℕ) (a : R) : coeff R m (monomial R n a) = if m = n then a else 0 := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [coeff, monomial_def, LinearMap.proj_apply (i := m)] + rw [coeff, monomial_def, LinearMap.proj_apply] dsimp only - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [LinearMap.stdBasis_apply, Function.update_apply, Pi.zero_apply] + rw [LinearMap.stdBasis_apply, Function.update_apply, Pi.zero_apply] #align mv_power_series.coeff_monomial MvPowerSeries.coeff_monomial @[simp] @@ -1442,8 +1440,7 @@ 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] + rw [monomial, Finsupp.single_zero, MvPowerSeries.monomial_zero_eq_C, C] set_option linter.uppercaseLean3 false in #align power_series.monomial_zero_eq_C PowerSeries.monomial_zero_eq_C @@ -1474,8 +1471,7 @@ set_option linter.uppercaseLean3 false in @[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 - erw [coeff, Finsupp.single_zero, X, MvPowerSeries.coeff_zero_X] + rw [coeff, Finsupp.single_zero, X, MvPowerSeries.coeff_zero_X] set_option linter.uppercaseLean3 false in #align power_series.coeff_zero_X PowerSeries.coeff_zero_X @@ -1551,7 +1547,7 @@ set_option linter.uppercaseLean3 false in theorem coeff_succ_mul_X (n : ℕ) (φ : R⟦X⟧) : coeff R (n + 1) (φ * X) = coeff R n φ := by simp only [coeff, Finsupp.single_add] convert φ.coeff_add_mul_monomial (single () n) (single () 1) _ - rw [mul_one]; rfl + rw [mul_one] set_option linter.uppercaseLean3 false in #align power_series.coeff_succ_mul_X PowerSeries.coeff_succ_mul_X @@ -1559,7 +1555,7 @@ set_option linter.uppercaseLean3 false in theorem coeff_succ_X_mul (n : ℕ) (φ : R⟦X⟧) : coeff R (n + 1) (X * φ) = coeff R n φ := by simp only [coeff, Finsupp.single_add, add_comm n 1] convert φ.coeff_add_monomial_mul (single () 1) (single () n) _ - rw [one_mul]; rfl + rw [one_mul] set_option linter.uppercaseLean3 false in #align power_series.coeff_succ_X_mul PowerSeries.coeff_succ_X_mul @@ -1957,8 +1953,7 @@ theorem coeff_inv_aux (n : ℕ) (a : R) (φ : R⟦X⟧) : -a * ∑ x in Finset.Nat.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 - erw [coeff, inv.aux, MvPowerSeries.coeff_inv_aux] + rw [coeff, inv.aux, MvPowerSeries.coeff_inv_aux] simp only [Finsupp.single_eq_zero] split_ifs; · rfl congr 1 diff --git a/Mathlib/RingTheory/SimpleModule.lean b/Mathlib/RingTheory/SimpleModule.lean index 77eba283dbee9..6168c37b7cde5 100644 --- a/Mathlib/RingTheory/SimpleModule.lean +++ b/Mathlib/RingTheory/SimpleModule.lean @@ -74,8 +74,6 @@ theorem covby_iff_quot_is_simple {A B : Submodule R M} (hAB : A ≤ B) : A ⋖ B ↔ IsSimpleModule R (B ⧸ Submodule.comap B.subtype A) := by set f : Submodule R B ≃o Set.Iic B := Submodule.MapSubtype.relIso B with hf rw [covby_iff_coatom_Iic hAB, isSimpleModule_iff_isCoatom, ← OrderIso.isCoatom_iff f, hf] - -- This used to be in the next `simp`, but we need `erw` after leanprover/lean4#2644 - erw [RelIso.coe_fn_mk] simp [-OrderIso.isCoatom_iff, Submodule.MapSubtype.relIso, Submodule.map_comap_subtype, inf_eq_right.2 hAB] #align covby_iff_quot_is_simple covby_iff_quot_is_simple diff --git a/Mathlib/RingTheory/Subring/Basic.lean b/Mathlib/RingTheory/Subring/Basic.lean index 4e5b4e3e1eacb..f64e14450d9e9 100644 --- a/Mathlib/RingTheory/Subring/Basic.lean +++ b/Mathlib/RingTheory/Subring/Basic.lean @@ -1354,10 +1354,6 @@ def subringMap (e : R ≃+* S) : s ≃+* s.map e.toRingHom := e.subsemiringMap s.toSubsemiring #align ring_equiv.subring_map RingEquiv.subringMap --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] RingEquiv.subringMap_symm_apply_coe - RingEquiv.subringMap_apply_coe - end RingEquiv namespace Subring diff --git a/Mathlib/RingTheory/Subsemiring/Basic.lean b/Mathlib/RingTheory/Subsemiring/Basic.lean index 34df7048356be..27bf73ba46db6 100644 --- a/Mathlib/RingTheory/Subsemiring/Basic.lean +++ b/Mathlib/RingTheory/Subsemiring/Basic.lean @@ -1324,9 +1324,6 @@ def subsemiringMap (e : R ≃+* S) (s : Subsemiring R) : s ≃+* s.map e.toRingH { e.toAddEquiv.addSubmonoidMap s.toAddSubmonoid, e.toMulEquiv.submonoidMap s.toSubmonoid with } #align ring_equiv.subsemiring_map RingEquiv.subsemiringMap --- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing -attribute [nolint simpNF] RingEquiv.subsemiringMap_symm_apply_coe RingEquiv.subsemiringMap_apply_coe - end RingEquiv /-! ### Actions by `Subsemiring`s diff --git a/Mathlib/RingTheory/Valuation/ValuationSubring.lean b/Mathlib/RingTheory/Valuation/ValuationSubring.lean index 2286840ac9564..aadb9feec4bb0 100644 --- a/Mathlib/RingTheory/Valuation/ValuationSubring.lean +++ b/Mathlib/RingTheory/Valuation/ValuationSubring.lean @@ -400,12 +400,6 @@ def primeSpectrumOrderEquiv : (PrimeSpectrum A)ᵒᵈ ≃o {S | A ≤ S} := fun h => by apply ofPrime_le_of_le; exact h⟩ } #align valuation_subring.prime_spectrum_order_equiv ValuationSubring.primeSpectrumOrderEquiv --- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing -attribute [nolint simpNF] ValuationSubring.primeSpectrumEquiv_symm_apply_asIdeal - ValuationSubring.primeSpectrumEquiv_apply_coe - ValuationSubring.primeSpectrumOrderEquiv_apply - ValuationSubring.primeSpectrumOrderEquiv_symm_apply - instance linearOrderOverring : LinearOrder {S | A ≤ S} := { (inferInstance : PartialOrder _) with le_total := @@ -718,15 +712,13 @@ def principalUnitGroupEquiv : map_mul' x y := rfl #align valuation_subring.principal_unit_group_equiv ValuationSubring.principalUnitGroupEquiv --- This was always a bad simp lemma, but the linter only noticed after lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem principalUnitGroupEquiv_apply (a : A.principalUnitGroup) : (((principalUnitGroupEquiv A a : Aˣ) : A) : K) = (a : Kˣ) := rfl #align valuation_subring.principal_unit_group_equiv_apply ValuationSubring.principalUnitGroupEquiv_apply --- This was always a bad simp lemma, but the linter only noticed after lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem principalUnitGroup_symm_apply (a : (Units.map (LocalRing.residue A).toMonoidHom).ker) : ((A.principalUnitGroupEquiv.symm a : Kˣ) : K) = ((a : Aˣ) : A) := rfl @@ -780,8 +772,7 @@ theorem unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk : A.unitGroupToResidueFieldUnits := rfl #align valuation_subring.units_mod_principal_units_equiv_residue_field_units_comp_quotient_group_mk ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk --- This was always a bad simp lemma, but the linter only noticed after lean4#2644 -@[simp, nolint simpNF] +@[simp] theorem unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply (x : A.unitGroup) : A.unitsModPrincipalUnitsEquivResidueFieldUnits.toMonoidHom (QuotientGroup.mk x) = diff --git a/Mathlib/Topology/Category/CompHaus/Projective.lean b/Mathlib/Topology/Category/CompHaus/Projective.lean index fbf4c976e868c..84d6b4dea6fda 100644 --- a/Mathlib/Topology/Category/CompHaus/Projective.lean +++ b/Mathlib/Topology/Category/CompHaus/Projective.lean @@ -53,8 +53,7 @@ instance projective_ultrafilter (X : Type*) : Projective (of <| Ultrafilter X) -- 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, comp.left_id] + rw [comp.assoc, ultrafilter_extend_extends, ← comp.assoc, this, comp.left_id] set_option linter.uppercaseLean3 false in #align CompHaus.projective_ultrafilter CompHaus.projective_ultrafilter diff --git a/Mathlib/Topology/Category/Profinite/Basic.lean b/Mathlib/Topology/Category/Profinite/Basic.lean index 82761849d23da..ab006fb78c4a8 100644 --- a/Mathlib/Topology/Category/Profinite/Basic.lean +++ b/Mathlib/Topology/Category/Profinite/Basic.lean @@ -383,35 +383,30 @@ theorem epi_iff_surjective {X Y : Profinite.{u}} (f : X ⟶ Y) : Epi f ↔ Funct ext x apply ULift.ext dsimp [LocallyConstant.ofClopen] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [comp_apply, ContinuousMap.coe_mk, comp_apply, ContinuousMap.coe_mk, + rw [comp_apply, ContinuousMap.coe_mk, comp_apply, ContinuousMap.coe_mk, Function.comp_apply, if_neg] refine' mt (fun α => hVU α) _ simp only [Set.mem_range_self, not_true, not_false_iff, Set.mem_compl_iff] apply_fun fun e => (e y).down at H dsimp [LocallyConstant.ofClopen] at H - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H + rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H exact top_ne_bot H · rw [← CategoryTheory.epi_iff_surjective] apply (forget Profinite).epi_of_epi_map #align Profinite.epi_iff_surjective Profinite.epi_iff_surjective instance {X Y : Profinite} (f : X ⟶ Y) [Epi f] : @Epi CompHaus _ _ _ f := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [CompHaus.epi_iff_surjective, ← epi_iff_surjective]; assumption + rwa [CompHaus.epi_iff_surjective, ← epi_iff_surjective] instance {X Y : Profinite} (f : X ⟶ Y) [@Epi CompHaus _ _ _ f] : Epi f := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [epi_iff_surjective, ← CompHaus.epi_iff_surjective]; assumption + rwa [epi_iff_surjective, ← CompHaus.epi_iff_surjective] theorem mono_iff_injective {X Y : Profinite.{u}} (f : X ⟶ Y) : Mono f ↔ Function.Injective f := by constructor · intro h haveI : Limits.PreservesLimits profiniteToCompHaus := inferInstance haveI : Mono (profiniteToCompHaus.map f) := inferInstance - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← CompHaus.mono_iff_injective] + rw [← CompHaus.mono_iff_injective] assumption · rw [← CategoryTheory.mono_iff_injective] apply (forget Profinite).mono_of_mono_map diff --git a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean b/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean index 63035ff10b9bd..b38af71e33900 100644 --- a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean +++ b/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean @@ -122,11 +122,9 @@ theorem exists_locallyConstant_fin_two (hC : IsLimit C) (f : LocallyConstant C.p obtain ⟨j, V, hV, h⟩ := exists_clopen_of_cofiltered C hC hU use j, LocallyConstant.ofClopen hV apply LocallyConstant.locallyConstant_eq_of_fiber_zero_eq - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [LocallyConstant.coe_comap _ _ (C.π.app j).continuous] + rw [LocallyConstant.coe_comap _ _ (C.π.app j).continuous] conv_rhs => rw [Set.preimage_comp] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [LocallyConstant.ofClopen_fiber_zero hV, ← h] + rw [LocallyConstant.ofClopen_fiber_zero hV, ← h] set_option linter.uppercaseLean3 false in #align Profinite.exists_locally_constant_fin_two Profinite.exists_locallyConstant_fin_two @@ -160,11 +158,9 @@ theorem exists_locallyConstant_finite_aux {α : Type*} [Finite α] (hC : IsLimit rw [h] dsimp ext1 x - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [LocallyConstant.coe_comap _ _ (C.π.app (j a)).continuous] + rw [LocallyConstant.coe_comap _ _ (C.π.app (j a)).continuous] dsimp [LocallyConstant.flip, LocallyConstant.unflip] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [LocallyConstant.coe_comap _ _ (C.π.app j0).continuous] + rw [LocallyConstant.coe_comap _ _ (C.π.app j0).continuous] dsimp rw [LocallyConstant.coe_comap _ _ _] -- Porting note: `repeat' rw [LocallyConstant.coe_comap]` didn't work @@ -172,7 +168,7 @@ theorem exists_locallyConstant_finite_aux {α : Type*} [Finite α] (hC : IsLimit · dsimp congr! 1 change _ = (C.π.app j0 ≫ F.map (fs a)) x - rw [C.w]; rfl + rw [C.w] · exact (F.map _).continuous set_option linter.uppercaseLean3 false in #align Profinite.exists_locally_constant_finite_aux Profinite.exists_locallyConstant_finite_aux @@ -186,17 +182,14 @@ theorem exists_locallyConstant_finite_nonempty {α : Type*} [Finite α] [Nonempt let σ : (α → Fin 2) → α := fun f => if h : ∃ a : α, ι a = f then h.choose else default refine' ⟨j, gg.map σ, _⟩ ext x - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [LocallyConstant.coe_comap _ _ (C.π.app j).continuous] + rw [LocallyConstant.coe_comap _ _ (C.π.app j).continuous] dsimp have h1 : ι (f x) = gg (C.π.app j x) := by change f.map (fun a b => if a = b then (0 : Fin 2) else 1) x = _ - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [h, LocallyConstant.coe_comap _ _ (C.π.app j).continuous] + rw [h, LocallyConstant.coe_comap _ _ (C.π.app j).continuous] rfl have h2 : ∃ a : α, ι a = gg (C.π.app j x) := ⟨f x, h1⟩ - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [dif_pos h2] + rw [dif_pos h2] apply_fun ι · rw [h2.choose_spec] exact h1 @@ -245,8 +238,7 @@ theorem exists_locallyConstant {α : Type*} (hC : IsLimit C) (f : LocallyConstan refine' ⟨j, ⟨ff ∘ g', g'.isLocallyConstant.comp _⟩, _⟩ ext1 t apply_fun fun e => e t at hj - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [LocallyConstant.coe_comap _ _ (C.π.app j).continuous] at hj ⊢ + rw [LocallyConstant.coe_comap _ _ (C.π.app j).continuous] at hj ⊢ dsimp at hj ⊢ rw [← hj] rfl diff --git a/Mathlib/Topology/Category/Profinite/Projective.lean b/Mathlib/Topology/Category/Profinite/Projective.lean index 65bbc0534b537..e6e6119497c97 100644 --- a/Mathlib/Topology/Category/Profinite/Projective.lean +++ b/Mathlib/Topology/Category/Profinite/Projective.lean @@ -49,8 +49,7 @@ 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, comp.left_id] + rw [comp.assoc, ultrafilter_extend_extends, ← comp.assoc, this, comp.left_id] #align Profinite.projective_ultrafilter Profinite.projective_ultrafilter /-- For any profinite `X`, the natural map `Ultrafilter X → X` is a projective presentation. -/ diff --git a/Mathlib/Topology/Category/Stonean/Limits.lean b/Mathlib/Topology/Category/Stonean/Limits.lean index a476b2167ffd9..e5d588c2e2931 100644 --- a/Mathlib/Topology/Category/Stonean/Limits.lean +++ b/Mathlib/Topology/Category/Stonean/Limits.lean @@ -222,8 +222,7 @@ lemma pullback.condition {X Y Z : Stonean.{u}} (f : X ⟶ Z) {i : Y ⟶ Z} obtain ⟨y, hy⟩ := h simp only [fst, snd, comp_apply] change f x = _ - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← hy, @ContinuousMap.coe_mk _ _ (Stonean.instTopologicalSpace (pullback f hi)) _ _ _] + rw [← hy, @ContinuousMap.coe_mk _ _ (Stonean.instTopologicalSpace (pullback f hi)) _ _ _] congr apply_fun (Homeomorph.ofEmbedding i hi.toEmbedding) simpa only [Homeomorph.ofEmbedding, Homeomorph.homeomorph_mk_coe, Equiv.ofInjective_apply, diff --git a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean index 0d21234da04dd..64fdbcb58c63f 100644 --- a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean +++ b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean @@ -53,11 +53,8 @@ def pullbackCone (f : X ⟶ Z) (g : Y ⟶ Z) : PullbackCone f g := (by dsimp [pullbackFst, pullbackSnd, Function.comp] ext ⟨x, h⟩ - -- Next 2 lines were - -- `rw [comp_apply, ContinuousMap.coe_mk, comp_apply, ContinuousMap.coe_mk]` - -- `exact h` before leanprover/lean4#2644 - rw [comp_apply, comp_apply] - congr!) + rw [comp_apply, ContinuousMap.coe_mk, comp_apply, ContinuousMap.coe_mk] + exact h) #align Top.pullback_cone TopCat.pullbackCone /-- The constructed cone is a limit. -/ @@ -77,12 +74,12 @@ 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] + 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] + rw [comp_apply, ContinuousMap.coe_mk] + rfl · intro m h₁ h₂ -- Porting note: used to be ext x apply ContinuousMap.ext; intro x @@ -171,8 +168,7 @@ theorem range_pullback_to_prod {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : apply Concrete.limit_ext rintro ⟨⟨⟩⟩ <;> rw [←comp_apply, prod.comp_lift, ←comp_apply, limit.lift_π] <;> - -- This used to be `simp` before leanprover/lean4#2644 - aesop_cat + simp #align Top.range_pullback_to_prod TopCat.range_pullback_to_prod theorem inducing_pullback_to_prod {X Y Z : TopCat.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) : diff --git a/Mathlib/Topology/ContinuousFunction/Compact.lean b/Mathlib/Topology/ContinuousFunction/Compact.lean index 3900a6ba39c2f..44372ea4077fd 100644 --- a/Mathlib/Topology/ContinuousFunction/Compact.lean +++ b/Mathlib/Topology/ContinuousFunction/Compact.lean @@ -496,10 +496,6 @@ theorem summable_of_locally_summable_norm {ι : Type*} {F : ι → C(X, E)} intro s ext1 x simp - -- This used to be the end of the proof before leanprover/lean4#2644 - erw [restrict_apply, restrict_apply, restrict_apply, restrict_apply] - simp - congr! simpa only [HasSum, A] using summable_of_summable_norm (hF K) #align continuous_map.summable_of_locally_summable_norm ContinuousMap.summable_of_locally_summable_norm diff --git a/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean b/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean index 946e1964df086..e3ff8955180c6 100644 --- a/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean +++ b/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean @@ -70,8 +70,6 @@ theorem polynomial_comp_attachBound (A : Subalgebra ℝ C(X, ℝ)) (f : A) (g : simp only [ContinuousMap.coe_comp, Function.comp_apply, ContinuousMap.attachBound_apply_coe, Polynomial.toContinuousMapOn_apply, Polynomial.aeval_subalgebra_coe, Polynomial.aeval_continuousMap_apply, Polynomial.toContinuousMap_apply] - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [ContinuousMap.attachBound_apply_coe] #align continuous_map.polynomial_comp_attach_bound ContinuousMap.polynomial_comp_attachBound /-- Given a continuous function `f` in a subalgebra of `C(X, ℝ)`, postcomposing by a polynomial diff --git a/Mathlib/Topology/Gluing.lean b/Mathlib/Topology/Gluing.lean index 8a07a17696c80..694923143d2dd 100644 --- a/Mathlib/Topology/Gluing.lean +++ b/Mathlib/Topology/Gluing.lean @@ -174,10 +174,8 @@ theorem eqvGen_of_π_eq let diagram := parallelPair 𝖣.diagram.fstSigmaMap 𝖣.diagram.sndSigmaMap ⋙ forget _ have : colimit.ι diagram one x = colimit.ι diagram one y := by dsimp only [coequalizer.π, ContinuousMap.toFun_eq_coe] at h - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [← ι_preservesColimitsIso_hom, forget_map_eq_coe, types_comp_apply, h] + rw [← ι_preservesColimitsIso_hom, forget_map_eq_coe, types_comp_apply, h] simp - rfl have : (colimit.ι diagram _ ≫ colim.map _ ≫ (colimit.isoColimitCocone _).hom) _ = (colimit.ι diagram _ ≫ colim.map _ ≫ (colimit.isoColimitCocone _).hom) _ := @@ -221,7 +219,7 @@ theorem ι_eq_iff_rel (i j : D.J) (x : D.U i) (y : D.U j) : Cofan.mk_ι_app] rw [←comp_apply, colimit.ι_desc, ←comp_apply, colimit.ι_desc] erw [sigmaIsoSigma_hom_ι_apply, sigmaIsoSigma_hom_ι_apply] - exact Or.inr ⟨y, ⟨rfl, rfl⟩⟩ + exact Or.inr ⟨y, by dsimp [GlueData.diagram]; simp only [true_and]; rfl⟩ · rintro (⟨⟨⟩⟩ | ⟨z, e₁, e₂⟩) rfl dsimp only at * @@ -412,19 +410,8 @@ 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 - -- 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] - rw [comp_app] --, comp_app, id_app] - -- erw [ContinuousMap.coe_mk] - conv_lhs => erw [ContinuousMap.coe_mk] - erw [id_app] - rw [ContinuousMap.coe_mk] - erw [Subtype.mk_eq_mk] - rw [Prod.mk.inj_iff] - erw [Subtype.mk_eq_mk] - rw [Subtype.ext_iff] - rw [and_self_iff] + 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] 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' diff --git a/Mathlib/Topology/Instances/Complex.lean b/Mathlib/Topology/Instances/Complex.lean index 24af3915fb251..c9c19f57c4d52 100644 --- a/Mathlib/Topology/Instances/Complex.lean +++ b/Mathlib/Topology/Instances/Complex.lean @@ -75,8 +75,7 @@ theorem Complex.uniformContinuous_ringHom_eq_id_or_conj (K : Subfield ℂ) {ψ : rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ofReal.rangeRestrict r = j (ι x) · have := RingHom.congr_fun (ringHom_eq_ofReal_of_continuous hψ₁) r - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [RingHom.comp_apply, RingHom.comp_apply, hr, RingEquiv.toRingHom_eq_coe] at this + rw [RingHom.comp_apply, RingHom.comp_apply, hr, RingEquiv.toRingHom_eq_coe] at this convert this using 1 · exact (DenseInducing.extend_eq di hc.continuous _).symm · rw [← ofReal.coe_rangeRestrict, hr] diff --git a/lake-manifest.json b/lake-manifest.json index b747d61569496..6bc8a3268c78a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -9,6 +9,14 @@ "name": "Qq", "inputRev?": "master", "inherited": false}}, + {"git": + {"url": "https://github.com/JLimperg/aesop", + "subDir?": null, + "rev": "41c6370eb2f0c9052bee6af0e0a017b9ba8da2b8", + "opts": {}, + "name": "aesop", + "inputRev?": "master", + "inherited": false}}, {"git": {"url": "https://github.com/mhuisi/lean4-cli.git", "subDir?": null, @@ -28,17 +36,9 @@ {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "85a0d4891518518edfccee16cbceac139efa460c", + "rev": "45a53252c3b0c670e1a33ef55e262a9be626d820", "opts": {}, "name": "std", "inputRev?": "main", - "inherited": false}}, - {"git": - {"url": "https://github.com/JLimperg/aesop", - "subDir?": null, - "rev": "0bd8465d8a5cfdd53c1ff0fd57ca5eaa53eb455c", - "opts": {}, - "name": "aesop", - "inputRev?": "master", "inherited": false}}], "name": "mathlib"} diff --git a/lean-toolchain b/lean-toolchain index aac5c604dccb7..400394aaf22a1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.2.0-rc2 +leanprover/lean4:v4.2.0-rc1