From 2457833a348168478e38b033a047d70e7805de5c Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Tue, 5 Mar 2024 22:19:29 +0000 Subject: [PATCH] chore: classify `@[simp] removed` porting notes (#11184) Classifying by adding issue number #11119 to porting notes claiming anything semantically equivalent to: - "`@[simp]` removed [...]" - "@[simp] removed [...]" - "removed `simp` attribute" --- Mathlib/Algebra/Group/WithOne/Basic.lean | 2 +- Mathlib/Algebra/Invertible/Basic.lean | 2 +- Mathlib/Algebra/Star/Basic.lean | 2 +- Mathlib/Data/Int/Interval.lean | 8 ++++---- Mathlib/Data/Set/Basic.lean | 16 ++++++++-------- Mathlib/Geometry/RingedSpace/Stalks.lean | 2 +- Mathlib/GroupTheory/GroupAction/ConjAct.lean | 12 ++++++------ Mathlib/Logic/Equiv/Set.lean | 2 +- Mathlib/Order/Filter/Pointwise.lean | 14 +++++++++----- Mathlib/Topology/Category/UniformSpace.lean | 3 ++- Mathlib/Topology/Sheaves/LocalPredicate.lean | 3 ++- 11 files changed, 36 insertions(+), 30 deletions(-) diff --git a/Mathlib/Algebra/Group/WithOne/Basic.lean b/Mathlib/Algebra/Group/WithOne/Basic.lean index a19f23a5e3a39b..503ba05bceace4 100644 --- a/Mathlib/Algebra/Group/WithOne/Basic.lean +++ b/Mathlib/Algebra/Group/WithOne/Basic.lean @@ -82,7 +82,7 @@ theorem lift_coe (x : α) : lift f x = f x := #align with_one.lift_coe WithOne.lift_coe #align with_zero.lift_coe WithZero.lift_coe --- Porting note: removed `simp` attribute to appease `simpNF` linter. +-- Porting note (#11119): removed `simp` attribute to appease `simpNF` linter. @[to_additive] theorem lift_one : lift f 1 = 1 := rfl diff --git a/Mathlib/Algebra/Invertible/Basic.lean b/Mathlib/Algebra/Invertible/Basic.lean index a05e5fb1968396..aac695f7798fa2 100644 --- a/Mathlib/Algebra/Invertible/Basic.lean +++ b/Mathlib/Algebra/Invertible/Basic.lean @@ -213,7 +213,7 @@ def invertibleDiv (a b : α) [Invertible a] [Invertible b] : Invertible (a / b) ⟨b / a, by simp [← mul_div_assoc], by simp [← mul_div_assoc]⟩ #align invertible_div invertibleDiv --- Porting note: removed `simp` attribute as `simp` can prove it +-- Porting note (#11119): removed `simp` attribute as `simp` can prove it theorem invOf_div (a b : α) [Invertible a] [Invertible b] [Invertible (a / b)] : ⅟ (a / b) = b / a := invOf_eq_right_inv (by simp [← mul_div_assoc]) diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean index 0aefe8415c9d5e..b5d00b3ba2752d 100644 --- a/Mathlib/Algebra/Star/Basic.lean +++ b/Mathlib/Algebra/Star/Basic.lean @@ -390,7 +390,7 @@ scoped[ComplexConjugate] notation "conj" => starRingEnd _ theorem starRingEnd_apply (x : R) : starRingEnd R x = star x := rfl #align star_ring_end_apply starRingEnd_apply -/- Porting note: removed `simp` attribute due to report by linter: +/- Porting note (#11119): removed `simp` attribute due to report by linter: simp can prove this: by simp only [RingHomCompTriple.comp_apply, RingHom.id_apply] diff --git a/Mathlib/Data/Int/Interval.lean b/Mathlib/Data/Int/Interval.lean index b8b9860eaef71f..b469b84060c6a5 100644 --- a/Mathlib/Data/Int/Interval.lean +++ b/Mathlib/Data/Int/Interval.lean @@ -147,22 +147,22 @@ theorem card_Ioo_of_lt (h : a < b) : ((Ioo a b).card : ℤ) = b - a - 1 := by rw [card_Ioo, sub_sub, toNat_sub_of_le h] #align int.card_Ioo_of_lt Int.card_Ioo_of_lt --- Porting note: removed `simp` attribute because `simpNF` says it can prove it +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it theorem card_fintype_Icc : Fintype.card (Set.Icc a b) = (b + 1 - a).toNat := by rw [← card_Icc, Fintype.card_ofFinset] #align int.card_fintype_Icc Int.card_fintype_Icc --- Porting note: removed `simp` attribute because `simpNF` says it can prove it +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it theorem card_fintype_Ico : Fintype.card (Set.Ico a b) = (b - a).toNat := by rw [← card_Ico, Fintype.card_ofFinset] #align int.card_fintype_Ico Int.card_fintype_Ico --- Porting note: removed `simp` attribute because `simpNF` says it can prove it +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it theorem card_fintype_Ioc : Fintype.card (Set.Ioc a b) = (b - a).toNat := by rw [← card_Ioc, Fintype.card_ofFinset] #align int.card_fintype_Ioc Int.card_fintype_Ioc --- Porting note: removed `simp` attribute because `simpNF` says it can prove it +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it theorem card_fintype_Ioo : Fintype.card (Set.Ioo a b) = (b - a - 1).toNat := by rw [← card_Ioo, Fintype.card_ofFinset] #align int.card_fintype_Ioo Int.card_fintype_Ioo diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index acad0f0c6177ea..f1d8ecb5d1a4c0 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -1255,7 +1255,7 @@ theorem setOf_eq_eq_singleton' {a : α} : { x | a = x } = {a} := #align set.set_of_eq_eq_singleton' Set.setOf_eq_eq_singleton' -- TODO: again, annotation needed --- Porting note: removed `simp` attribute +--Porting note (#11119): removed `simp` attribute theorem mem_singleton (a : α) : a ∈ ({a} : Set α) := @rfl _ _ #align set.mem_singleton Set.mem_singleton @@ -1291,7 +1291,7 @@ theorem singleton_ne_empty (a : α) : ({a} : Set α) ≠ ∅ := (singleton_nonempty _).ne_empty #align set.singleton_ne_empty Set.singleton_ne_empty --- Porting note: removed `simp` attribute because `simp` can prove it +--Porting note (#11119): removed `simp` attribute because `simp` can prove it theorem empty_ssubset_singleton : (∅ : Set α) ⊂ {a} := (singleton_nonempty _).empty_ssubset #align set.empty_ssubset_singleton Set.empty_ssubset_singleton @@ -1364,7 +1364,7 @@ theorem default_coe_singleton (x : α) : (default : ({x} : Set α)) = ⟨x, rfl /-! ### Lemmas about pairs -/ --- Porting note: removed `simp` attribute because `simp` can prove it +--Porting note (#11119): removed `simp` attribute because `simp` can prove it theorem pair_eq_singleton (a : α) : ({a, a} : Set α) = {a} := union_self _ #align set.pair_eq_singleton Set.pair_eq_singleton @@ -1426,22 +1426,22 @@ theorem sep_eq_empty_iff_mem_false : { x ∈ s | p x } = ∅ ↔ ∀ x ∈ s, ¬ simp_rw [ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false_iff, not_and] #align set.sep_eq_empty_iff_mem_false Set.sep_eq_empty_iff_mem_false --- Porting note: removed `simp` attribute because `simp` can prove it +--Porting note (#11119): removed `simp` attribute because `simp` can prove it theorem sep_true : { x ∈ s | True } = s := inter_univ s #align set.sep_true Set.sep_true --- Porting note: removed `simp` attribute because `simp` can prove it +--Porting note (#11119): removed `simp` attribute because `simp` can prove it theorem sep_false : { x ∈ s | False } = ∅ := inter_empty s #align set.sep_false Set.sep_false --- Porting note: removed `simp` attribute because `simp` can prove it +--Porting note (#11119): removed `simp` attribute because `simp` can prove it theorem sep_empty (p : α → Prop) : { x ∈ (∅ : Set α) | p x } = ∅ := empty_inter p #align set.sep_empty Set.sep_empty --- Porting note: removed `simp` attribute because `simp` can prove it +--Porting note (#11119): removed `simp` attribute because `simp` can prove it theorem sep_univ : { x ∈ (univ : Set α) | p x } = { x | p x } := univ_inter p #align set.sep_univ Set.sep_univ @@ -2055,7 +2055,7 @@ theorem insert_diff_singleton_comm (hab : a ≠ b) (s : Set α) : diff_singleton_eq_self (mem_singleton_iff.not.2 hab.symm)] #align set.insert_diff_singleton_comm Set.insert_diff_singleton_comm --- Porting note: removed `simp` attribute because `simp` can prove it +--Porting note (#11119): removed `simp` attribute because `simp` can prove it theorem diff_self {s : Set α} : s \ s = ∅ := sdiff_self #align set.diff_self Set.diff_self diff --git a/Mathlib/Geometry/RingedSpace/Stalks.lean b/Mathlib/Geometry/RingedSpace/Stalks.lean index 69d78647590976..6e878962f83b3e 100644 --- a/Mathlib/Geometry/RingedSpace/Stalks.lean +++ b/Mathlib/Geometry/RingedSpace/Stalks.lean @@ -82,7 +82,7 @@ def restrictStalkIso {U : TopCat} (X : PresheafedSpace.{_, _, v} C) {f : U ⟶ ( set_option linter.uppercaseLean3 false in #align algebraic_geometry.PresheafedSpace.restrict_stalk_iso AlgebraicGeometry.PresheafedSpace.restrictStalkIso --- Porting note: removed `simp` attribute, for left hand side is not in simple normal form. +-- Porting note (#11119): removed `simp` attribute, for left hand side is not in simple normal form. @[elementwise, reassoc] theorem restrictStalkIso_hom_eq_germ {U : TopCat} (X : PresheafedSpace.{_, _, v} C) {f : U ⟶ (X : TopCat.{v})} (h : OpenEmbedding f) (V : Opens U) (x : U) (hx : x ∈ V) : diff --git a/Mathlib/GroupTheory/GroupAction/ConjAct.lean b/Mathlib/GroupTheory/GroupAction/ConjAct.lean index 0a7af8618d2bb0..5708d1470a4790 100644 --- a/Mathlib/GroupTheory/GroupAction/ConjAct.lean +++ b/Mathlib/GroupTheory/GroupAction/ConjAct.lean @@ -111,12 +111,12 @@ theorem ofConjAct_toConjAct (x : G) : ofConjAct (toConjAct x) = x := rfl #align conj_act.of_conj_act_to_conj_act ConjAct.ofConjAct_toConjAct --- Porting note: removed `simp` attribute because `simpNF` says it can prove it +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it theorem ofConjAct_one : ofConjAct (1 : ConjAct G) = 1 := rfl #align conj_act.of_conj_act_one ConjAct.ofConjAct_one --- Porting note: removed `simp` attribute because `simpNF` says it can prove it +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it theorem toConjAct_one : toConjAct (1 : G) = 1 := rfl #align conj_act.to_conj_act_one ConjAct.toConjAct_one @@ -131,12 +131,12 @@ theorem toConjAct_inv (x : G) : toConjAct x⁻¹ = (toConjAct x)⁻¹ := rfl #align conj_act.to_conj_act_inv ConjAct.toConjAct_inv --- Porting note: removed `simp` attribute because `simpNF` says it can prove it +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it theorem ofConjAct_mul (x y : ConjAct G) : ofConjAct (x * y) = ofConjAct x * ofConjAct y := rfl #align conj_act.of_conj_act_mul ConjAct.ofConjAct_mul --- Porting note: removed `simp` attribute because `simpNF` says it can prove it +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it theorem toConjAct_mul (x y : G) : toConjAct (x * y) = toConjAct x * toConjAct y := rfl #align conj_act.to_conj_act_mul ConjAct.toConjAct_mul @@ -213,12 +213,12 @@ section GroupWithZero variable [GroupWithZero G₀] --- Porting note: removed `simp` attribute because `simpNF` says it can prove it +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it theorem ofConjAct_zero : ofConjAct (0 : ConjAct G₀) = 0 := rfl #align conj_act.of_conj_act_zero ConjAct.ofConjAct_zero --- Porting note: removed `simp` attribute because `simpNF` says it can prove it +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it theorem toConjAct_zero : toConjAct (0 : G₀) = 0 := rfl #align conj_act.to_conj_act_zero ConjAct.toConjAct_zero diff --git a/Mathlib/Logic/Equiv/Set.lean b/Mathlib/Logic/Equiv/Set.lean index 82df093491387d..3937bf4b4dfc01 100644 --- a/Mathlib/Logic/Equiv/Set.lean +++ b/Mathlib/Logic/Equiv/Set.lean @@ -122,7 +122,7 @@ theorem preimage_subset {α β} (e : α ≃ β) (s t : Set β) : e ⁻¹' s ⊆ e.surjective.preimage_subset_preimage_iff #align equiv.preimage_subset Equiv.preimage_subset --- Porting note: Removed `simp` attribute. `simp` can prove it. +-- Porting note (#11119): removed `simp` attribute. `simp` can prove it. theorem image_subset {α β} (e : α ≃ β) (s t : Set α) : e '' s ⊆ e '' t ↔ s ⊆ t := image_subset_image_iff e.injective #align equiv.image_subset Equiv.image_subset diff --git a/Mathlib/Order/Filter/Pointwise.lean b/Mathlib/Order/Filter/Pointwise.lean index 24f6595e485f7b..ad14f36e9833e5 100644 --- a/Mathlib/Order/Filter/Pointwise.lean +++ b/Mathlib/Order/Filter/Pointwise.lean @@ -167,7 +167,8 @@ theorem pureOneHom_apply (a : α) : pureOneHom a = pure a := variable [One β] -@[to_additive] -- Porting note: removed `simp` attribute because `simpNF` says it can prove it. +@[to_additive] +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it. protected theorem map_one [FunLike F α β] [OneHomClass F α β] (φ : F) : map φ 1 = 1 := by rw [Filter.map_one', map_one, pure_one] #align filter.map_one Filter.map_one @@ -375,7 +376,8 @@ theorem mul_pure : f * pure b = f.map (· * b) := #align filter.mul_pure Filter.mul_pure #align filter.add_pure Filter.add_pure -@[to_additive] -- Porting note: removed `simp` attribute because `simpNF` says it can prove it. +@[to_additive] +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it. theorem pure_mul_pure : (pure a : Filter α) * pure b = pure (a * b) := map₂_pure #align filter.pure_mul_pure Filter.pure_mul_pure @@ -521,7 +523,8 @@ theorem div_pure : f / pure b = f.map (· / b) := #align filter.div_pure Filter.div_pure #align filter.sub_pure Filter.sub_pure -@[to_additive] -- Porting note: removed `simp` attribute because `simpNF` says it can prove it. +@[to_additive] +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it. theorem pure_div_pure : (pure a : Filter α) / pure b = pure (a / b) := map₂_pure #align filter.pure_div_pure Filter.pure_div_pure @@ -1051,7 +1054,8 @@ theorem smul_pure : f • pure b = f.map (· • b) := #align filter.smul_pure Filter.smul_pure #align filter.vadd_pure Filter.vadd_pure -@[to_additive] -- Porting note: removed `simp` attribute because `simpNF` says it can prove it. +@[to_additive] +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it. theorem pure_smul_pure : (pure a : Filter α) • (pure b : Filter β) = pure (a • b) := map₂_pure #align filter.pure_smul_pure Filter.pure_smul_pure @@ -1164,7 +1168,7 @@ theorem vsub_pure : f -ᵥ pure b = f.map (· -ᵥ b) := map₂_pure_right #align filter.vsub_pure Filter.vsub_pure --- Porting note: removed `simp` attribute because `simpNF` says it can prove it. +-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it. theorem pure_vsub_pure : (pure a : Filter β) -ᵥ pure b = (pure (a -ᵥ b) : Filter α) := map₂_pure #align filter.pure_vsub_pure Filter.pure_vsub_pure diff --git a/Mathlib/Topology/Category/UniformSpace.lean b/Mathlib/Topology/Category/UniformSpace.lean index 4223c808c28e29..d7dc2124927f45 100644 --- a/Mathlib/Topology/Category/UniformSpace.lean +++ b/Mathlib/Topology/Category/UniformSpace.lean @@ -79,7 +79,8 @@ theorem coe_id (X : UniformSpaceCat) : (𝟙 X : X → X) = id := rfl #align UniformSpace.coe_id UniformSpaceCat.coe_id --- Porting note: removed `simp` attribute due to `LEFT-HAND SIDE HAS VARIABLE AS HEAD SYMBOL.` +-- Porting note (#11119): removed `simp` attribute +-- due to `LEFT-HAND SIDE HAS VARIABLE AS HEAD SYMBOL.` theorem coe_mk {X Y : UniformSpaceCat} (f : X → Y) (hf : UniformContinuous f) : ((⟨f, hf⟩ : X ⟶ Y) : X → Y) = f := rfl diff --git a/Mathlib/Topology/Sheaves/LocalPredicate.lean b/Mathlib/Topology/Sheaves/LocalPredicate.lean index 398d856b4eef08..ef00a689d3c502 100644 --- a/Mathlib/Topology/Sheaves/LocalPredicate.lean +++ b/Mathlib/Topology/Sheaves/LocalPredicate.lean @@ -244,7 +244,8 @@ def stalkToFiber (P : LocalPredicate T) (x : X) : (subsheafToTypes P).presheaf.s set_option linter.uppercaseLean3 false in #align Top.stalk_to_fiber TopCat.stalkToFiber --- Porting note: removed `simp` attribute, due to left hand side is not in simple normal form. +-- Porting note (#11119): removed `simp` attribute, +-- due to left hand side is not in simple normal form. theorem stalkToFiber_germ (P : LocalPredicate T) (U : Opens X) (x : U) (f) : stalkToFiber P x ((subsheafToTypes P).presheaf.germ x f) = f.1 x := by dsimp [Presheaf.germ, stalkToFiber]