diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian.lean
index 1dae80d20c38f..5a738b21716c8 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gaussian.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gaussian.lean
@@ -118,7 +118,7 @@ theorem integrableOn_rpow_mul_exp_neg_mul_rpow {p s b : ℝ} (hs : -1 < s) (hp :
       rpow_neg_one, mul_inv_cancel_left₀]
     all_goals linarith [mem_Ioi.mp hx]
   refine Integrable.const_mul ?_ _
-  rw [← integrableOn_def]
+  rw [← IntegrableOn]
   exact integrableOn_rpow_mul_exp_neg_rpow hs hp
 
 theorem integrableOn_rpow_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) {s : ℝ} (hs : -1 < s) :
diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean
index 2d2157c403462..fe5a802203321 100644
--- a/Mathlib/Computability/TMToPartrec.lean
+++ b/Mathlib/Computability/TMToPartrec.lean
@@ -1240,8 +1240,7 @@ 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`. -/
+-- The equation lemma of `elim` simplifies to `match` structures.
 
 theorem K'.elim_main (a b c d) : K'.elim a b c d K'.main = a := rfl
 
@@ -1251,7 +1250,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]
diff --git a/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean b/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
index b0287cdfd5b78..d9e9cfc91b42f 100644
--- a/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
+++ b/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]
diff --git a/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean b/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
index a5b8a1c4047fd..8c43a934ad08c 100644
--- a/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
+++ b/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
@@ -178,20 +178,17 @@ 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`.
-
+-- 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 +210,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,
diff --git a/Mathlib/MeasureTheory/Function/L1Space.lean b/Mathlib/MeasureTheory/Function/L1Space.lean
index 8d0c6a7304e5c..2ed79069a585c 100644
--- a/Mathlib/MeasureTheory/Function/L1Space.lean
+++ b/Mathlib/MeasureTheory/Function/L1Space.lean
@@ -110,8 +110,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]
@@ -440,12 +438,6 @@ def Integrable {α} {_ : MeasurableSpace α} (f : α → β) (μ : Measure α :=
   AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
 #align measure_theory.integrable MeasureTheory.Integrable
 
-theorem integrable_def {α} {_ : MeasurableSpace α} (f : α → β) (μ : Measure α) :
-    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
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
index e4c7b7f0ead0e..b3f587301859a 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
+++ b/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
diff --git a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean
index b5a6d52bae931..b3f433032c923 100644
--- a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean
+++ b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean
@@ -91,13 +91,6 @@ def IntegrableOn (f : α → E) (s : Set α) (μ : Measure α := by volume_tac)
   Integrable f (μ.restrict s)
 #align measure_theory.integrable_on MeasureTheory.IntegrableOn
 
--- Porting note (#11215): TODO Delete this when leanprover/lean4#2243 is fixed.
-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
diff --git a/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean b/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
index a39e97ff26d35..39c07dc24008f 100644
--- a/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
+++ b/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
@@ -360,10 +360,10 @@ lemma f_modif_aux2 {s : ℂ} (hs : P.k < re s) :
         - P.ε • (∫ (x : ℝ) in Ioc 0 1, (x : ℂ) ^ (s - P.k - 1)) • P.g₀ := by
     rw [integral_sub, integral_smul, integral_smul_const, integral_smul_const]
     · apply Integrable.smul_const
-      rw [← integrableOn_def, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
+      rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
       exact intervalIntegral.intervalIntegrable_cpow' h_re1
     · refine (Integrable.smul_const ?_ _).smul _
-      rw [← integrableOn_def, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
+      rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
       exact intervalIntegral.intervalIntegrable_cpow' h_re2
   _ = _ := by simp_rw [← intervalIntegral.integral_of_le zero_le_one,
       integral_cpow (Or.inl h_re1), integral_cpow (Or.inl h_re2), ofReal_zero, ofReal_one,
diff --git a/Mathlib/Probability/Distributions/Exponential.lean b/Mathlib/Probability/Distributions/Exponential.lean
index 0e032b448eeff..e080e5e42c661 100644
--- a/Mathlib/Probability/Distributions/Exponential.lean
+++ b/Mathlib/Probability/Distributions/Exponential.lean
@@ -156,7 +156,7 @@ lemma lintegral_exponentialPDF_eq_antiDeriv {r : ℝ} (hr : 0 < r) (x : ℝ) :
     · simp only [neg_mul, one_mul]
       exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
     · apply Integrable.aestronglyMeasurable (Integrable.const_mul _ _)
-      rw [← integrableOn_def, integrableOn_Icc_iff_integrableOn_Ioc]
+      rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
       exact exp_neg_integrableOn_Ioc hr
     · refine ne_of_lt (IntegrableOn.set_lintegral_lt_top ?_)
       rw [integrableOn_Icc_iff_integrableOn_Ioc]