[Merged by Bors] - chore: remove unnecessary @[eqns] attributes

Mathlib/Computability/TMToPartrec.lean

@@ -1240,9 +1240,6 @@ def K'.elim (a b c d : List Γ') : K' → List Γ'
   | K'.stack => d
 #align turing.partrec_to_TM2.K'.elim Turing.PartrecToTM2.K'.elim
 
-/- Porting note: The equation lemma of `elim` simplifies to `match` structures. To prevent this,
-we replace equation lemmas of `elim`. -/
-
 theorem K'.elim_main (a b c d) : K'.elim a b c d K'.main = a := rfl
 
 theorem K'.elim_rev (a b c d) : K'.elim a b c d K'.rev = b := rfl
@@ -1251,7 +1248,6 @@ theorem K'.elim_aux (a b c d) : K'.elim a b c d K'.aux = c := rfl
 
 theorem K'.elim_stack (a b c d) : K'.elim a b c d K'.stack = d := rfl
 
-attribute [eqns K'.elim_main K'.elim_rev K'.elim_aux K'.elim_stack] K'.elim
 attribute [simp] K'.elim
 
 @[simp]

Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

@@ -409,7 +409,7 @@ theorem withDensityᵥ_rnDeriv_eq (s : SignedMeasure α) (μ : Measure α) [Sigm
   rw [absolutelyContinuous_ennreal_iff, (_ : μ.toENNRealVectorMeasure.ennrealToMeasure = μ),
     totalVariation_absolutelyContinuous_iff] at h
   · ext1 i hi
-    rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv, integral_sub,
+    rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv_def, integral_sub,
       set_integral_toReal_rnDeriv h.1 i, set_integral_toReal_rnDeriv h.2 i]
     · conv_rhs => rw [← s.toSignedMeasure_toJordanDecomposition]
       erw [VectorMeasure.sub_apply]

Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean

@@ -178,20 +178,16 @@ def rnDeriv (s : SignedMeasure α) (μ : Measure α) : α → ℝ := fun x =>
     (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal
 #align measure_theory.signed_measure.rn_deriv MeasureTheory.SignedMeasure.rnDeriv
 
--- Porting note: The generated equation theorem is the form of `rnDeriv s μ x`.
-
 theorem rnDeriv_def (s : SignedMeasure α) (μ : Measure α) : rnDeriv s μ = fun x =>
     (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal -
       (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal :=
   rfl
 
-attribute [eqns rnDeriv_def] rnDeriv
-
 variable {s t : SignedMeasure α}
 
 @[measurability]
 theorem measurable_rnDeriv (s : SignedMeasure α) (μ : Measure α) : Measurable (rnDeriv s μ) := by
-  rw [rnDeriv]
+  rw [rnDeriv_def]
   measurability
 #align measure_theory.signed_measure.measurable_rn_deriv MeasureTheory.SignedMeasure.measurable_rnDeriv
 
@@ -213,7 +209,7 @@ theorem singularPart_add_withDensity_rnDeriv_eq [s.HaveLebesgueDecomposition μ]
     s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s := by
   conv_rhs =>
     rw [← toSignedMeasure_toJordanDecomposition s, JordanDecomposition.toSignedMeasure]
-  rw [singularPart, rnDeriv,
+  rw [singularPart, rnDeriv_def,
     withDensityᵥ_sub' (integrable_toReal_of_lintegral_ne_top _ _)
       (integrable_toReal_of_lintegral_ne_top _ _),
     withDensityᵥ_toReal, withDensityᵥ_toReal, sub_eq_add_neg, sub_eq_add_neg,

Mathlib/MeasureTheory/Function/L1Space.lean

@@ -112,8 +112,6 @@ theorem hasFiniteIntegral_def {_ : MeasurableSpace α} (f : α → β) (μ : Mea
     HasFiniteIntegral f μ ↔ ((∫⁻ a, ‖f a‖₊ ∂μ) < ∞) :=
   Iff.rfl
 
-attribute [eqns hasFiniteIntegral_def] HasFiniteIntegral
-
 theorem hasFiniteIntegral_iff_norm (f : α → β) :
     HasFiniteIntegral f μ ↔ (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) < ∞ := by
   simp only [HasFiniteIntegral, ofReal_norm_eq_coe_nnnorm]
@@ -446,8 +444,6 @@ theorem integrable_def {α} {_ : MeasurableSpace α} (f : α → β) (μ : Measu
     Integrable f μ ↔ (AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ) :=
   Iff.rfl
 
-attribute [eqns integrable_def] Integrable
-
 theorem memℒp_one_iff_integrable {f : α → β} : Memℒp f 1 μ ↔ Integrable f μ := by
   simp_rw [Integrable, HasFiniteIntegral, Memℒp, snorm_one_eq_lintegral_nnnorm]
 #align measure_theory.mem_ℒp_one_iff_integrable MeasureTheory.memℒp_one_iff_integrable

Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -109,13 +109,6 @@ def Memℒp {α} {_ : MeasurableSpace α} (f : α → E) (p : ℝ≥0∞)
   AEStronglyMeasurable f μ ∧ snorm f p μ < ∞
 #align measure_theory.mem_ℒp MeasureTheory.Memℒp
 
--- Porting note (#11215): TODO Delete this when leanprover/lean4#2243 is fixed.
-theorem memℒp_def {α} {_ : MeasurableSpace α} (f : α → E) (p : ℝ≥0∞) (μ : Measure α) :
-    Memℒp f p μ ↔ (AEStronglyMeasurable f μ ∧ snorm f p μ < ∞) :=
-  Iff.rfl
-
-attribute [eqns memℒp_def] Memℒp
-
 theorem Memℒp.aestronglyMeasurable {f : α → E} {p : ℝ≥0∞} (h : Memℒp f p μ) :
     AEStronglyMeasurable f μ :=
   h.1

Mathlib/MeasureTheory/Integral/IntegrableOn.lean

@@ -96,8 +96,6 @@ theorem integrableOn_def (f : α → E) (s : Set α) (μ : Measure α) :
     IntegrableOn f s μ ↔ Integrable f (μ.restrict s) :=
   Iff.rfl
 
-attribute [eqns integrableOn_def] IntegrableOn
-
 theorem IntegrableOn.integrable (h : IntegrableOn f s μ) : Integrable f (μ.restrict s) :=
   h
 #align measure_theory.integrable_on.integrable MeasureTheory.IntegrableOn.integrable