chore: re-add @[simp] attribute lost in the port (#18121)

This PR re-adds the `@[simp]` attributes that had a porting note that they could be proved by `@[simp]`, but where that does not appear to be the case currently. Of course, the `simp` set may have changed sufficiently to require un`@[simp]`ing some of these anyway, but we should add a more up to date comment in that case.
leanprover-community · Oct 25, 2024 · 1232423 · 1232423
1 parent d85e7db
commit 1232423
Show file tree

Hide file tree

Showing 16 changed files with 32 additions and 39 deletions.
diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -153,7 +153,6 @@ theorem cells_bot : (⊥ : YoungDiagram).cells = ∅ :=
   rfl
 
 -- Porting note: removed `↑`, added `.cells` and changed proof
--- @[simp] -- Porting note (#10618): simp can prove this
 @[norm_cast]
 theorem coe_bot : (⊥ : YoungDiagram).cells = (∅ : Set (ℕ × ℕ)) := by
   refine Set.eq_of_subset_of_subset ?_ ?_

diff --git a/Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean b/Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean
@@ -35,7 +35,7 @@ theorem uniqueMDiffOn_iff_uniqueDiffOn : UniqueMDiffOn 𝓘(𝕜, E) s ↔ Uniqu
 
 alias ⟨UniqueMDiffOn.uniqueDiffOn, UniqueDiffOn.uniqueMDiffOn⟩ := uniqueMDiffOn_iff_uniqueDiffOn
 
--- Porting note (#10618): was `@[simp, mfld_simps]` but `simp` can prove it
+@[simp, mfld_simps]
 theorem writtenInExtChartAt_model_space : writtenInExtChartAt 𝓘(𝕜, E) 𝓘(𝕜, E') x f = f :=
   rfl
 

diff --git a/Mathlib/GroupTheory/Perm/Sign.lean b/Mathlib/GroupTheory/Perm/Sign.lean
@@ -370,23 +370,23 @@ section SignType.sign
 
 variable [Fintype α]
 
---@[simp] Porting note (#10618): simp can prove
+@[simp]
 theorem sign_mul (f g : Perm α) : sign (f * g) = sign f * sign g :=
   MonoidHom.map_mul sign f g
 
 @[simp]
 theorem sign_trans (f g : Perm α) : sign (f.trans g) = sign g * sign f := by
   rw [← mul_def, sign_mul]
 
---@[simp] Porting note (#10618): simp can prove
+@[simp]
 theorem sign_one : sign (1 : Perm α) = 1 :=
   MonoidHom.map_one sign
 
 @[simp]
 theorem sign_refl : sign (Equiv.refl α) = 1 :=
   MonoidHom.map_one sign
 
---@[simp] Porting note (#10618): simp can prove
+@[simp]
 theorem sign_inv (f : Perm α) : sign f⁻¹ = sign f := by
   rw [MonoidHom.map_inv sign f, Int.units_inv_eq_self]
 

diff --git a/Mathlib/LinearAlgebra/Isomorphisms.lean b/Mathlib/LinearAlgebra/Isomorphisms.lean
@@ -149,7 +149,7 @@ theorem quotientQuotientEquivQuotientAux_mk (x : M ⧸ S) :
     quotientQuotientEquivQuotientAux S T h (Quotient.mk x) = mapQ S T LinearMap.id h x :=
   liftQ_apply _ _ _
 
--- @[simp] -- Porting note (#10618): simp can prove this
+@[simp]
 theorem quotientQuotientEquivQuotientAux_mk_mk (x : M) :
     quotientQuotientEquivQuotientAux S T h (Quotient.mk (Quotient.mk x)) = Quotient.mk x := by simp
 

diff --git a/Mathlib/Logic/Equiv/Defs.lean b/Mathlib/Logic/Equiv/Defs.lean
@@ -599,7 +599,7 @@ theorem psigmaCongrRight_trans {α} {β₁ β₂ β₃ : α → Sort*}
 theorem psigmaCongrRight_symm {α} {β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) :
     (psigmaCongrRight F).symm = psigmaCongrRight fun a => (F a).symm := rfl
 
--- Porting note (#10618): simp can now prove this, so I have removed `@[simp]`
+@[simp]
 theorem psigmaCongrRight_refl {α} {β : α → Sort*} :
     (psigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl (Σ' a, β a) := rfl
 
@@ -620,7 +620,7 @@ theorem sigmaCongrRight_trans {α} {β₁ β₂ β₃ : α → Type*}
 theorem sigmaCongrRight_symm {α} {β₁ β₂ : α → Type*} (F : ∀ a, β₁ a ≃ β₂ a) :
     (sigmaCongrRight F).symm = sigmaCongrRight fun a => (F a).symm := rfl
 
--- Porting note (#10618): simp can now prove this, so I have removed `@[simp]`
+@[simp]
 theorem sigmaCongrRight_refl {α} {β : α → Type*} :
     (sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl (Σ a, β a) := rfl
 

diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
@@ -120,7 +120,7 @@ theorem intervalIntegrable_const_iff {c : E} :
     IntervalIntegrable (fun _ => c) μ a b ↔ c = 0 ∨ μ (Ι a b) < ∞ := by
   simp only [intervalIntegrable_iff, integrableOn_const]
 
-@[simp] -- Porting note (#10618): simp can prove this
+@[simp]
 theorem intervalIntegrable_const [IsLocallyFiniteMeasure μ] {c : E} :
     IntervalIntegrable (fun _ => c) μ a b :=
   intervalIntegrable_const_iff.2 <| Or.inr measure_Ioc_lt_top

diff --git a/Mathlib/MeasureTheory/Measure/NullMeasurable.lean b/Mathlib/MeasureTheory/Measure/NullMeasurable.lean
@@ -171,7 +171,6 @@ protected theorem disjointed {f : ℕ → Set α} (h : ∀ i, NullMeasurableSet
     NullMeasurableSet (disjointed f n) μ :=
   MeasurableSet.disjointed h n
 
--- @[simp] -- Porting note (#10618): simp can prove thisrove this
 protected theorem const (p : Prop) : NullMeasurableSet { _a : α | p } μ :=
   MeasurableSet.const p
 

diff --git a/Mathlib/RingTheory/AlgebraicIndependent.lean b/Mathlib/RingTheory/AlgebraicIndependent.lean
@@ -363,13 +363,17 @@ theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply
         (aeval (fun o : Option ι => o.elim Polynomial.X fun s : ι => Polynomial.C (X s)) y) :=
   rfl
 
---@[simp] Porting note: removing simp because the linter complains about deterministic timeout
+/-- `simp`-normal form of `mvPolynomialOptionEquivPolynomialAdjoin_C` -/
+@[simp]
+theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C'
+    (hx : AlgebraicIndependent R x) (r) :
+    Polynomial.C (hx.aevalEquiv (C r)) = Polynomial.C (algebraMap _ _ r) := by
+  simp [aevalEquiv]
+
 theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C
     (hx : AlgebraicIndependent R x) (r) :
     hx.mvPolynomialOptionEquivPolynomialAdjoin (C r) = Polynomial.C (algebraMap _ _ r) := by
-  rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_C,
-    IsScalarTower.algebraMap_apply R (MvPolynomial ι R), ← Polynomial.C_eq_algebraMap,
-    Polynomial.map_C, RingHom.coe_coe, AlgEquiv.commutes]
+  simp
 
 theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none
     (hx : AlgebraicIndependent R x) :

diff --git a/Mathlib/RingTheory/MvPowerSeries/Basic.lean b/Mathlib/RingTheory/MvPowerSeries/Basic.lean
@@ -177,8 +177,7 @@ theorem eq_of_coeff_monomial_ne_zero {m n : σ →₀ ℕ} {a : R} (h : coeff R
 theorem coeff_comp_monomial (n : σ →₀ ℕ) : (coeff R n).comp (monomial R n) = LinearMap.id :=
   LinearMap.ext <| coeff_monomial_same n
 
--- Porting note (#10618): simp can prove this.
--- @[simp]
+@[simp]
 theorem coeff_zero (n : σ →₀ ℕ) : coeff R n (0 : MvPowerSeries σ R) = 0 :=
   rfl
 
@@ -434,13 +433,11 @@ theorem constantCoeff_C (a : R) : constantCoeff σ R (C σ R a) = a :=
 theorem constantCoeff_comp_C : (constantCoeff σ R).comp (C σ R) = RingHom.id R :=
   rfl
 
--- Porting note (#10618): simp can prove this.
--- @[simp]
+@[simp]
 theorem constantCoeff_zero : constantCoeff σ R 0 = 0 :=
   rfl
 
--- Porting note (#10618): simp can prove this.
--- @[simp]
+@[simp]
 theorem constantCoeff_one : constantCoeff σ R 1 = 1 :=
   rfl
 
@@ -454,8 +451,7 @@ theorem isUnit_constantCoeff (φ : MvPowerSeries σ R) (h : IsUnit φ) :
     IsUnit (constantCoeff σ R φ) :=
   h.map _
 
--- Porting note (#10618): simp can prove this.
--- @[simp]
+@[simp]
 theorem coeff_smul (f : MvPowerSeries σ R) (n) (a : R) : coeff _ n (a • f) = a * coeff _ n f :=
   rfl
 

diff --git a/Mathlib/RingTheory/MvPowerSeries/Inverse.lean b/Mathlib/RingTheory/MvPowerSeries/Inverse.lean
@@ -228,8 +228,7 @@ theorem inv_eq_zero {φ : MvPowerSeries σ k} : φ⁻¹ = 0 ↔ constantCoeff σ
 theorem zero_inv : (0 : MvPowerSeries σ k)⁻¹ = 0 := by
   rw [inv_eq_zero, constantCoeff_zero]
 
--- Porting note (#10618): simp can prove this.
--- @[simp]
+@[simp]
 theorem invOfUnit_eq (φ : MvPowerSeries σ k) (h : constantCoeff σ k φ ≠ 0) :
     invOfUnit φ (Units.mk0 _ h) = φ⁻¹ :=
   rfl

diff --git a/Mathlib/RingTheory/PowerSeries/Basic.lean b/Mathlib/RingTheory/PowerSeries/Basic.lean
@@ -327,13 +327,11 @@ theorem constantCoeff_C (a : R) : constantCoeff R (C R a) = a :=
 theorem constantCoeff_comp_C : (constantCoeff R).comp (C R) = RingHom.id R :=
   rfl
 
--- Porting note (#10618): simp can prove this.
--- @[simp]
+@[simp]
 theorem constantCoeff_zero : constantCoeff R 0 = 0 :=
   rfl
 
--- Porting note (#10618): simp can prove this.
--- @[simp]
+@[simp]
 theorem constantCoeff_one : constantCoeff R 1 = 1 :=
   rfl
 

diff --git a/Mathlib/RingTheory/PowerSeries/Inverse.lean b/Mathlib/RingTheory/PowerSeries/Inverse.lean
@@ -150,8 +150,7 @@ theorem inv_eq_zero {φ : k⟦X⟧} : φ⁻¹ = 0 ↔ constantCoeff k φ = 0 :=
 theorem zero_inv : (0 : k⟦X⟧)⁻¹ = 0 :=
   MvPowerSeries.zero_inv
 
--- Porting note (#10618): simp can prove this.
--- @[simp]
+@[simp]
 theorem invOfUnit_eq (φ : k⟦X⟧) (h : constantCoeff k φ ≠ 0) :
     invOfUnit φ (Units.mk0 _ h) = φ⁻¹ :=
   MvPowerSeries.invOfUnit_eq _ _

diff --git a/Mathlib/SetTheory/Cardinal/ToNat.lean b/Mathlib/SetTheory/Cardinal/ToNat.lean
@@ -116,8 +116,7 @@ theorem aleph0_toNat : toNat ℵ₀ = 0 :=
 
 theorem mk_toNat_eq_card [Fintype α] : toNat #α = Fintype.card α := by simp
 
--- porting note (#10618): simp can prove this
--- @[simp]
+@[simp]
 theorem zero_toNat : toNat 0 = 0 := map_zero _
 
 theorem one_toNat : toNat 1 = 1 := map_one _

diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean
@@ -436,7 +436,7 @@ protected theorem map_zero (f : M₁ →SL[σ₁₂] M₂) : f (0 : M₁) = 0 :=
 protected theorem map_add (f : M₁ →SL[σ₁₂] M₂) (x y : M₁) : f (x + y) = f x + f y :=
   map_add f x y
 
--- @[simp] -- Porting note (#10618): simp can prove this
+@[simp]
 protected theorem map_smulₛₗ (f : M₁ →SL[σ₁₂] M₂) (c : R₁) (x : M₁) : f (c • x) = σ₁₂ c • f x :=
   (toLinearMap _).map_smulₛₗ _ _
 
@@ -1681,7 +1681,7 @@ theorem map_zero (e : M₁ ≃SL[σ₁₂] M₂) : e (0 : M₁) = 0 :=
 theorem map_add (e : M₁ ≃SL[σ₁₂] M₂) (x y : M₁) : e (x + y) = e x + e y :=
   (e : M₁ →SL[σ₁₂] M₂).map_add x y
 
--- @[simp] -- Porting note (#10618): simp can prove this
+@[simp]
 theorem map_smulₛₗ (e : M₁ ≃SL[σ₁₂] M₂) (c : R₁) (x : M₁) : e (c • x) = σ₁₂ c • e x :=
   (e : M₁ →SL[σ₁₂] M₂).map_smulₛₗ c x
 

diff --git a/Mathlib/Topology/Category/TopCat/Basic.lean b/Mathlib/Topology/Category/TopCat/Basic.lean
@@ -53,10 +53,10 @@ instance instFunLike (X Y : TopCat) : FunLike (X ⟶ Y) X Y :=
 instance instContinuousMapClass (X Y : TopCat) : ContinuousMapClass (X ⟶ Y) X Y :=
   inferInstanceAs <| ContinuousMapClass C(X, Y) X Y
 
--- Porting note (#10618): simp can prove this; removed simp
+@[simp]
 theorem id_app (X : TopCat.{u}) (x : ↑X) : (𝟙 X : X ⟶ X) x = x := rfl
 
--- Porting note (#10618): simp can prove this; removed simp
+@[simp]
 theorem comp_app {X Y Z : TopCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
     (f ≫ g : X → Z) x = g (f x) := rfl
 

diff --git a/Mathlib/Topology/UniformSpace/Equiv.lean b/Mathlib/Topology/UniformSpace/Equiv.lean
@@ -178,7 +178,7 @@ theorem symm_comp_self (h : α ≃ᵤ β) : (h.symm : β → α) ∘ h = id :=
 theorem self_comp_symm (h : α ≃ᵤ β) : (h : α → β) ∘ h.symm = id :=
   funext h.apply_symm_apply
 
--- @[simp] -- Porting note (#10618): `simp` can prove this `simp only [Equiv.range_eq_univ]`
+@[simp]
 theorem range_coe (h : α ≃ᵤ β) : range h = univ :=
   h.surjective.range_eq
 
@@ -188,11 +188,11 @@ theorem image_symm (h : α ≃ᵤ β) : image h.symm = preimage h :=
 theorem preimage_symm (h : α ≃ᵤ β) : preimage h.symm = image h :=
   (funext h.toEquiv.image_eq_preimage).symm
 
--- @[simp] -- Porting note (#10618): `simp` can prove this `simp only [Equiv.image_preimage]`
+@[simp]
 theorem image_preimage (h : α ≃ᵤ β) (s : Set β) : h '' (h ⁻¹' s) = s :=
   h.toEquiv.image_preimage s
 
---@[simp] -- Porting note (#10618): `simp` can prove this `simp only [Equiv.preimage_image]`
+@[simp]
 theorem preimage_image (h : α ≃ᵤ β) (s : Set α) : h ⁻¹' (h '' s) = s :=
   h.toEquiv.preimage_image s