diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/H1.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/H1.lean
index fcec4d8..6fa9227 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/H1.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/H1.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2026 Adam Benenson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Benenson
+-/
+
 import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Analysis.Calculus.FDeriv.Const
 import Mathlib.Analysis.InnerProductSpace.Dual
@@ -5,12 +11,6 @@ import Mathlib.MeasureTheory.Function.LpSpace.Complete
 import Mathlib.MeasureTheory.Function.LpSpace.Indicator
 import Mathlib.Topology.Algebra.Support
 
-/-
-Copyright (c) 2026 Adam Benenson. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Adam Benenson
--/
-
 /-!
 # `RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.H1`
 
@@ -55,15 +55,19 @@ section
 variable
   {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
 
-local instance : MeasurableSpace E := borel E
-local instance : BorelSpace E := ⟨rfl⟩
-local instance : OpensMeasurableSpace E := by infer_instance
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceH1 : MeasurableSpace E := borel E
+local instance instBorelSpaceH1 : BorelSpace E := ⟨rfl⟩
+local instance instOpensMeasurableSpaceH1 : OpensMeasurableSpace E := by infer_instance
 
 variable (μ : Measure E) [IsFiniteMeasureOnCompacts μ]
 
-private abbrev L2ℝ : Type _ := ↥(E →₂[μ] ℝ)
-private abbrev L2E : Type _ := ↥(E →₂[μ] E)
-private abbrev H1Target : Type _ := L2ℝ (μ := μ) × L2E (μ := μ)
+/-- The space of square-integrable real-valued functions. -/
+abbrev L2ℝ : Type _ := ↥(E →₂[μ] ℝ)
+/-- The space of square-integrable vector-valued functions. -/
+abbrev L2E : Type _ := ↥(E →₂[μ] E)
+/-- The product space containing a function and its first derivative. -/
+abbrev H1Target : Type _ := L2ℝ (μ := μ) × L2E (μ := μ)
 
 /-- `C¹` real-valued functions on `E` with compact support, as a submodule of `E → ℝ`. -/
 def C1c : Submodule ℝ (E → ℝ) where
@@ -78,7 +82,7 @@ def C1c : Submodule ℝ (E → ℝ) where
     intro c f hf
     refine ⟨hf.1.const_smul c, ?_⟩
     -- `HasCompactSupport` is stable under pointwise scalar multiplication.
-    simpa using (HasCompactSupport.smul_left (f := fun _ : E => c) hf.2)
+    exact (HasCompactSupport.smul_left (f := fun _ : E => c) hf.2)
 
 /-- The pointwise gradient (as an `E`-valued function), via Riesz representation. -/
 noncomputable def grad (f : E → ℝ) : E → E :=
@@ -88,21 +92,21 @@ lemma continuous_grad {f : E → ℝ} (hf : ContDiff ℝ 1 f) : Continuous (grad
   have hcont : Continuous (fderiv ℝ f) := hf.continuous_fderiv one_ne_zero
   have : Continuous fun x => (InnerProductSpace.toDual ℝ E).symm (fderiv ℝ f x) :=
     (InnerProductSpace.toDual ℝ E).symm.continuous.comp hcont
-  simpa [grad] using this
+  exact this
 
 lemma hasCompactSupport_grad {f : E → ℝ} (hf : HasCompactSupport f) :
     HasCompactSupport (grad (E := E) f) := by
   -- Outside the support of `f`, `fderiv` is identically `0`, hence so is `grad`.
   have hf' : HasCompactSupport (fderiv ℝ f) := hf.fderiv ℝ
   -- `grad` is composition with a linear map sending `0` to `0`.
-  simpa [grad] using
+  exact
     (HasCompactSupport.comp_left (f := fderiv ℝ f) (g := (InnerProductSpace.toDual ℝ E).symm)
       hf' (by simp))
 
 lemma tsupport_grad_subset (f : E → ℝ) : tsupport (grad (E := E) f) ⊆ tsupport f := by
   have hcomp :
       tsupport (grad (E := E) f) ⊆ tsupport (fderiv ℝ f) := by
-    simpa [grad, Function.comp] using
+    exact
       (tsupport_comp_subset
         (g := (InnerProductSpace.toDual ℝ E).symm) (hg := by simp)
         (f := fderiv ℝ f))
@@ -165,8 +169,8 @@ private lemma toL2_smul (c : ℝ) (f : ↥(C1c (E := E))) :
 /-- Linear map sending `C¹_c` functions to their `L²` classes. -/
 noncomputable def toL2Linear : ↥(C1c (E := E)) →ₗ[ℝ] L2ℝ (μ := μ) where
   toFun := toL2 (μ := μ) (E := E)
-  map_add' := toL2_add (μ := μ) (E := E)
-  map_smul' := toL2_smul (μ := μ) (E := E)
+  map_add' := by exact toL2_add (μ := μ) (E := E)
+  map_smul' := by exact toL2_smul (μ := μ) (E := E)
 
 private lemma toL2Grad_add (f g : ↥(C1c (E := E))) :
     toL2Grad (μ := μ) (E := E) (f + g) =
@@ -226,8 +230,8 @@ private lemma toL2Grad_smul (c : ℝ) (f : ↥(C1c (E := E))) :
 /-- Linear map sending `C¹_c` functions to the `L²` class of their gradient. -/
 noncomputable def toL2GradLinear : ↥(C1c (E := E)) →ₗ[ℝ] L2E (μ := μ) where
   toFun := toL2Grad (μ := μ) (E := E)
-  map_add' := toL2Grad_add (μ := μ) (E := E)
-  map_smul' := toL2Grad_smul (μ := μ) (E := E)
+  map_add' := by exact toL2Grad_add (μ := μ) (E := E)
+  map_smul' := by exact toL2Grad_smul (μ := μ) (E := E)
 
 /-- The graph map `f ↦ (f, ∇f)` into `L² × L²(E)`. -/
 noncomputable def graph : ↥(C1c (E := E)) →ₗ[ℝ] H1Target (μ := μ) :=
@@ -243,7 +247,7 @@ theorem isClosed_h1 : IsClosed (h1 (μ := μ) (E := E) : Set (H1Target (μ := μ
   exact Submodule.isClosed_topologicalClosure (LinearMap.range (graph (μ := μ) (E := E)))
 
 /-- `H¹` is complete (a Hilbert space once the ambient `L²` spaces are). -/
-instance instCompleteSpace_h1 : CompleteSpace (↥(h1 (μ := μ) (E := E))) := by
+instance instCompleteSpaceh1 : CompleteSpace (↥(h1 (μ := μ) (E := E))) := by
   classical
   exact (isClosed_h1 (μ := μ) (E := E)).isComplete.completeSpace_coe
 
diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Approximation.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Approximation.lean
index 1ae0860..e44c3dc 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Approximation.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Approximation.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2026 Adam Benenson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Benenson
+-/
+
 import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.Translation
 import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Smoothing
 import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
@@ -10,12 +16,6 @@ import Mathlib.MeasureTheory.Measure.Haar.Unique
 import Mathlib.MeasureTheory.Function.L2Space
 import Mathlib.Probability.Moments.Variance
 
-/-
-Copyright (c) 2026 Adam Benenson. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Adam Benenson
--/
-
 /-!
 # `L²` compactness criterion: approximation-by-translation bounds (Euclidean)
 
@@ -44,13 +44,14 @@ section Volume
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
 
-local instance : MeasurableSpace E := borel E
-local instance : BorelSpace E := ⟨rfl⟩
-local instance : OpensMeasurableSpace E := by
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceApproximation : MeasurableSpace E := borel E
+local instance instBorelSpaceApproximation : BorelSpace E := ⟨rfl⟩
+local instance instOpensMeasurableSpaceApproximation : OpensMeasurableSpace E := by
   infer_instance
-local instance : MeasurableAdd E := by
+local instance instMeasurableAddApproximation : MeasurableAdd E := by
   infer_instance
-local instance : MeasurableNeg E := by
+local instance instMeasurableNegApproximation : MeasurableNeg E := by
   infer_instance
 
 variable {K : Set E} (hK : IsCompact K) (hKm : MeasurableSet K)
@@ -81,7 +82,9 @@ lemma kernelMeasure_univ (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ) (
   -- Conclude using `∫ ψ = 1`.
   simpa [hψint] using (hwd.trans hlin)
 
-local instance instIsProbabilityMeasure_kernelMeasure
+/-- The kernel measure `kernelMeasure ψ` is a probability measure when `ψ` is a continuous,
+compactly supported, nonnegative density integrating to `1`. -/
+lemma isProbabilityMeasure_kernelMeasure
     (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ)
     (hψ0 : ∀ x, 0 ≤ ψ x)
     (hψint : ∫ x, ψ x ∂(volume : Measure E) = 1) :
@@ -96,7 +99,7 @@ lemma integral_kernelMeasure_eq_integral_smul (hψc : Continuous ψ) (hψ0 : ∀
     (hψc.measurable.ennreal_ofReal : Measurable fun x => ENNReal.ofReal (ψ x))
   have htop :
       (MeasureTheory.ae (volume : Measure E)).Eventually
-        (fun x => ENNReal.ofReal (ψ x) < ∞) :=
+        (fun x => ENNReal.ofReal (ψ x) < (⊤ : ℝ≥0∞)) :=
     Filter.Eventually.of_forall (fun _ => by simp)
   have hwd :=
     (integral_withDensity_eq_integral_toReal_smul (μ := (volume : Measure E))
@@ -189,7 +192,7 @@ lemma norm_sq_translateL2_sub_extendByZeroL2_eq_integral_sq (t : E)
         MeasureTheory.MeasurePreserving (fun x : E => x - t)
           (volume : Measure E) (volume : Measure E) :=
       MeasureTheory.measurePreserving_sub_right (μ := (volume : Measure E)) t
-    simpa [Function.comp] using (hmp.quasiMeasurePreserving.ae_eq_comp hF_ae)
+    exact (hmp.quasiMeasurePreserving.ae_eq_comp hF_ae)
   -- TranslateL2 gives `F(x - t)` a.e.
   have htrans :
       ((translateL2 (μ := (volume : Measure E)) (-t)) F : E → ℝ) =ᵐ[(volume : Measure E)]
@@ -221,7 +224,7 @@ lemma norm_sq_translateL2_sub_extendByZeroL2_eq_integral_sq (t : E)
             ∂(volume : Measure E) =
           ∫ x, (f (x - t) - f x) ^ 2 ∂(volume : Measure E) := by
       refine MeasureTheory.integral_congr_ae ?_
-      simpa using hdiff.pow_const 2
+      exact hdiff.pow_const 2
     exact h1.trans h2
   simpa [F, f] using hcalc
 
@@ -242,7 +245,7 @@ private lemma kernelMeasure_le_smul_volume (hψc : Continuous ψ) (hψcs : HasCo
       simpa [Real.norm_eq_abs, abs_of_nonneg (hψ0 x)] using hx'
     exact ENNReal.ofReal_le_ofReal hx
   -- Unfold `withDensity` and bound the density by the constant `ENNReal.ofReal C`.
-  simp [kernelMeasure, MeasureTheory.withDensity_apply, hs]
+  simp only [kernelMeasure, MeasureTheory.withDensity_apply, hs]
   have hle :
       (∫⁻ x in s, ENNReal.ofReal (ψ x) ∂(volume : Measure E)) ≤
         ∫⁻ x in s, ENNReal.ofReal C ∂(volume : Measure E) := by
@@ -262,9 +265,9 @@ lemma smoothFun_sub_extendByZeroFun_sq_le_integral_sq
           ∂kernelMeasure (E := E) ψ := by
   classical
   let μ : Measure E := kernelMeasure (E := E) ψ
-  haveI : MeasureTheory.IsProbabilityMeasure μ :=
-    instIsProbabilityMeasure_kernelMeasure (E := E) (ψ := ψ) hψc hψcs hψ0 hψint
-  haveI : MeasureTheory.IsFiniteMeasure μ := by infer_instance
+  have : MeasureTheory.IsProbabilityMeasure μ :=
+    isProbabilityMeasure_kernelMeasure (E := E) (ψ := ψ) hψc hψcs hψ0 hψint
+  have : MeasureTheory.IsFiniteMeasure μ := by infer_instance
   rcases kernelMeasure_le_smul_volume (E := E) (ψ := ψ) hψc hψcs hψ0 with ⟨c, hc_top, hμle⟩
   let f : E → ℝ := extendByZeroFun (E := E) (K := K) u
   have hf_vol : MeasureTheory.MemLp f (2 : ℝ≥0∞) (volume : Measure E) := by
@@ -288,7 +291,11 @@ lemma smoothFun_sub_extendByZeroFun_sq_le_integral_sq
           (volume : Measure E) (volume : Measure E) :=
       MeasureTheory.measurePreserving_add_right
         (μ := (volume : Measure E)) x
-    simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using hadd.comp hneg
+    have hcomp : ((fun y : E => y + x) ∘ fun t : E => -t) = fun t : E => x - t := by
+      funext t
+      simp [sub_eq_add_neg, add_comm]
+    have := hadd.comp hneg
+    rwa [hcomp] at this
   have hf_shift_vol :
       MeasureTheory.MemLp (fun t : E => f (x - t))
         (2 : ℝ≥0∞) (volume : Measure E) :=
@@ -334,10 +341,10 @@ lemma norm_sq_smoothL2_sub_extendByZeroL2_le_integral_norm_sq_translateL2_sub_ex
           ∂kernelMeasure (E := E) ψ := by
   classical
   let μ : Measure E := kernelMeasure (E := E) ψ
-  haveI : MeasureTheory.IsProbabilityMeasure μ :=
-    instIsProbabilityMeasure_kernelMeasure (E := E) (ψ := ψ) hψc hψcs hψ0 hψint
-  haveI : MeasureTheory.IsFiniteMeasure μ := by infer_instance
-  haveI : MeasureTheory.SFinite μ := by infer_instance
+  have : MeasureTheory.IsProbabilityMeasure μ :=
+    isProbabilityMeasure_kernelMeasure (E := E) (ψ := ψ) hψc hψcs hψ0 hψint
+  have : MeasureTheory.IsFiniteMeasure μ := by infer_instance
+  have : MeasureTheory.SFinite μ := by infer_instance
   let F : (E →₂[(volume : Measure E)] ℝ) := extendByZeroL2 (E := E) (K := K) hKm u
   let f : E → ℝ := extendByZeroFun (E := E) (K := K) u
   let S : (E →₂[(volume : Measure E)] ℝ) := smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs u
@@ -361,7 +368,7 @@ lemma norm_sq_smoothL2_sub_extendByZeroL2_le_integral_norm_sq_translateL2_sub_ex
         (∫ x, ((S - F) x) ^ 2 ∂(volume : Measure E)) =
           ∫ x, (smoothFun (E := E) (K := K) ψ u x - f x) ^ 2 ∂(volume : Measure E) := by
       refine MeasureTheory.integral_congr_ae ?_
-      simpa using hSF_ae.pow_const 2
+      exact hSF_ae.pow_const 2
     exact h1.trans h2
   have hLHS_int :
       MeasureTheory.Integrable (fun x : E => (smoothFun (E := E) (K := K) ψ u x - f x) ^ 2)
@@ -414,7 +421,7 @@ lemma norm_sq_smoothL2_sub_extendByZeroL2_le_integral_norm_sq_translateL2_sub_ex
       MeasureTheory.Integrable (fun z : E × E => (f (z.1 - z.2)) ^ 2)
         ((volume : Measure E).prod μ) := by
     have := (hsub.integrable_comp hf_fst_sq_prod.aestronglyMeasurable).2 hf_fst_sq_prod
-    simpa [Function.comp] using this
+    exact this
   have hdom :
       MeasureTheory.Integrable (fun z : E × E => (2 : ℝ) * ((f (z.1 - z.2)) ^ 2 + (f z.1) ^ 2))
         ((volume : Measure E).prod μ) := by
@@ -426,7 +433,7 @@ lemma norm_sq_smoothL2_sub_extendByZeroL2_le_integral_norm_sq_translateL2_sub_ex
         MeasureTheory.AEStronglyMeasurable f
           (Measure.map Prod.fst
             ((volume : Measure E).prod μ)) := by
-      simpa [Measure.map_fst_prod] using hf_mem.1
+      simpa [Measure.map_fst_prod] using hf_mem.aestronglyMeasurable
     exact MeasureTheory.AEStronglyMeasurable.comp_measurable
       (μ := (volume : Measure E).prod μ) (f := Prod.fst)
       (g := f) hf_map measurable_fst
@@ -436,7 +443,7 @@ lemma norm_sq_smoothL2_sub_extendByZeroL2_le_integral_norm_sq_translateL2_sub_ex
         ((volume : Measure E).prod μ) := by
     have := MeasureTheory.AEStronglyMeasurable.comp_measurePreserving (g := fun z : E × E => f z.1)
       hf_fst_aesm hsub
-    simpa [Function.comp] using this
+    exact this
   have h_aesm :
       MeasureTheory.AEStronglyMeasurable h ((volume : Measure E).prod μ) := by
     -- Build up AE-strong measurability from the two components.
@@ -444,7 +451,7 @@ lemma norm_sq_smoothL2_sub_extendByZeroL2_le_integral_norm_sq_translateL2_sub_ex
         MeasureTheory.AEStronglyMeasurable (fun z : E × E => f (z.1 - z.2) - f z.1)
           ((volume : Measure E).prod μ) :=
       hf_shift_aesm.sub hf_fst_aesm
-    simpa [h] using (hsub'.pow 2)
+    exact (hsub'.pow 2)
   have hint_h : MeasureTheory.Integrable h ((volume : Measure E).prod μ) := by
     refine MeasureTheory.Integrable.mono (μ := (volume : Measure E).prod μ) hdom h_aesm ?_
     refine Filter.Eventually.of_forall ?_
@@ -507,7 +514,6 @@ lemma norm_sq_smoothL2_sub_extendByZeroL2_le_integral_norm_sq_translateL2_sub_ex
   -- Restore the original statement.
   simpa [S, F, μ] using hmain
 
-
 end Volume
 
 end
diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/ArzelaAscoli.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/ArzelaAscoli.lean
index 37fe123..ff15e73 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/ArzelaAscoli.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/ArzelaAscoli.lean
@@ -1,15 +1,15 @@
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Compactness
-import Mathlib.Analysis.Normed.Group.Bounded
-import Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
-import Mathlib.MeasureTheory.Function.L2Space
-import Mathlib.MeasureTheory.Integral.Bochner.Set
-
 /-
 Copyright (c) 2026 Adam Benenson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Benenson
 -/
 
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Compactness
+import Mathlib.Analysis.Normed.Group.Bounded
+import Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
+import Mathlib.MeasureTheory.Function.L2Space
+import Mathlib.MeasureTheory.Integral.Bochner.Set
+
 /-!
 # `L²` compactness criterion: Arzelà–Ascoli for the smoothing operator (Euclidean)
 
@@ -42,13 +42,14 @@ section Volume
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
 
-local instance instMeasurableSpaceE_L2CompactnessArzelaAscoli : MeasurableSpace E := borel E
-local instance instBorelSpaceE_L2CompactnessArzelaAscoli : BorelSpace E := ⟨rfl⟩
-local instance instOpensMeasurableSpaceE_L2CompactnessArzelaAscoli : OpensMeasurableSpace E := by
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceEL2CompactnessArzelaAscoli : MeasurableSpace E := borel E
+local instance instBorelSpaceEL2CompactnessArzelaAscoli : BorelSpace E := ⟨rfl⟩
+local instance instOpensMeasurableSpaceEL2CompactnessArzelaAscoli : OpensMeasurableSpace E := by
   infer_instance
-local instance instMeasurableAddE_L2CompactnessArzelaAscoli : MeasurableAdd E := by
+local instance instMeasurableAddEL2CompactnessArzelaAscoli : MeasurableAdd E := by
   infer_instance
-local instance instMeasurableNegE_L2CompactnessArzelaAscoli : MeasurableNeg E := by
+local instance instMeasurableNegEL2CompactnessArzelaAscoli : MeasurableNeg E := by
   infer_instance
 
 variable {K : Set E} {ψ : E → ℝ}
@@ -110,8 +111,309 @@ private lemma exists_norm_ψ_bound_on_diffSet (hK : IsCompact K) (hψc : Continu
       exact ⟨hx, ht⟩
     exact hne ⟨(x : E) - t, this⟩
 
+private lemma smoothFun_image_mem_closedBall (hK : IsCompact K)
+    (hKm : MeasurableSet K) (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ) {R : ℝ}
+    (hRpos : 0 < R) (Cψ : ℝ) (hCψ_nonneg : 0 ≤ Cψ)
+    (hψ_bound : ∀ x : ↥(Kψ (K := K) (ψ := ψ)), ∀ t : E, t ∈ K → ‖ψ ((x : E) - t)‖ ≤ Cψ) :
+    let mK : ℝ :=
+      (MeasureTheory.measureUnivNNReal (volume.restrict K)) ^ ((2 : ℝ≥0∞).toReal⁻¹)
+    ∀ (f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) (x : ↥(Kψ (K := K) (ψ := ψ))),
+      f ∈ (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs ''
+            Metric.closedBall (0 : _) R) →
+        f x ∈ Metric.closedBall (0 : ℝ) (R * (mK * Cψ)) := by
+  intro mK
+  classical
+  have hR : 0 ≤ R := hRpos.le
+  have hμK : (volume : Measure E) K < (⊤ : ℝ≥0∞) := hK.measure_lt_top (μ := (volume : Measure E))
+  have : Fact ((volume : Measure E) K < (⊤ : ℝ≥0∞)) := ⟨hμK⟩
+  have : IsFiniteMeasure ((volume : Measure E).restrict K) := by infer_instance
+  let μ : Measure E := (volume : Measure E).restrict K
+  have hmK : 0 ≤ mK := by
+    have : 0 ≤ (MeasureTheory.measureUnivNNReal (volume.restrict K)) := by simp
+    exact Real.rpow_nonneg this _
+  intro f x hfA
+  rcases hfA with ⟨u, hu_ball, rfl⟩
+  have hu_norm : ‖u‖ ≤ R := by
+    simpa [Metric.mem_closedBall, dist_eq_norm] using hu_ball
+  -- Build the `L²(K)` kernel element.
+  have hker :
+      MemLp (fun t : E => ψ ((x : E) - t)) (2 : ℝ≥0∞) (volume.restrict K) := by
+    refine MemLp.of_bound (μ := (volume.restrict K))
+      (hf := (hψc.aestronglyMeasurable.comp_measurable
+        (measurable_const.sub measurable_id))) Cψ ?_
+    filter_upwards
+      [MeasureTheory.ae_restrict_mem
+        (μ := (volume : Measure E)) hKm] with t ht
+    exact hψ_bound x t ht
+  let kx : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ :=
+    hker.toLp (fun t : E => ψ ((x : E) - t))
+  have hkx_norm : ‖kx‖ ≤ mK * Cψ := by
+    have h_ae :
+        ∀ᵐ t ∂(volume.restrict K), ‖(fun t : E => ψ ((x : E) - t)) t‖ ≤ Cψ := by
+      filter_upwards [MeasureTheory.ae_restrict_mem (μ := (volume : Measure E)) hKm] with t ht
+      exact hψ_bound x t ht
+    have := (MeasureTheory.Lp.norm_le_of_ae_bound
+      (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞))
+      (f := kx) (hC := hCψ_nonneg) (by
+        -- transport the bound through the `toLp` representative
+        filter_upwards [h_ae,
+          MeasureTheory.MemLp.coeFn_toLp
+            (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞))
+            (f := fun t : E => ψ ((x : E) - t))
+            hker] with t ht hrep
+        simpa [kx, hrep] using ht))
+    simpa [mK] using this
+  -- Express the smoothing value as an `L²` inner product, then apply Cauchy–Schwarz.
+  have hsmooth :
+      smoothFun (E := E) (K := K) ψ u (x : E) =
+        ∫ t, u t * kx t ∂(volume.restrict K) := by
+    have h_ae :
+        (fun t : E => u t * kx t) =ᵐ[volume.restrict K] fun t : E => u t * ψ ((x : E) - t) := by
+      filter_upwards [MeasureTheory.MemLp.coeFn_toLp
+        (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞))
+        (f := fun t : E => ψ ((x : E) - t))
+        hker] with t ht
+      simp [kx, ht]
+    -- rewrite `smoothFun` as an integral on `volume.restrict K`
+    rw [smoothFun_eq_integral_restrict
+      (E := E) (K := K) (ψ := ψ) (hKm := hKm) u (x : E)]
+    exact (MeasureTheory.integral_congr_ae h_ae.symm)
+  have hsmooth' :
+      smoothFun (E := E) (K := K) ψ u (x : E) =
+        ∫ t, kx t * u t ∂(volume.restrict K) := by
+    simp [hsmooth, mul_comm]
+  have hinner :
+      smoothFun (E := E) (K := K) ψ u (x : E) =
+        inner ℝ (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ) kx := by
+    erw [MeasureTheory.L2.inner_def]; exact hsmooth'
+  have habs :
+      |smoothFun (E := E) (K := K) ψ u (x : E)| ≤ ‖u‖ * ‖kx‖ := by
+    simpa [hinner] using
+      (abs_real_inner_le_norm (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ) kx)
+  have habs' : |smoothFun (E := E) (K := K) ψ u (x : E)| ≤ R * (mK * Cψ) := by
+    calc
+      |smoothFun (E := E) (K := K) ψ u (x : E)|
+          ≤ ‖u‖ * ‖kx‖ := habs
+      _ ≤ R * (mK * Cψ) := by
+        exact mul_le_mul hu_norm hkx_norm (norm_nonneg _) hR
+  have : dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x) 0 ≤ R * (mK * Cψ) := by
+    simpa [smoothBCF_apply (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x,
+      dist_eq_norm, Real.norm_eq_abs] using habs'
+  simpa [Metric.mem_closedBall, dist_eq_norm] using this
+
 /-- Arzelà--Ascoli: smoothing maps `L²(K)` bounded sets into a precompact set
 in `BCF(K + tsupport ψ)`. -/
+private lemma uniformEquicontinuous_smoothBCF_closedBall (hK : IsCompact K)
+    (hKm : MeasurableSet K) (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ) {R : ℝ}
+    (hRpos : 0 < R) (Cψ : ℝ) (hCψ_nonneg : 0 ≤ Cψ)
+    (hψ_bound : ∀ x : ↥(Kψ (K := K) (ψ := ψ)), ∀ t : E, t ∈ K → ‖ψ ((x : E) - t)‖ ≤ Cψ) :
+    let A : Set (BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) :=
+      smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs '' Metric.closedBall (0 : _) R
+    UniformEquicontinuous ((↑) : A → ↥(Kψ (K := K) (ψ := ψ)) → ℝ) := by
+  intro A
+  classical
+  have hR : 0 ≤ R := hRpos.le
+  have hR0 : R ≠ 0 := ne_of_gt hRpos
+  have hμK : (volume : Measure E) K < (⊤ : ℝ≥0∞) := hK.measure_lt_top (μ := (volume : Measure E))
+  have : Fact ((volume : Measure E) K < (⊤ : ℝ≥0∞)) := ⟨hμK⟩
+  have : IsFiniteMeasure ((volume : Measure E).restrict K) := by infer_instance
+  let μ : Measure E := (volume : Measure E).restrict K
+  let mK : ℝ :=
+    (MeasureTheory.measureUnivNNReal (volume.restrict K)) ^ ((2 : ℝ≥0∞).toReal⁻¹)
+  have hmK : 0 ≤ mK := Real.rpow_nonneg (by simp) _
+  let s : Set ℝ := Metric.closedBall (0 : ℝ) (R * (mK * Cψ))
+  have in_s :=
+    smoothFun_image_mem_closedBall (K := K) (ψ := ψ) hK hKm hψc hψcs
+      (R := R) hRpos Cψ hCψ_nonneg hψ_bound
+  rw [Metric.uniformEquicontinuous_iff]
+  intro ε hε
+  -- Handle the zero-measure case separately (then `mK = 0` and everything is constant).
+  by_cases hmK0 : mK = 0
+  · refine ⟨1, by norm_num, ?_⟩
+    intro x y _ f
+    -- With `mK = 0`, the range bound forces all values to be `0`.
+    set F : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ :=
+      (f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) with hF
+    have hzero : ∀ z, F z = 0 := by
+      intro z
+      have hmem : F z ∈ s := in_s (f := F) z f.property
+      have hle : dist (F z) 0 ≤ 0 := by
+        have : dist (F z) 0 ≤ R * (mK * Cψ) := by simpa [s, Metric.mem_closedBall] using hmem
+        simpa [hmK0] using this
+      exact dist_eq_zero.1 (le_antisymm hle dist_nonneg)
+    simpa [hzero x, hzero y] using hε
+  · have hRmK_ne : R * mK ≠ 0 := mul_ne_zero hR0 hmK0
+    let ε2 : ℝ := ε / 2
+    have hε2pos : 0 < ε2 := by
+      simpa [ε2] using half_pos hε
+    let ε' : ℝ := ε2 / (R * mK)
+    have hε'pos : 0 < ε' :=
+      div_pos hε2pos (mul_pos hRpos (lt_of_le_of_ne hmK (Ne.symm hmK0)))
+    have hε'lt : R * mK * ε' = ε2 := by
+      dsimp [ε']
+      field_simp [hRmK_ne, mul_assoc, mul_left_comm, mul_comm]
+    -- Use uniform continuity of `ψ` to get `deltaLoss`.
+    have hUC : UniformContinuous ψ := uniformContinuous_ψ (E := E) (ψ := ψ) hψc hψcs
+    rcases (Metric.uniformContinuous_iff.1 hUC) ε' hε'pos with ⟨deltaLoss, hδpos, hδ⟩
+    refine ⟨deltaLoss, hδpos, ?_⟩
+    intro x y hxy f
+    -- Work with the `smoothBCF` representative of `f`.
+    rcases f.property with ⟨u, hu_ball, hu_eq⟩
+    have hu_eq' :
+        (f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) =
+          smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u := by
+      simpa using hu_eq.symm
+    have hu_norm : ‖u‖ ≤ R := by
+      simpa [Metric.mem_closedBall, dist_eq_norm] using hu_ball
+    -- Kernel elements at `x` and `y`.
+    have hkerx :
+        MemLp (fun t : E => ψ ((x : E) - t)) (2 : ℝ≥0∞) (volume.restrict K) := by
+      refine MemLp.of_bound (μ := (volume.restrict K))
+        (hf := (hψc.aestronglyMeasurable.comp_measurable
+          (measurable_const.sub measurable_id))) Cψ ?_
+      filter_upwards
+        [MeasureTheory.ae_restrict_mem
+          (μ := (volume : Measure E)) hKm] with t ht
+      exact hψ_bound x t ht
+    have hkery :
+        MemLp (fun t : E => ψ ((y : E) - t)) (2 : ℝ≥0∞) (volume.restrict K) := by
+      refine MemLp.of_bound (μ := (volume.restrict K))
+        (hf := (hψc.aestronglyMeasurable.comp_measurable
+          (measurable_const.sub measurable_id))) Cψ ?_
+      filter_upwards [MeasureTheory.ae_restrict_mem (μ := (volume : Measure E)) hKm] with t ht
+      exact hψ_bound y t ht
+    let kx : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ :=
+      hkerx.toLp (fun t : E => ψ ((x : E) - t))
+    let ky : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ :=
+      hkery.toLp (fun t : E => ψ ((y : E) - t))
+    -- AE bound on `‖kx - ky‖` by `ε'`.
+    have h_ae :
+        ∀ᵐ t ∂(volume.restrict K), ‖(kx - ky) t‖ ≤ ε' := by
+      filter_upwards [MeasureTheory.ae_restrict_mem (μ := (volume : Measure E)) hKm,
+        MeasureTheory.MemLp.coeFn_toLp (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞))
+          (f := fun t : E => ψ ((x : E) - t)) hkerx,
+        MeasureTheory.MemLp.coeFn_toLp (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞))
+          (f := fun t : E => ψ ((y : E) - t)) hkery,
+        (MeasureTheory.Lp.coeFn_sub (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞)) kx ky)] with
+        t ht hx_t hy_t hsub
+      have hxy' : dist ((x : E) - t) ((y : E) - t) < deltaLoss := by
+        rw [dist_sub_right]
+        exact hxy
+      have hψxy : dist (ψ ((x : E) - t)) (ψ ((y : E) - t)) < ε' :=
+        hδ (a := (x : E) - t) (b := (y : E) - t) hxy'
+      have : ‖ψ ((x : E) - t) - ψ ((y : E) - t)‖ ≤ ε' := by
+        simpa [dist_eq_norm, sub_eq_add_neg] using le_of_lt hψxy
+      have hx' : kx t = ψ ((x : E) - t) := by simpa [kx] using hx_t
+      have hy' : ky t = ψ ((y : E) - t) := by simpa [ky] using hy_t
+      have hnorm : ‖kx t - ky t‖ ≤ ε' := by
+        simpa [hx', hy'] using this
+      have hsub' : (kx - ky) t = kx t - ky t := by
+        simpa [Pi.sub_apply] using hsub
+      simpa [hsub'.symm] using hnorm
+    have hkdiff : ‖kx - ky‖ ≤ mK * ε' := by
+      have := (MeasureTheory.Lp.norm_le_of_ae_bound (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞))
+        (f := (kx - ky : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ)) (hC := le_of_lt hε'pos) h_ae)
+      simpa [mK, mul_comm, mul_left_comm, mul_assoc] using this
+    -- Bound the difference of values using Cauchy–Schwarz.
+    have hdist :
+        dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x)
+            (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y)
+          ≤ ‖u‖ * ‖kx - ky‖ := by
+      -- Express each value as an inner product.
+      have hx_val :
+          smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x =
+            inner ℝ (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ) kx := by
+        have hsmooth :
+            smoothFun (E := E) (K := K) ψ u (x : E) =
+              ∫ t, u t * kx t ∂(volume.restrict K) := by
+          have h_ae' :
+              (fun t : E => u t * kx t) =ᵐ[volume.restrict K]
+                fun t : E => u t * ψ ((x : E) - t) := by
+            filter_upwards [MeasureTheory.MemLp.coeFn_toLp
+              (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞))
+              (f := fun t : E => ψ ((x : E) - t))
+              hkerx] with t ht
+            simp [kx, ht]
+          rw [smoothFun_eq_integral_restrict
+            (E := E) (K := K) (ψ := ψ) (hKm := hKm)
+            u (x : E)]
+          exact (MeasureTheory.integral_congr_ae h_ae'.symm)
+        have hsmooth' :
+            smoothFun (E := E) (K := K) ψ u (x : E) =
+              ∫ t, kx t * u t ∂(volume.restrict K) := by
+          simp [hsmooth, mul_comm]
+        erw [smoothBCF_apply (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x,
+          MeasureTheory.L2.inner_def]; exact hsmooth'
+      have hy_val :
+          smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y =
+            inner ℝ (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ) ky := by
+        have hsmooth :
+            smoothFun (E := E) (K := K) ψ u (y : E) =
+              ∫ t, u t * ky t ∂(volume.restrict K) := by
+          have h_ae' :
+              (fun t : E => u t * ky t) =ᵐ[volume.restrict K]
+                fun t : E => u t * ψ ((y : E) - t) := by
+            filter_upwards [MeasureTheory.MemLp.coeFn_toLp
+              (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞))
+              (f := fun t : E => ψ ((y : E) - t))
+              hkery] with t ht
+            simp [ky, ht]
+          rw [smoothFun_eq_integral_restrict
+            (E := E) (K := K) (ψ := ψ) (hKm := hKm)
+            u (y : E)]
+          exact (MeasureTheory.integral_congr_ae h_ae'.symm)
+        have hsmooth' :
+            smoothFun (E := E) (K := K) ψ u (y : E) =
+              ∫ t, ky t * u t ∂(volume.restrict K) := by
+          simp [hsmooth, mul_comm]
+        erw [smoothBCF_apply (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y,
+          MeasureTheory.L2.inner_def]; exact hsmooth'
+      have :
+          ‖smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x -
+              smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y‖ ≤
+            ‖u‖ * ‖kx - ky‖ := by
+        have :
+            smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x -
+                smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y =
+              inner ℝ (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ) (kx - ky) := by
+          simp [hx_val, hy_val, inner_sub_right]
+        have this' :
+            smoothFun (E := E) (K := K) ψ u (x : E) - smoothFun (E := E) (K := K) ψ u (y : E) =
+              inner ℝ (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ) (kx - ky) := by
+          simpa [smoothBCF_apply (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs] using this
+        have hCS :=
+          (abs_real_inner_le_norm (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ) (kx - ky))
+        simpa [this', dist_eq_norm, Real.norm_eq_abs] using hCS
+      simpa [dist_eq_norm] using this
+    have hle :
+        dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x)
+            (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y)
+          ≤ R * (mK * ε') := by
+      calc
+        dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x)
+            (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y)
+            ≤ ‖u‖ * ‖kx - ky‖ := hdist
+        _ ≤ ‖u‖ * (mK * ε') := by
+          exact mul_le_mul_of_nonneg_left hkdiff (norm_nonneg _)
+        _ ≤ R * (mK * ε') := by
+          have hmKε' : 0 ≤ mK * ε' := mul_nonneg hmK (le_of_lt hε'pos)
+          exact mul_le_mul_of_nonneg_right hu_norm hmKε'
+    have hRmkε' : R * (mK * ε') = ε2 := by
+      have : R * mK * ε' = ε2 := by
+        simpa [ε', mul_assoc] using hε'lt
+      simpa [mul_assoc] using this
+    have hle' :
+        dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x)
+            (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y) ≤ ε2 := by
+      simpa [hRmkε'] using hle
+    have hε2lt : ε2 < ε := by
+      simpa [ε2] using half_lt_self hε
+    have :
+        dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x)
+            (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y) < ε :=
+      lt_of_le_of_lt hle' hε2lt
+    simpa [hu_eq'] using this
+
 theorem smoothBCF_image_closedBall_isCompact (hK : IsCompact K) (hKm : MeasurableSet K)
     (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ) {R : ℝ} (hR : 0 ≤ R) :
     IsCompact
@@ -130,15 +432,15 @@ theorem smoothBCF_image_closedBall_isCompact (hK : IsCompact K) (hKm : Measurabl
     simp [hball]
   · have hRpos : 0 < R := lt_of_le_of_ne hR (Ne.symm hR0)
     -- Compactness of the codomain.
-    letI : CompactSpace ↥(Kψ (K := K) (ψ := ψ)) :=
+    let : CompactSpace ↥(Kψ (K := K) (ψ := ψ)) :=
       isCompact_iff_compactSpace.1 (isCompact_Kψ (K := K) (ψ := ψ) hK hψcs)
     let A :
         Set (BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) :=
       smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs '' Metric.closedBall (0 : _) R
     -- `volume.restrict K` is finite since `K` is compact.
-    have hμK : (volume : Measure E) K < ∞ := hK.measure_lt_top (μ := (volume : Measure E))
-    letI : Fact ((volume : Measure E) K < ∞) := ⟨hμK⟩
-    haveI : IsFiniteMeasure (volume.restrict K) := by
+    have hμK : (volume : Measure E) K < (⊤ : ℝ≥0∞) := hK.measure_lt_top (μ := (volume : Measure E))
+    let : Fact ((volume : Measure E) K < (⊤ : ℝ≥0∞)) := ⟨hμK⟩
+    have : IsFiniteMeasure (volume.restrict K) := by
       infer_instance
     let μ : Measure E := (volume : Measure E).restrict K
     let mK : ℝ :=
@@ -227,211 +529,10 @@ theorem smoothBCF_image_closedBall_isCompact (hK : IsCompact K) (hKm : Measurabl
           dist_eq_norm, Real.norm_eq_abs] using habs'
       simpa [s, Metric.mem_closedBall, dist_eq_norm] using this
     -- Equicontinuity for `A`.
-    have H' : UniformEquicontinuous ((↑) : A → ↥(Kψ (K := K) (ψ := ψ)) → ℝ) := by
-      rw [Metric.uniformEquicontinuous_iff]
-      intro ε hε
-      -- Handle the zero-measure case separately (then `mK = 0` and everything is constant).
-      by_cases hmK0 : mK = 0
-      · refine ⟨1, by norm_num, ?_⟩
-        intro x y _ f
-        -- With `mK = 0`, the range bound forces all values to be `0`.
-        have hx0 : dist ((f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) x) 0 ≤
-            R * (mK * Cψ) := by
-          have :
-              (f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) x ∈ s :=
-            in_s (f := (f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ)) x f.property
-          simpa [s, Metric.mem_closedBall] using this
-        have hy0 : dist ((f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) y) 0 ≤
-            R * (mK * Cψ) := by
-          have :
-              (f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) y ∈ s :=
-            in_s (f := (f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ)) y f.property
-          simpa [s, Metric.mem_closedBall] using this
-        have hx0' :
-            dist ((f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) x) 0 = 0 := by
-          have : dist ((f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) x) 0 ≤ 0 := by
-            simpa [hmK0] using hx0
-          exact le_antisymm this dist_nonneg
-        have hy0' :
-            dist ((f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) y) 0 = 0 := by
-          have : dist ((f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) y) 0 ≤ 0 := by
-            simpa [hmK0] using hy0
-          exact le_antisymm this dist_nonneg
-        have hx : (f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) x = 0 :=
-          dist_eq_zero.1 hx0'
-        have hy : (f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) y = 0 :=
-          dist_eq_zero.1 hy0'
-        simpa [hx, hy] using hε
-      · have hRmK_ne : R * mK ≠ 0 := mul_ne_zero hR0 hmK0
-        let ε2 : ℝ := ε / 2
-        have hε2pos : 0 < ε2 := by
-          simpa [ε2] using half_pos hε
-        let ε' : ℝ := ε2 / (R * mK)
-        have hε'pos : 0 < ε' :=
-          div_pos hε2pos (mul_pos hRpos (lt_of_le_of_ne hmK (Ne.symm hmK0)))
-        have hε'lt : R * mK * ε' = ε2 := by
-          dsimp [ε']
-          field_simp [hRmK_ne, mul_assoc, mul_left_comm, mul_comm]
-        -- Use uniform continuity of `ψ` to get `δ`.
-        have hUC : UniformContinuous ψ := uniformContinuous_ψ (E := E) (ψ := ψ) hψc hψcs
-        rcases (Metric.uniformContinuous_iff.1 hUC) ε' hε'pos with ⟨δ, hδpos, hδ⟩
-        refine ⟨δ, hδpos, ?_⟩
-        intro x y hxy f
-        -- Work with the `smoothBCF` representative of `f`.
-        rcases f.property with ⟨u, hu_ball, hu_eq⟩
-        have hu_eq' :
-            (f : BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) =
-              smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u := by
-          simpa using hu_eq.symm
-        have hu_norm : ‖u‖ ≤ R := by
-          simpa [Metric.mem_closedBall, dist_eq_norm] using hu_ball
-        -- Kernel elements at `x` and `y`.
-        have hkerx :
-            MemLp (fun t : E => ψ ((x : E) - t)) (2 : ℝ≥0∞) (volume.restrict K) := by
-          refine MemLp.of_bound (μ := (volume.restrict K))
-            (hf := (hψc.aestronglyMeasurable.comp_measurable
-              (measurable_const.sub measurable_id))) Cψ ?_
-          filter_upwards
-            [MeasureTheory.ae_restrict_mem
-              (μ := (volume : Measure E)) hKm] with t ht
-          exact hψ_bound x t ht
-        have hkery :
-            MemLp (fun t : E => ψ ((y : E) - t)) (2 : ℝ≥0∞) (volume.restrict K) := by
-          refine MemLp.of_bound (μ := (volume.restrict K))
-            (hf := (hψc.aestronglyMeasurable.comp_measurable
-              (measurable_const.sub measurable_id))) Cψ ?_
-          filter_upwards [MeasureTheory.ae_restrict_mem (μ := (volume : Measure E)) hKm] with t ht
-          exact hψ_bound y t ht
-        let kx : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ :=
-          hkerx.toLp (fun t : E => ψ ((x : E) - t))
-        let ky : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ :=
-          hkery.toLp (fun t : E => ψ ((y : E) - t))
-        -- AE bound on `‖kx - ky‖` by `ε'`.
-        have h_ae :
-            ∀ᵐ t ∂(volume.restrict K), ‖(kx - ky) t‖ ≤ ε' := by
-          filter_upwards [MeasureTheory.ae_restrict_mem (μ := (volume : Measure E)) hKm,
-            MeasureTheory.MemLp.coeFn_toLp (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞))
-              (f := fun t : E => ψ ((x : E) - t)) hkerx,
-            MeasureTheory.MemLp.coeFn_toLp (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞))
-              (f := fun t : E => ψ ((y : E) - t)) hkery,
-            (MeasureTheory.Lp.coeFn_sub (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞)) kx ky)] with
-            t ht hx_t hy_t hsub
-          have hxy' : dist ((x : E) - t) ((y : E) - t) < δ := by
-            simpa [sub_eq_add_neg, add_assoc] using hxy
-          have hψxy : dist (ψ ((x : E) - t)) (ψ ((y : E) - t)) < ε' :=
-            hδ (a := (x : E) - t) (b := (y : E) - t) hxy'
-          have : ‖ψ ((x : E) - t) - ψ ((y : E) - t)‖ ≤ ε' := by
-            simpa [dist_eq_norm, sub_eq_add_neg] using le_of_lt hψxy
-          have hx' : kx t = ψ ((x : E) - t) := by simpa [kx] using hx_t
-          have hy' : ky t = ψ ((y : E) - t) := by simpa [ky] using hy_t
-          have hnorm : ‖kx t - ky t‖ ≤ ε' := by
-            simpa [hx', hy'] using this
-          have hsub' : (kx - ky) t = kx t - ky t := by
-            simpa [Pi.sub_apply] using hsub
-          simpa [hsub'.symm] using hnorm
-        have hkdiff : ‖kx - ky‖ ≤ mK * ε' := by
-          have := (MeasureTheory.Lp.norm_le_of_ae_bound (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞))
-            (f := (kx - ky : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ)) (hC := le_of_lt hε'pos) h_ae)
-          simpa [mK, mul_comm, mul_left_comm, mul_assoc] using this
-        -- Bound the difference of values using Cauchy–Schwarz.
-        have hdist :
-            dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x)
-                (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y)
-              ≤ ‖u‖ * ‖kx - ky‖ := by
-          -- Express each value as an inner product.
-          have hx_val :
-              smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x =
-                inner ℝ (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ) kx := by
-            have hsmooth :
-                smoothFun (E := E) (K := K) ψ u (x : E) =
-                  ∫ t, u t * kx t ∂(volume.restrict K) := by
-              have h_ae' :
-                  (fun t : E => u t * kx t) =ᵐ[volume.restrict K]
-                    fun t : E => u t * ψ ((x : E) - t) := by
-                filter_upwards [MeasureTheory.MemLp.coeFn_toLp
-                  (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞))
-                  (f := fun t : E => ψ ((x : E) - t))
-                  hkerx] with t ht
-                simp [kx, ht]
-              rw [smoothFun_eq_integral_restrict
-                (E := E) (K := K) (ψ := ψ) (hKm := hKm)
-                u (x : E)]
-              exact (MeasureTheory.integral_congr_ae h_ae'.symm)
-            have hsmooth' :
-                smoothFun (E := E) (K := K) ψ u (x : E) =
-                  ∫ t, kx t * u t ∂(volume.restrict K) := by
-              simp [hsmooth, mul_comm]
-            erw [smoothBCF_apply (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x,
-              MeasureTheory.L2.inner_def]; exact hsmooth'
-          have hy_val :
-              smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y =
-                inner ℝ (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ) ky := by
-            have hsmooth :
-                smoothFun (E := E) (K := K) ψ u (y : E) =
-                  ∫ t, u t * ky t ∂(volume.restrict K) := by
-              have h_ae' :
-                  (fun t : E => u t * ky t) =ᵐ[volume.restrict K]
-                    fun t : E => u t * ψ ((y : E) - t) := by
-                filter_upwards [MeasureTheory.MemLp.coeFn_toLp
-                  (μ := (volume.restrict K)) (p := (2 : ℝ≥0∞))
-                  (f := fun t : E => ψ ((y : E) - t))
-                  hkery] with t ht
-                simp [ky, ht]
-              rw [smoothFun_eq_integral_restrict
-                (E := E) (K := K) (ψ := ψ) (hKm := hKm)
-                u (y : E)]
-              exact (MeasureTheory.integral_congr_ae h_ae'.symm)
-            have hsmooth' :
-                smoothFun (E := E) (K := K) ψ u (y : E) =
-                  ∫ t, ky t * u t ∂(volume.restrict K) := by
-              simp [hsmooth, mul_comm]
-            erw [smoothBCF_apply (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y,
-              MeasureTheory.L2.inner_def]; exact hsmooth'
-          have :
-              ‖smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x -
-                  smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y‖ ≤
-                ‖u‖ * ‖kx - ky‖ := by
-            have :
-                smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x -
-                    smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y =
-                  inner ℝ (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ) (kx - ky) := by
-              simp [hx_val, hy_val, inner_sub_right]
-            have this' :
-                smoothFun (E := E) (K := K) ψ u (x : E) - smoothFun (E := E) (K := K) ψ u (y : E) =
-                  inner ℝ (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ) (kx - ky) := by
-              simpa [smoothBCF_apply (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs] using this
-            have hCS :=
-              (abs_real_inner_le_norm (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μ) (kx - ky))
-            simpa [this', dist_eq_norm, Real.norm_eq_abs] using hCS
-          simpa [dist_eq_norm] using this
-        have hle :
-            dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x)
-                (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y)
-              ≤ R * (mK * ε') := by
-          calc
-            dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x)
-                (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y)
-                ≤ ‖u‖ * ‖kx - ky‖ := hdist
-            _ ≤ ‖u‖ * (mK * ε') := by
-              exact mul_le_mul_of_nonneg_left hkdiff (norm_nonneg _)
-            _ ≤ R * (mK * ε') := by
-              have hmKε' : 0 ≤ mK * ε' := mul_nonneg hmK (le_of_lt hε'pos)
-              exact mul_le_mul_of_nonneg_right hu_norm hmKε'
-        have hRmkε' : R * (mK * ε') = ε2 := by
-          have : R * mK * ε' = ε2 := by
-            simpa [ε', mul_assoc] using hε'lt
-          simpa [mul_assoc] using this
-        have hle' :
-            dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x)
-                (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y) ≤ ε2 := by
-          simpa [hRmkε'] using hle
-        have hε2lt : ε2 < ε := by
-          simpa [ε2] using half_lt_self hε
-        have :
-            dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u x)
-                (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u y) < ε :=
-          lt_of_le_of_lt hle' hε2lt
-        simpa [hu_eq'] using this
+    have H' :
+        UniformEquicontinuous ((↑) : A → ↥(Kψ (K := K) (ψ := ψ)) → ℝ) :=
+      uniformEquicontinuous_smoothBCF_closedBall (K := K) (ψ := ψ) hK hKm hψc hψcs
+        (R := R) hRpos Cψ hCψ_nonneg hψ_bound
     have H : Equicontinuous ((↑) : A → ↥(Kψ (K := K) (ψ := ψ)) → ℝ) := H'.equicontinuous
     -- Apply Arzelà–Ascoli.
     simpa [A, s] using
diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Compactness.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Compactness.lean
index 00cba3a..70360de 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Compactness.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Compactness.lean
@@ -1,15 +1,15 @@
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Smoothing
-import Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
-import Mathlib.MeasureTheory.Measure.Typeclasses.Finite
-import Mathlib.Topology.Algebra.Monoid
-import Mathlib.Topology.UniformSpace.HeineCantor
-
 /-
 Copyright (c) 2026 Adam Benenson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Benenson
 -/
 
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Smoothing
+import Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
+import Mathlib.MeasureTheory.Measure.Typeclasses.Finite
+import Mathlib.Topology.Algebra.Monoid
+import Mathlib.Topology.UniformSpace.HeineCantor
+
 /-!
 # `L²` compactness criterion: compact smoothing operator (Euclidean)
 
@@ -44,13 +44,14 @@ section Volume
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
 
-local instance instMeasurableSpaceE_L2CompactnessCompactness : MeasurableSpace E := borel E
-local instance instBorelSpaceE_L2CompactnessCompactness : BorelSpace E := ⟨rfl⟩
-local instance instOpensMeasurableSpaceE_L2CompactnessCompactness : OpensMeasurableSpace E := by
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceEL2CompactnessCompactness : MeasurableSpace E := borel E
+local instance instBorelSpaceEL2CompactnessCompactness : BorelSpace E := ⟨rfl⟩
+local instance instOpensMeasurableSpaceEL2CompactnessCompactness : OpensMeasurableSpace E := by
   infer_instance
-local instance instMeasurableAddE_L2CompactnessCompactness : MeasurableAdd E := by
+local instance instMeasurableAddEL2CompactnessCompactness : MeasurableAdd E := by
   infer_instance
-local instance instMeasurableNegE_L2CompactnessCompactness : MeasurableNeg E := by
+local instance instMeasurableNegEL2CompactnessCompactness : MeasurableNeg E := by
   infer_instance
 
 variable {K : Set E}
@@ -65,14 +66,15 @@ lemma isCompact_Kψ (hK : IsCompact K) (hψcs : HasCompactSupport ψ) :
     IsCompact (Kψ (K := K) (ψ := ψ)) :=
   IsCompact.add hK hψcs.isCompact
 
-private def smoothOn (hKm : MeasurableSet K) (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ)
+/-- Restrict the smoothed function to its compact domain as a continuous map. -/
+def smoothOn (hKm : MeasurableSet K) (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ)
     (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) (volume.restrict K)) :
     C(↥(Kψ (K := K) (ψ := ψ)), ℝ) where
   toFun x := smoothFun (E := E) (K := K) ψ u x
   continuous_toFun := by
     have : Continuous (smoothFun (E := E) (K := K) ψ u) :=
       continuous_smoothFun (E := E) (K := K) (ψ := ψ) (hKm := hKm) hψc hψcs u
-    simpa using this.comp continuous_subtype_val
+    exact this.comp continuous_subtype_val
 
 /-- `smoothFun` packaged as a `BoundedContinuousFunction` on the compact set `K + tsupport ψ`. -/
 def smoothBCF (hK : IsCompact K) (hKm : MeasurableSet K) (hψc : Continuous ψ)
@@ -106,7 +108,7 @@ lemma uniformContinuous_ψ (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ)
   -- If `ψ x` is `ε`-far from `0`, then `ψ x ≠ 0`, hence `x` belongs to the support and therefore
   -- to the topological support.
   have hx' : ¬ dist (ψ x) 0 < ε := by
-    simpa [Set.mem_compl_iff, Set.mem_setOf_eq] using hx
+    simpa [Set.mem_compl_iff, Set.mem_ofPred_eq] using hx
   have hxε : ε ≤ dist (ψ x) 0 := le_of_not_gt (by simpa [gt_iff_lt] using hx')
   have hx0 : ψ x ≠ 0 := by
     intro hψ0
@@ -130,10 +132,10 @@ private lemma integrable_norm_L2_restrict (hK : IsCompact K)
     Integrable (fun x : E => ‖u x‖) (volume.restrict K) := by
   classical
   -- On a finite measure space, `L² ⊆ L¹`.
-  have hμ : (volume : Measure E) K < ∞ :=
+  have hμ : (volume : Measure E) K < (⊤ : ℝ≥0∞) :=
     (hK.measure_lt_top (μ := (volume : Measure E)))
-  letI : Fact ((volume : Measure E) K < ∞) := ⟨hμ⟩
-  haveI : IsFiniteMeasure (volume.restrict K) := by
+  let : Fact ((volume : Measure E) K < (⊤ : ℝ≥0∞)) := ⟨hμ⟩
+  have : IsFiniteMeasure (volume.restrict K) := by
     infer_instance
   have hu2 : MemLp (fun x : E => u x) (2 : ℝ≥0∞) (volume.restrict K) :=
     MeasureTheory.Lp.memLp u
diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/FrechetKolmogorov.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/FrechetKolmogorov.lean
index 6af8031..35c2ec0 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/FrechetKolmogorov.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/FrechetKolmogorov.lean
@@ -1,13 +1,13 @@
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Approximation
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Transfer
-import Mathlib.Topology.UniformSpace.Cauchy
-
 /-
 Copyright (c) 2026 Adam Benenson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Benenson
 -/
 
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Approximation
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Transfer
+import Mathlib.Topology.UniformSpace.Cauchy
+
 /-!
 # `L²` compactness criterion: Fréchet–Kolmogorov (Euclidean, compact support case)
 
@@ -52,13 +52,14 @@ section Volume
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
 
-local instance instMeasurableSpaceE_L2CompactnessFrechetKolmogorov : MeasurableSpace E := borel E
-local instance instBorelSpaceE_L2CompactnessFrechetKolmogorov : BorelSpace E := ⟨rfl⟩
-local instance instOpensMeasurableSpaceE_L2CompactnessFrechetKolmogorov :
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceEL2CompactnessFrechetKolmogorov : MeasurableSpace E := borel E
+local instance instBorelSpaceEL2CompactnessFrechetKolmogorov : BorelSpace E := ⟨rfl⟩
+local instance instOpensMeasurableSpaceEL2CompactnessFrechetKolmogorov :
     OpensMeasurableSpace E := by infer_instance
-local instance instMeasurableAddE_L2CompactnessFrechetKolmogorov : MeasurableAdd E := by
+local instance instMeasurableAddEL2CompactnessFrechetKolmogorov : MeasurableAdd E := by
   infer_instance
-local instance instMeasurableNegE_L2CompactnessFrechetKolmogorov : MeasurableNeg E := by
+local instance instMeasurableNegEL2CompactnessFrechetKolmogorov : MeasurableNeg E := by
   infer_instance
 
 variable {K : Set E} {ψ : E → ℝ}
@@ -125,7 +126,7 @@ theorem totallyBounded_extendByZeroL2_image_of_forall_exists_translationIntegral
   rcases Set.mem_iUnion.1 hSu_cover with ⟨y, hy⟩
   rcases Set.mem_iUnion.1 hy with ⟨hyT, hyBall⟩
   have hyDist : dist (smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs u) y < ε / 2 := by
-    simpa [Metric.ball, Set.mem_setOf_eq] using hyBall
+    simpa [Metric.ball, Set.mem_ofPred_eq] using hyBall
   have hdist_smooth_ext :
       dist (extendByZeroL2 (E := E) (K := K) hKm u)
           (smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs u) ≤ ε / 2 := by
@@ -156,7 +157,7 @@ theorem totallyBounded_extendByZeroL2_image_of_forall_exists_translationIntegral
       lt_of_le_of_lt htri hlt
     simpa [add_halves ε] using htmp
   have hxBall : extendByZeroL2 (E := E) (K := K) hKm u ∈ Metric.ball y ε := by
-    simpa [Metric.ball, Set.mem_setOf_eq] using hxDist
+    simpa [Metric.ball, Set.mem_ofPred_eq] using hxDist
   exact Set.mem_iUnion.2 ⟨y, Set.mem_iUnion.2 ⟨hyT, hxBall⟩⟩
 
 theorem isCompact_closure_extendByZeroL2_image_of_forall_exists_translationIntegral_small
diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Kernels.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Kernels.lean
index 833b243..8543986 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Kernels.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Kernels.lean
@@ -1,22 +1,22 @@
-import Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
-import Mathlib.MeasureTheory.Integral.Bochner.Set
-import Mathlib.Topology.Algebra.Support
-
 /-
 Copyright (c) 2026 Adam Benenson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Benenson
 -/
 
+import Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
+import Mathlib.MeasureTheory.Integral.Bochner.Set
+import Mathlib.Topology.Algebra.Support
+
 /-!
 # `L²` compactness criterion: existence of small-support probability kernels (Euclidean)
 
 This file provides a “kernel factory” for the Euclidean Fréchet–Kolmogorov / Riesz–Kolmogorov
-criterion: for any radius `δ > 0`, produce a continuous compactly supported function `ψ : E → ℝ`
+criterion: for any radius `deltaLoss > 0`, produce a continuous compactly supported function `ψ : E → ℝ`
 such that:
 
 - `ψ ≥ 0`,
-- `tsupport ψ ⊆ Metric.ball 0 δ`,
+- `tsupport ψ ⊆ Metric.ball 0 deltaLoss`,
 - `∫ ψ = 1` (so `kernelMeasure ψ` is a probability measure).
 
 The construction uses mathlib’s `exists_smooth_tsupport_subset` bump-function lemma and normalizes
@@ -41,21 +41,22 @@ section Volume
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
 
-local instance instMeasurableSpaceE_L2CompactnessKernels : MeasurableSpace E := borel E
-local instance instBorelSpaceE_L2CompactnessKernels : BorelSpace E := ⟨rfl⟩
-local instance instOpensMeasurableSpaceE_L2CompactnessKernels : OpensMeasurableSpace E := by
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceEL2CompactnessKernels : MeasurableSpace E := borel E
+local instance instBorelSpaceEL2CompactnessKernels : BorelSpace E := ⟨rfl⟩
+local instance instOpensMeasurableSpaceEL2CompactnessKernels : OpensMeasurableSpace E := by
   infer_instance
 
-/-- For any `δ > 0`, there exists a continuous compactly supported kernel `ψ` supported in
-`Metric.ball 0 δ`, with `ψ ≥ 0` and `∫ ψ = 1` (w.r.t. Lebesgue measure). -/
-theorem exists_kernel_tsupport_subset_ball_integral_eq_one {δ : ℝ} (hδ : 0 < δ) :
+/-- For any `deltaLoss > 0`, there exists a continuous compactly supported kernel `ψ` supported in
+`Metric.ball 0 deltaLoss`, with `ψ ≥ 0` and `∫ ψ = 1` (w.r.t. Lebesgue measure). -/
+theorem exists_kernel_tsupport_subset_ball_integral_eq_one {deltaLoss : ℝ} (hδ : 0 < deltaLoss) :
     ∃ ψ : E → ℝ, Continuous ψ ∧ HasCompactSupport ψ ∧ (∀ x, 0 ≤ ψ x) ∧
-      (∫ x, ψ x ∂(volume : Measure E) = 1) ∧ tsupport ψ ⊆ Metric.ball (0 : E) δ := by
+      (∫ x, ψ x ∂(volume : Measure E) = 1) ∧ tsupport ψ ⊆ Metric.ball (0 : E) deltaLoss := by
   classical
-  -- Start from a smooth bump supported in `ball 0 δ` with value `1` at `0`.
-  have hs : (Metric.ball (0 : E) δ) ∈ 𝓝 (0 : E) := Metric.ball_mem_nhds _ hδ
+  -- Start from a smooth bump supported in `ball 0 deltaLoss` with value `1` at `0`.
+  have hs : (Metric.ball (0 : E) deltaLoss) ∈ 𝓝 (0 : E) := Metric.ball_mem_nhds _ hδ
   rcases exists_contDiff_tsupport_subset (n := ⊤)
-    (E := E) (s := Metric.ball (0 : E) δ) (x := (0 : E)) hs with
+    (E := E) (s := Metric.ball (0 : E) deltaLoss) (x := (0 : E)) hs with
     ⟨f, hf_tsupp, hf_cs, hf_smooth, hf_range, hf0⟩
   have hf_cont : Continuous f := hf_smooth.continuous
   have hf_nonneg : ∀ x, 0 ≤ f x := by
@@ -77,9 +78,9 @@ theorem exists_kernel_tsupport_subset_ball_integral_eq_one {δ : ℝ} (hδ : 0 <
   -- Normalize: `ψ = I⁻¹ • f`.
   let ψ : E → ℝ := fun x => I⁻¹ * f x
   have hψc : Continuous ψ := by
-    simpa [ψ] using (continuous_const.mul hf_cont)
+    exact (continuous_const.mul hf_cont)
   have hψcs : HasCompactSupport ψ := by
-    simpa [ψ, smul_eq_mul] using
+    exact
       (HasCompactSupport.smul_left (f := fun _x : E => I⁻¹) (f' := f) hf_cs)
   have hψ0 : ∀ x, 0 ≤ ψ x := by
     intro x
@@ -93,7 +94,7 @@ theorem exists_kernel_tsupport_subset_ball_integral_eq_one {δ : ℝ} (hδ : 0 <
       simpa [ψ, I] using
         (MeasureTheory.integral_const_mul (μ := (volume : Measure E)) (r := I⁻¹) (f := f))
     simp [this, hI0]
-  have hψ_tsupp : tsupport ψ ⊆ Metric.ball (0 : E) δ := by
+  have hψ_tsupp : tsupport ψ ⊆ Metric.ball (0 : E) deltaLoss := by
     -- Scaling does not enlarge topological support; use the bump support inclusion.
     have hsub : tsupport ψ ⊆ tsupport f := by
       simpa [ψ, smul_eq_mul] using (tsupport_smul_subset_right (f := fun _x : E => I⁻¹) (g := f))
diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Smoothing.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Smoothing.lean
index 3543832..8d6b0bb 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Smoothing.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Smoothing.lean
@@ -1,13 +1,13 @@
-import RellichKondrachov.MeasureTheory.Function.LpSpace.Restrict
-import Mathlib.Analysis.Convolution
-import Mathlib.Topology.Algebra.Support
-
 /-
 Copyright (c) 2026 Adam Benenson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Benenson
 -/
 
+import RellichKondrachov.MeasureTheory.Function.LpSpace.Restrict
+import Mathlib.Analysis.Convolution
+import Mathlib.Topology.Algebra.Support
+
 /-!
 # `L²` compactness criterion: smoothing setup (Euclidean)
 
@@ -38,11 +38,12 @@ section
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
 
-local instance : MeasurableSpace E := borel E
-local instance : BorelSpace E := ⟨rfl⟩
-local instance : OpensMeasurableSpace E := by
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceSmoothing : MeasurableSpace E := borel E
+local instance instBorelSpaceSmoothing : BorelSpace E := ⟨rfl⟩
+local instance instOpensMeasurableSpaceSmoothing : OpensMeasurableSpace E := by
   infer_instance
-local instance : MeasurableAdd E := by
+local instance instMeasurableAddSmoothing : MeasurableAdd E := by
   infer_instance
 
 omit [InnerProductSpace ℝ E] [CompleteSpace E] in
@@ -68,11 +69,12 @@ section Volume
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
 
 -- `volume` is the canonical Haar measure on finite-dimensional real vector spaces.
-local instance : MeasurableSpace E := borel E
-local instance : BorelSpace E := ⟨rfl⟩
-local instance : OpensMeasurableSpace E := by
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceSmoothing1 : MeasurableSpace E := borel E
+local instance instBorelSpaceSmoothing1 : BorelSpace E := ⟨rfl⟩
+local instance instOpensMeasurableSpaceSmoothing1 : OpensMeasurableSpace E := by
   infer_instance
-local instance : MeasurableAdd E := by
+local instance instMeasurableAddSmoothing1 : MeasurableAdd E := by
   infer_instance
 
 variable {K : Set E}
@@ -116,7 +118,7 @@ lemma extendByZeroL2_eq_extendByZeroₗᵢ (hKm : MeasurableSet K)
       (MeasureTheory.Lp.extendByZeroₗᵢ (μ := (volume : Measure E)) (E := ℝ) (p := (2 : ℝ≥0∞))
         (s := K) hKm) u := by
   classical
-  letI : Fact (1 ≤ (2 : ℝ≥0∞)) := ⟨by norm_num⟩
+  let : Fact (1 ≤ (2 : ℝ≥0∞)) := ⟨by norm_num⟩
   refine MeasureTheory.Lp.ext ?_
   have h1 :
       (extendByZeroL2 (E := E) (K := K) hKm u : E → ℝ) =ᵐ[(volume : Measure E)]
@@ -126,7 +128,6 @@ lemma extendByZeroL2_eq_extendByZeroₗᵢ (hKm : MeasurableSet K)
       ((MeasureTheory.Lp.extendByZeroₗᵢ (μ := (volume : Measure E)) (E := ℝ) (p := (2 : ℝ≥0∞))
         (s := K) hKm) u : E → ℝ) =ᵐ[(volume : Measure E)]
         extendByZeroFun (E := E) (K := K) u := by
-    simp [extendByZeroFun]
     exact
       (MeasureTheory.Lp.extendByZeroₗᵢ_ae_eq (μ := (volume : Measure E)) (E := ℝ)
         (p := (2 : ℝ≥0∞)) (s := K) hKm u)
@@ -136,7 +137,7 @@ lemma norm_extendByZeroL2 (hKm : MeasurableSet K)
     (u : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) (volume.restrict K)) :
     ‖extendByZeroL2 (E := E) (K := K) hKm u‖ = ‖u‖ := by
   classical
-  letI : Fact (1 ≤ (2 : ℝ≥0∞)) := ⟨by norm_num⟩
+  let : Fact (1 ≤ (2 : ℝ≥0∞)) := ⟨by norm_num⟩
   calc
     ‖extendByZeroL2 (E := E) (K := K) hKm u‖ =
         ‖(MeasureTheory.Lp.extendByZeroₗᵢ (μ := (volume : Measure E)) (E := ℝ) (p := (2 : ℝ≥0∞))
@@ -172,7 +173,7 @@ lemma continuous_smoothFun
     exact hf_memLp.locallyIntegrable h12
   simpa [smoothFun] using
     (hψcs.continuous_convolution_right
-      (L := ContinuousLinearMap.lsmul ℝ ℝ)
+      («L» := ContinuousLinearMap.lsmul ℝ ℝ)
       (μ := (volume : Measure E)) hf_loc hψc)
 
 lemma hasCompactSupport_smoothFun (hK : IsCompact K) (hψcs : HasCompactSupport ψ)
@@ -181,7 +182,7 @@ lemma hasCompactSupport_smoothFun (hK : IsCompact K) (hψcs : HasCompactSupport
   have hf : HasCompactSupport (extendByZeroFun (K := K) u) :=
     hasCompactSupport_extendByZeroFun (K := K) hK u
   simpa [smoothFun] using
-    (hf.convolution (L := ContinuousLinearMap.lsmul ℝ ℝ)
+    (hf.convolution («L» := ContinuousLinearMap.lsmul ℝ ℝ)
       (μ := (volume : Measure E)) hψcs)
 
 lemma support_smoothFun_subset_add_tsupport
@@ -192,7 +193,7 @@ lemma support_smoothFun_subset_add_tsupport
       Function.support (smoothFun (E := E) (K := K) ψ u) ⊆
         Function.support (extendByZeroFun (E := E) (K := K) u) + Function.support ψ := by
     simpa [smoothFun] using
-      (support_convolution_subset (L := ContinuousLinearMap.lsmul ℝ ℝ) (μ := (volume : Measure E))
+      (support_convolution_subset («L» := ContinuousLinearMap.lsmul ℝ ℝ) (μ := (volume : Measure E))
         (f := extendByZeroFun (E := E) (K := K) u) (g := ψ))
   have h1 : Function.support (extendByZeroFun (E := E) (K := K) u) ⊆ K := by
     simp [extendByZeroFun]
diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Transfer.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Transfer.lean
index 51414a8..2be859b 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Transfer.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Transfer.lean
@@ -1,13 +1,13 @@
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.ArzelaAscoli
-import Mathlib.MeasureTheory.Function.LpSpace.Basic
-import Mathlib.Topology.MetricSpace.Pseudo.Basic
-
 /-
 Copyright (c) 2026 Adam Benenson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Benenson
 -/
 
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.ArzelaAscoli
+import Mathlib.MeasureTheory.Function.LpSpace.Basic
+import Mathlib.Topology.MetricSpace.Pseudo.Basic
+
 /-!
 # `L²` compactness criterion: transfer from `BCF` compactness to `L²` (Euclidean)
 
@@ -39,32 +39,217 @@ section Volume
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
 
-local instance instMeasurableSpaceE_L2CompactnessTransfer : MeasurableSpace E := borel E
-local instance instBorelSpaceE_L2CompactnessTransfer : BorelSpace E := ⟨rfl⟩
-local instance instOpensMeasurableSpaceE_L2CompactnessTransfer : OpensMeasurableSpace E := by
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceEL2CompactnessTransfer : MeasurableSpace E := borel E
+local instance instBorelSpaceEL2CompactnessTransfer : BorelSpace E := ⟨rfl⟩
+local instance instOpensMeasurableSpaceEL2CompactnessTransfer : OpensMeasurableSpace E := by
   infer_instance
-local instance instMeasurableAddE_L2CompactnessTransfer : MeasurableAdd E := by
+local instance instMeasurableAddEL2CompactnessTransfer : MeasurableAdd E := by
   infer_instance
-local instance instMeasurableNegE_L2CompactnessTransfer : MeasurableNeg E := by
+local instance instMeasurableNegEL2CompactnessTransfer : MeasurableNeg E := by
   infer_instance
 
 variable {K : Set E} {ψ : E → ℝ}
 
+private lemma dist_smoothL2_le_mul_dist_smoothBCF (hK : IsCompact K) (hKm : MeasurableSet K)
+    (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ) :
+    ∀ u v : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) (volume.restrict K),
+      dist (smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs u)
+          (smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs v) ≤
+        (MeasureTheory.measureUnivNNReal ((volume : Measure E).restrict (Kψ (K := K) (ψ := ψ)))) ^
+            ((2 : ℝ≥0∞).toReal⁻¹) *
+          dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u)
+              (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs v) := by
+  classical
+  let : Fact (1 ≤ (2 : ℝ≥0∞)) := ⟨by norm_num⟩
+  let s : Set E := Kψ (K := K) (ψ := ψ)
+  have hs_compact : IsCompact s := isCompact_Kψ (K := K) (ψ := ψ) hK hψcs
+  have hs : MeasurableSet s := hs_compact.measurableSet
+  have hs_lt_top : (volume : Measure E) s < (⊤ : ℝ≥0∞) :=
+    hs_compact.measure_lt_top (μ := (volume : Measure E))
+  let μs : Measure E := (volume : Measure E).restrict s
+  have : Fact ((volume : Measure E) s < (⊤ : ℝ≥0∞)) := ⟨hs_lt_top⟩
+  have : IsFiniteMeasure μs := by
+    infer_instance
+  let mS : ℝ := (MeasureTheory.measureUnivNNReal μs) ^ ((2 : ℝ≥0∞).toReal⁻¹)
+  intro u v
+  set Su :=
+    smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs u
+  set Sv :=
+    smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs v
+  set Bu :=
+    smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u
+  set Bv :=
+    smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs v
+  have hBuBv : 0 ≤ ‖Bu - Bv‖ := norm_nonneg _
+  -- Work on `F := Su - Sv` and restrict to the finite-measure set `s`.
+  let F : (E →₂[(volume : Measure E)] ℝ) := Su - Sv
+  let g : E → ℝ := fun x => (F : E → ℝ) x
+  have hg : MeasureTheory.MemLp g (2 : ℝ≥0∞) (volume : Measure E) := MeasureTheory.Lp.memLp F
+  have hg_restrict : MeasureTheory.MemLp g (2 : ℝ≥0∞) μs := hg.restrict s
+  let Fs : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μs := hg_restrict.toLp g
+  -- Show `Fs` is pointwise bounded by `‖Bu - Bv‖` on `μs`.
+  have hF_ae :
+      (g =ᵐ[μs] fun x : E =>
+        smoothFun (E := E) (K := K) ψ u x -
+          smoothFun (E := E) (K := K) ψ v x) := by
+    have hsub :
+        (F : E → ℝ) =ᵐ[(volume : Measure E)] (Su : E → ℝ) - (Sv : E → ℝ) := by
+      simpa [F, g, Su, Sv] using
+        (MeasureTheory.Lp.coeFn_sub (μ := (volume : Measure E)) Su Sv)
+    have hu :
+        (Su : E → ℝ) =ᵐ[(volume : Measure E)] smoothFun (E := E) (K := K) ψ u :=
+      smoothL2_ae_eq (E := E) (K := K) (ψ := ψ) (hK := hK) (hKm := hKm) hψc hψcs u
+    have hv :
+        (Sv : E → ℝ) =ᵐ[(volume : Measure E)] smoothFun (E := E) (K := K) ψ v :=
+      smoothL2_ae_eq (E := E) (K := K) (ψ := ψ) (hK := hK) (hKm := hKm) hψc hψcs v
+    have hF :
+        (F : E → ℝ) =ᵐ[(volume : Measure E)]
+          fun x : E =>
+            smoothFun (E := E) (K := K) ψ u x - smoothFun (E := E) (K := K) ψ v x := by
+      have h := hsub.trans (hu.sub hv)
+      filter_upwards [h] with x hx
+      simpa [Pi.sub_apply] using hx
+    exact MeasureTheory.ae_restrict_of_ae (μ := (volume : Measure E)) (s := s) hF
+  have hFs_ae : ((Fs : E → ℝ) =ᵐ[μs] g) := by
+    simpa [Fs, g] using
+      (MeasureTheory.MemLp.coeFn_toLp (μ := μs) (p := (2 : ℝ≥0∞)) (f := g) hg_restrict)
+  have hbound :
+      ∀ᵐ x ∂μs, ‖Fs x‖ ≤ ‖Bu - Bv‖ := by
+    have hpoint :
+        ∀ x : E, x ∈ s → ‖smoothFun (E := E) (K := K) ψ u x - smoothFun (E := E) (K := K) ψ v x‖ ≤
+          ‖Bu - Bv‖ := by
+      intro x hx
+      let x' : ↥(Kψ (K := K) (ψ := ψ)) := ⟨x, hx⟩
+      have hBu : Bu x' = smoothFun (E := E) (K := K) ψ u x := by
+        simp [Bu, x']
+      have hBv : Bv x' = smoothFun (E := E) (K := K) ψ v x := by
+        simp [Bv, x']
+      have : ‖(Bu - Bv) x'‖ ≤ ‖Bu - Bv‖ :=
+        (Bu - Bv).norm_coe_le_norm x'
+      simpa [hBu, hBv] using this
+    filter_upwards
+      [MeasureTheory.ae_restrict_mem (μ := (volume : Measure E)) hs,
+        hFs_ae, hF_ae] with x hx hFs hF
+    have := hpoint x hx
+    -- rewrite through the AE equalities
+    simpa [hFs, hF] using this
+  have hnorm_Fs : ‖Fs‖ ≤ mS * ‖Bu - Bv‖ := by
+    have := (MeasureTheory.Lp.norm_le_of_ae_bound (μ := μs) (p := (2 : ℝ≥0∞))
+      (f := Fs) (hC := hBuBv) hbound)
+    simpa [mS] using this
+  -- Relate the `L²` norm on `volume` to the restricted norm on `μs` using extension-by-zero.
+  have hsupport :
+      ∀ x : E, x ∉ s →
+        smoothFun (E := E) (K := K) ψ u x -
+          smoothFun (E := E) (K := K) ψ v x = 0 := by
+    intro x hx
+    have hu_supp : Function.support (smoothFun (E := E) (K := K) ψ u) ⊆ s := by
+      exact
+        (support_smoothFun_subset_add_tsupport (E := E) (K := K) (ψ := ψ) u)
+    have hv_supp : Function.support (smoothFun (E := E) (K := K) ψ v) ⊆ s := by
+      exact
+        (support_smoothFun_subset_add_tsupport (E := E) (K := K) (ψ := ψ) v)
+    have hu0 : smoothFun (E := E) (K := K) ψ u x = 0 := by
+      have : x ∉ Function.support (smoothFun (E := E) (K := K) ψ u) := fun hx' => hx (hu_supp hx')
+      simpa [Function.support] using this
+    have hv0 : smoothFun (E := E) (K := K) ψ v x = 0 := by
+      have : x ∉ Function.support (smoothFun (E := E) (K := K) ψ v) := fun hx' => hx (hv_supp hx')
+      simpa [Function.support] using this
+    simp [hu0, hv0]
+  have hF0 :
+      ∀ᵐ x ∂(volume : Measure E), x ∉ s → g x = 0 := by
+    have hF_ae_full :
+        (g =ᵐ[(volume : Measure E)]
+          fun x : E =>
+            smoothFun (E := E) (K := K) ψ u x -
+              smoothFun (E := E) (K := K) ψ v x) := by
+      have hsub :
+          (F : E → ℝ) =ᵐ[(volume : Measure E)] (Su : E → ℝ) - (Sv : E → ℝ) := by
+        simpa [F, g, Su, Sv] using
+          (MeasureTheory.Lp.coeFn_sub (μ := (volume : Measure E)) Su Sv)
+      have hu :
+          (Su : E → ℝ) =ᵐ[(volume : Measure E)] smoothFun (E := E) (K := K) ψ u :=
+        smoothL2_ae_eq (E := E) (K := K) (ψ := ψ) (hK := hK) (hKm := hKm) hψc hψcs u
+      have hv :
+          (Sv : E → ℝ) =ᵐ[(volume : Measure E)] smoothFun (E := E) (K := K) ψ v :=
+        smoothL2_ae_eq (E := E) (K := K) (ψ := ψ) (hK := hK) (hKm := hKm) hψc hψcs v
+      have hF :
+          (F : E → ℝ) =ᵐ[(volume : Measure E)]
+            fun x : E =>
+              smoothFun (E := E) (K := K) ψ u x - smoothFun (E := E) (K := K) ψ v x := by
+        have h := hsub.trans (hu.sub hv)
+        filter_upwards [h] with x hx
+        simpa [Pi.sub_apply] using hx
+      simpa [g] using hF
+    filter_upwards [hF_ae_full] with x hx
+    intro hxnot
+    have : smoothFun (E := E) (K := K) ψ u x - smoothFun (E := E) (K := K) ψ v x = 0 :=
+      hsupport x hxnot
+    simpa [hx] using this
+  have hF_ind :
+      (s.indicator g =ᵐ[(volume : Measure E)] g) := by
+    filter_upwards [hF0] with x hx
+    by_cases hxmem : x ∈ s
+    · simp [g, hxmem]
+    · have : g x = 0 := hx hxmem
+      simp [g, hxmem, this]
+  -- Conclude `‖F‖ = ‖Fs‖` using `extendByZeroₗᵢ` and the indicator identity.
+  let Fext :
+      MeasureTheory.Lp ℝ (2 : ℝ≥0∞) (volume : Measure E) :=
+    (MeasureTheory.Lp.extendByZeroₗᵢ (μ := (volume : Measure E)) (E := ℝ) (p := (2 : ℝ≥0∞))
+      (s := s) hs) Fs
+  have hFext_ae :
+      ((Fext : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) (volume : Measure E)) :
+          E → ℝ) =ᵐ[(volume : Measure E)]
+        s.indicator fun x : E => (Fs : E → ℝ) x := by
+    simpa [Fext] using
+      (MeasureTheory.Lp.extendByZeroₗᵢ_ae_eq
+        (μ := (volume : Measure E)) (p := (2 : ℝ≥0∞))
+        (s := s) hs Fs)
+  have hFs_on :
+      ∀ᵐ x ∂(volume : Measure E), x ∈ s → (Fs : E → ℝ) x = g x := by
+    -- rewrite the AE equality `Fs = g` on the restricted measure as an implication on `volume`
+    have := (MeasureTheory.ae_restrict_iff' (μ := (volume : Measure E)) (s := s) hs).1 hFs_ae
+    simpa [g] using this
+  have hindicator :
+      (s.indicator (fun x : E => (Fs : E → ℝ) x) =ᵐ[(volume : Measure E)] s.indicator g) := by
+    filter_upwards [hFs_on] with x hx
+    by_cases hxmem : x ∈ s
+    · simp [hxmem, hx hxmem]
+    · simp [hxmem]
+  have hFext_ae' :
+      (Fext : E → ℝ) =ᵐ[(volume : Measure E)] g := by
+    exact hFext_ae.trans (hindicator.trans hF_ind)
+  have hFext_eq : Fext = F := by
+    refine MeasureTheory.Lp.ext ?_
+    simpa [g, F] using hFext_ae'
+  have hnorm_F : ‖F‖ ≤ mS * ‖Bu - Bv‖ := by
+    -- use `‖F‖ = ‖Fs‖` via the isometry.
+    have hnorm_ext : ‖Fext‖ = ‖Fs‖ := by
+      simp [Fext]
+    -- `Fext = F` and `Fs` is bounded.
+    have : ‖Fext‖ ≤ mS * ‖Bu - Bv‖ := by
+      simpa [hnorm_ext] using hnorm_Fs
+    simpa [hFext_eq] using this
+  -- Convert to the `dist` statement.
+  simpa [Su, Sv, Bu, Bv, F, dist_eq_norm, mS, mul_assoc] using hnorm_F
+
 theorem smoothL2_image_closedBall_isCompact (hK : IsCompact K) (hKm : MeasurableSet K)
     (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ) {R : ℝ} (hR : 0 ≤ R) :
     IsCompact
         (closure
           (smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs '' Metric.closedBall (0 : _) R)) := by
   classical
-  letI : Fact (1 ≤ (2 : ℝ≥0∞)) := ⟨by norm_num⟩
+  let : Fact (1 ≤ (2 : ℝ≥0∞)) := ⟨by norm_num⟩
   let s : Set E := Kψ (K := K) (ψ := ψ)
   have hs_compact : IsCompact s := isCompact_Kψ (K := K) (ψ := ψ) hK hψcs
   have hs : MeasurableSet s := hs_compact.measurableSet
-  have hs_lt_top : (volume : Measure E) s < ∞ :=
+  have hs_lt_top : (volume : Measure E) s < (⊤ : ℝ≥0∞) :=
     hs_compact.measure_lt_top (μ := (volume : Measure E))
   let μs : Measure E := (volume : Measure E).restrict s
-  haveI : Fact ((volume : Measure E) s < ∞) := ⟨hs_lt_top⟩
-  haveI : IsFiniteMeasure μs := by
+  have : Fact ((volume : Measure E) s < (⊤ : ℝ≥0∞)) := ⟨hs_lt_top⟩
+  have : IsFiniteMeasure μs := by
     infer_instance
   let mS : ℝ := (MeasureTheory.measureUnivNNReal μs) ^ ((2 : ℝ≥0∞).toReal⁻¹)
   have hmS : 0 ≤ mS := by
@@ -79,178 +264,14 @@ theorem smoothL2_image_closedBall_isCompact (hK : IsCompact K) (hKm : Measurable
     smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs '' U
   have hA_compact : IsCompact (closure A) :=
     smoothBCF_image_closedBall_isCompact (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs (R := R) hR
-  have hdist_smoothL2_le :
-      ∀ u v : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) (volume.restrict K),
-        dist (smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs u)
-            (smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs v) ≤
-          mS *
-            dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u)
-                (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs v) := by
-    intro u v
-    set Su :=
-      smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs u
-    set Sv :=
-      smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs v
-    set Bu :=
-      smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u
-    set Bv :=
-      smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs v
-    have hBuBv : 0 ≤ ‖Bu - Bv‖ := norm_nonneg _
-    -- Work on `F := Su - Sv` and restrict to the finite-measure set `s`.
-    let F : (E →₂[(volume : Measure E)] ℝ) := Su - Sv
-    let g : E → ℝ := fun x => (F : E → ℝ) x
-    have hg : MeasureTheory.MemLp g (2 : ℝ≥0∞) (volume : Measure E) := MeasureTheory.Lp.memLp F
-    have hg_restrict : MeasureTheory.MemLp g (2 : ℝ≥0∞) μs := hg.restrict s
-    let Fs : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) μs := hg_restrict.toLp g
-    -- Show `Fs` is pointwise bounded by `‖Bu - Bv‖` on `μs`.
-    have hF_ae :
-        (g =ᵐ[μs] fun x : E =>
-          smoothFun (E := E) (K := K) ψ u x -
-            smoothFun (E := E) (K := K) ψ v x) := by
-      have hsub :
-          (F : E → ℝ) =ᵐ[(volume : Measure E)] (Su : E → ℝ) - (Sv : E → ℝ) := by
-        simpa [F, g, Su, Sv] using
-          (MeasureTheory.Lp.coeFn_sub (μ := (volume : Measure E)) Su Sv)
-      have hu :
-          (Su : E → ℝ) =ᵐ[(volume : Measure E)] smoothFun (E := E) (K := K) ψ u :=
-        smoothL2_ae_eq (E := E) (K := K) (ψ := ψ) (hK := hK) (hKm := hKm) hψc hψcs u
-      have hv :
-          (Sv : E → ℝ) =ᵐ[(volume : Measure E)] smoothFun (E := E) (K := K) ψ v :=
-        smoothL2_ae_eq (E := E) (K := K) (ψ := ψ) (hK := hK) (hKm := hKm) hψc hψcs v
-      have hF :
-          (F : E → ℝ) =ᵐ[(volume : Measure E)]
-            fun x : E =>
-              smoothFun (E := E) (K := K) ψ u x - smoothFun (E := E) (K := K) ψ v x := by
-        simpa [Pi.sub_apply] using hsub.trans (hu.sub hv)
-      exact MeasureTheory.ae_restrict_of_ae (μ := (volume : Measure E)) (s := s) hF
-    have hFs_ae : ((Fs : E → ℝ) =ᵐ[μs] g) := by
-      simpa [Fs, g] using
-        (MeasureTheory.MemLp.coeFn_toLp (μ := μs) (p := (2 : ℝ≥0∞)) (f := g) hg_restrict)
-    have hbound :
-        ∀ᵐ x ∂μs, ‖Fs x‖ ≤ ‖Bu - Bv‖ := by
-      have hpoint :
-          ∀ x : E, x ∈ s → ‖smoothFun (E := E) (K := K) ψ u x - smoothFun (E := E) (K := K) ψ v x‖ ≤
-            ‖Bu - Bv‖ := by
-        intro x hx
-        let x' : ↥(Kψ (K := K) (ψ := ψ)) := ⟨x, hx⟩
-        have hBu : Bu x' = smoothFun (E := E) (K := K) ψ u x := by
-          simp [Bu, x']
-        have hBv : Bv x' = smoothFun (E := E) (K := K) ψ v x := by
-          simp [Bv, x']
-        have : ‖(Bu - Bv) x'‖ ≤ ‖Bu - Bv‖ :=
-          (Bu - Bv).norm_coe_le_norm x'
-        simpa [hBu, hBv] using this
-      filter_upwards
-        [MeasureTheory.ae_restrict_mem (μ := (volume : Measure E)) hs,
-          hFs_ae, hF_ae] with x hx hFs hF
-      have := hpoint x hx
-      -- rewrite through the AE equalities
-      simpa [hFs, hF] using this
-    have hnorm_Fs : ‖Fs‖ ≤ mS * ‖Bu - Bv‖ := by
-      have := (MeasureTheory.Lp.norm_le_of_ae_bound (μ := μs) (p := (2 : ℝ≥0∞))
-        (f := Fs) (hC := hBuBv) hbound)
-      simpa [mS] using this
-    -- Relate the `L²` norm on `volume` to the restricted norm on `μs` using extension-by-zero.
-    have hsupport :
-        ∀ x : E, x ∉ s →
-          smoothFun (E := E) (K := K) ψ u x -
-            smoothFun (E := E) (K := K) ψ v x = 0 := by
-      intro x hx
-      have hu_supp : Function.support (smoothFun (E := E) (K := K) ψ u) ⊆ s := by
-        simpa [s] using
-          (support_smoothFun_subset_add_tsupport (E := E) (K := K) (ψ := ψ) u)
-      have hv_supp : Function.support (smoothFun (E := E) (K := K) ψ v) ⊆ s := by
-        simpa [s] using
-          (support_smoothFun_subset_add_tsupport (E := E) (K := K) (ψ := ψ) v)
-      have hu0 : smoothFun (E := E) (K := K) ψ u x = 0 := by
-        have : x ∉ Function.support (smoothFun (E := E) (K := K) ψ u) := fun hx' => hx (hu_supp hx')
-        simpa [Function.support] using this
-      have hv0 : smoothFun (E := E) (K := K) ψ v x = 0 := by
-        have : x ∉ Function.support (smoothFun (E := E) (K := K) ψ v) := fun hx' => hx (hv_supp hx')
-        simpa [Function.support] using this
-      simp [hu0, hv0]
-    have hF0 :
-        ∀ᵐ x ∂(volume : Measure E), x ∉ s → g x = 0 := by
-      have hF_ae_full :
-          (g =ᵐ[(volume : Measure E)]
-            fun x : E =>
-              smoothFun (E := E) (K := K) ψ u x -
-                smoothFun (E := E) (K := K) ψ v x) := by
-        have hsub :
-            (F : E → ℝ) =ᵐ[(volume : Measure E)] (Su : E → ℝ) - (Sv : E → ℝ) := by
-          simpa [F, g, Su, Sv] using
-            (MeasureTheory.Lp.coeFn_sub (μ := (volume : Measure E)) Su Sv)
-        have hu :
-            (Su : E → ℝ) =ᵐ[(volume : Measure E)] smoothFun (E := E) (K := K) ψ u :=
-          smoothL2_ae_eq (E := E) (K := K) (ψ := ψ) (hK := hK) (hKm := hKm) hψc hψcs u
-        have hv :
-            (Sv : E → ℝ) =ᵐ[(volume : Measure E)] smoothFun (E := E) (K := K) ψ v :=
-          smoothL2_ae_eq (E := E) (K := K) (ψ := ψ) (hK := hK) (hKm := hKm) hψc hψcs v
-        have hF :
-            (F : E → ℝ) =ᵐ[(volume : Measure E)]
-              fun x : E =>
-                smoothFun (E := E) (K := K) ψ u x - smoothFun (E := E) (K := K) ψ v x := by
-          simpa [Pi.sub_apply] using hsub.trans (hu.sub hv)
-        simpa [g] using hF
-      filter_upwards [hF_ae_full] with x hx
-      intro hxnot
-      have : smoothFun (E := E) (K := K) ψ u x - smoothFun (E := E) (K := K) ψ v x = 0 :=
-        hsupport x hxnot
-      simpa [hx] using this
-    have hF_ind :
-        (s.indicator g =ᵐ[(volume : Measure E)] g) := by
-      filter_upwards [hF0] with x hx
-      by_cases hxmem : x ∈ s
-      · simp [g, hxmem]
-      · have : g x = 0 := hx hxmem
-        simp [g, hxmem, this]
-    -- Conclude `‖F‖ = ‖Fs‖` using `extendByZeroₗᵢ` and the indicator identity.
-    let Fext :
-        MeasureTheory.Lp ℝ (2 : ℝ≥0∞) (volume : Measure E) :=
-      (MeasureTheory.Lp.extendByZeroₗᵢ (μ := (volume : Measure E)) (E := ℝ) (p := (2 : ℝ≥0∞))
-        (s := s) hs) Fs
-    have hFext_ae :
-        ((Fext : MeasureTheory.Lp ℝ (2 : ℝ≥0∞) (volume : Measure E)) :
-            E → ℝ) =ᵐ[(volume : Measure E)]
-          s.indicator fun x : E => (Fs : E → ℝ) x := by
-      simpa [Fext] using
-        (MeasureTheory.Lp.extendByZeroₗᵢ_ae_eq
-          (μ := (volume : Measure E)) (p := (2 : ℝ≥0∞))
-          (s := s) hs Fs)
-    have hFs_on :
-        ∀ᵐ x ∂(volume : Measure E), x ∈ s → (Fs : E → ℝ) x = g x := by
-      -- rewrite the AE equality `Fs = g` on the restricted measure as an implication on `volume`
-      have := (MeasureTheory.ae_restrict_iff' (μ := (volume : Measure E)) (s := s) hs).1 hFs_ae
-      simpa [g] using this
-    have hindicator :
-        (s.indicator (fun x : E => (Fs : E → ℝ) x) =ᵐ[(volume : Measure E)] s.indicator g) := by
-      filter_upwards [hFs_on] with x hx
-      by_cases hxmem : x ∈ s
-      · simp [hxmem, hx hxmem]
-      · simp [hxmem]
-    have hFext_ae' :
-        (Fext : E → ℝ) =ᵐ[(volume : Measure E)] g := by
-      exact hFext_ae.trans (hindicator.trans hF_ind)
-    have hFext_eq : Fext = F := by
-      refine MeasureTheory.Lp.ext ?_
-      simpa [g, F] using hFext_ae'
-    have hnorm_F : ‖F‖ ≤ mS * ‖Bu - Bv‖ := by
-      -- use `‖F‖ = ‖Fs‖` via the isometry.
-      have hnorm_ext : ‖Fext‖ = ‖Fs‖ := by
-        simp [Fext]
-      -- `Fext = F` and `Fs` is bounded.
-      have : ‖Fext‖ ≤ mS * ‖Bu - Bv‖ := by
-        simpa [hnorm_ext] using hnorm_Fs
-      simpa [hFext_eq] using this
-    -- Convert to the `dist` statement.
-    simpa [Su, Sv, Bu, Bv, F, dist_eq_norm, mS, mul_assoc] using hnorm_F
+  have hdist_smoothL2_le :=
+    dist_smoothL2_le_mul_dist_smoothBCF (K := K) (ψ := ψ) hK hKm hψc hψcs
   have hTB_B : TotallyBounded B := by
     -- Use a finite `BCF` ε-net for `A` with centers in the image, then transfer to `L²`.
     rw [Metric.totallyBounded_iff]
     intro ε hε
     by_cases hmS0 : mS = 0
-    ·
-      let c : (E →₂[(volume : Measure E)] ℝ) :=
+    · let c : (E →₂[(volume : Measure E)] ℝ) :=
         smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs (0 : _)
       refine ⟨{c}, by simp [c], ?_⟩
       intro w hw
@@ -260,9 +281,15 @@ theorem smoothL2_image_closedBall_isCompact (hK : IsCompact K) (hKm : Measurable
       have hdist0 :
           dist (smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs u)
               c = 0 := by
+        have hmS0' :
+            (MeasureTheory.measureUnivNNReal ((volume : Measure E).restrict s) : ℝ) ^
+              ((2 : ℝ≥0∞).toReal⁻¹) = 0 := hmS0
         have :
             dist (smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs u) c ≤ 0 := by
-          simpa [c, hmS0] using hle
+          have hle' := hle
+          simp only [s] at hmS0'
+          rw [hmS0', zero_mul] at hle'
+          simpa [c] using hle'
         exact le_antisymm this dist_nonneg
       refine mem_iUnion.2 ?_
       refine ⟨c, mem_iUnion.2 ?_⟩
@@ -270,10 +297,10 @@ theorem smoothL2_image_closedBall_isCompact (hK : IsCompact K) (hKm : Measurable
       -- membership in the open ball follows from `dist = 0` and `ε > 0`
       simpa [Metric.mem_ball, hdist0] using hε
     · have hmSpos : 0 < mS := lt_of_le_of_ne hmS (Ne.symm hmS0)
-      let δ : ℝ := ε / mS
-      have hδpos : 0 < δ := div_pos hε hmSpos
+      let deltaLoss : ℝ := ε / mS
+      have hδpos : 0 < deltaLoss := div_pos hε hmSpos
       obtain ⟨t, htAsub, htFin, htCover⟩ :=
-        exists_finite_cover_balls_of_isCompact_closure (s := A) (ε := δ) hA_compact hδpos
+        exists_finite_cover_balls_of_isCompact_closure (s := A) (ε := deltaLoss) hA_compact hδpos
       let tFin : Finset (BoundedContinuousFunction (↥(Kψ (K := K) (ψ := ψ))) ℝ) :=
         htFin.toFinset
       have htFin_mem :
@@ -300,14 +327,14 @@ theorem smoothL2_image_closedBall_isCompact (hK : IsCompact K) (hKm : Measurable
       rcases hw with ⟨u, huU, rfl⟩
       have hBu : (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u) ∈ A := by
         exact ⟨u, huU, rfl⟩
-      have : smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u ∈ ⋃ x ∈ t, Metric.ball x δ :=
+      have : smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u ∈ ⋃ x ∈ t, Metric.ball x deltaLoss :=
         htCover hBu
       rcases mem_iUnion.1 this with ⟨f, hf⟩
       rcases mem_iUnion.1 hf with ⟨hf_t, hf_ball⟩
       have hf_tFin : f ∈ tFin := (htFin_mem (f := f)).2 hf_t
       let f' : ι := ⟨f, hf_tFin⟩
       have hf_ball' :
-          dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u) f < δ := hf_ball
+          dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u) f < deltaLoss := hf_ball
       have hdist :
           dist (smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs u)
               (smoothL2 (E := E) (K := K) ψ hK hKm hψc hψcs (uOf f')) < ε := by
@@ -317,17 +344,17 @@ theorem smoothL2_image_closedBall_isCompact (hK : IsCompact K) (hKm : Measurable
           simpa [f'] using huOfEq f'
         have hdist' :
             dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u)
-                (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs (uOf f')) < δ := by
+                (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs (uOf f')) < deltaLoss := by
           simpa [hf_eq] using hf_ball'
         have : mS * dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u)
                 (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs (uOf f')) < ε := by
           have : mS * dist (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs u)
-                  (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs (uOf f')) < mS * δ := by
+                  (smoothBCF (E := E) (K := K) (ψ := ψ) hK hKm hψc hψcs (uOf f')) < mS * deltaLoss := by
             exact mul_lt_mul_of_pos_left hdist' hmSpos
-          have hmul : mS * δ = ε := by
+          have hmul : mS * deltaLoss = ε := by
             have hmS_ne : mS ≠ 0 := ne_of_gt hmSpos
             calc
-              mS * δ = mS * (ε / mS) := by simp [δ]
+              mS * deltaLoss = mS * (ε / mS) := by simp [deltaLoss]
               _ = mS * ε / mS := (mul_div_assoc mS ε mS).symm
               _ = ε := by simpa using (mul_div_cancel_left₀ ε hmS_ne)
           simpa [hmul] using this
diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/TranslationIntegral.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/TranslationIntegral.lean
index cdb4346..6914c2a 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/TranslationIntegral.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/TranslationIntegral.lean
@@ -1,13 +1,13 @@
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Approximation
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.Translation
-import Mathlib.MeasureTheory.Integral.Bochner.Basic
-
 /-
 Copyright (c) 2026 Adam Benenson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Benenson
 -/
 
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Approximation
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.Translation
+import Mathlib.MeasureTheory.Integral.Bochner.Basic
+
 /-!
 # `L²` compactness criterion: bounding the translation-integral by a translation modulus
 
@@ -38,59 +38,60 @@ section Volume
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
 
-local instance instMeasurableSpaceE_L2CompactnessTranslationIntegral : MeasurableSpace E := borel E
-local instance instBorelSpaceE_L2CompactnessTranslationIntegral : BorelSpace E := ⟨rfl⟩
-local instance instOpensMeasurableSpaceE_L2CompactnessTranslationIntegral :
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceEL2CompactnessTranslationIntegral : MeasurableSpace E := borel E
+local instance instBorelSpaceEL2CompactnessTranslationIntegral : BorelSpace E := ⟨rfl⟩
+local instance instOpensMeasurableSpaceEL2CompactnessTranslationIntegral :
     OpensMeasurableSpace E := by infer_instance
-local instance instMeasurableAddE_L2CompactnessTranslationIntegral : MeasurableAdd E := by
+local instance instMeasurableAddEL2CompactnessTranslationIntegral : MeasurableAdd E := by
   infer_instance
-local instance instMeasurableNegE_L2CompactnessTranslationIntegral : MeasurableNeg E := by
+local instance instMeasurableNegEL2CompactnessTranslationIntegral : MeasurableNeg E := by
   infer_instance
 
 variable {ψ : E → ℝ}
 
-private lemma kernelMeasure_compl_ball_eq_zero_of_tsupport_subset {δ : ℝ}
-    (hψsupp : tsupport ψ ⊆ Metric.ball (0 : E) δ) :
-    kernelMeasure (E := E) ψ ((Metric.ball (0 : E) δ)ᶜ) = 0 := by
+private lemma kernelMeasure_compl_ball_eq_zero_of_tsupport_subset {deltaLoss : ℝ}
+    (hψsupp : tsupport ψ ⊆ Metric.ball (0 : E) deltaLoss) :
+    kernelMeasure (E := E) ψ ((Metric.ball (0 : E) deltaLoss)ᶜ) = 0 := by
   classical
-  have hψzero : ∀ x : E, x ∈ (Metric.ball (0 : E) δ)ᶜ → ψ x = 0 := by
+  have hψzero : ∀ x : E, x ∈ (Metric.ball (0 : E) deltaLoss)ᶜ → ψ x = 0 := by
     intro x hx
     have hx' : x ∉ tsupport ψ := by
       intro hx_ts
       exact hx (hψsupp hx_ts)
     exact image_eq_zero_of_notMem_tsupport (f := ψ) hx'
-  have hmeas : MeasurableSet ((Metric.ball (0 : E) δ)ᶜ) :=
-    (measurableSet_ball : MeasurableSet (Metric.ball (0 : E) δ)).compl
+  have hmeas : MeasurableSet ((Metric.ball (0 : E) deltaLoss)ᶜ) :=
+    (measurableSet_ball : MeasurableSet (Metric.ball (0 : E) deltaLoss)).compl
   have hEq :
-      Set.EqOn (fun x : E => ENNReal.ofReal (ψ x)) 0 ((Metric.ball (0 : E) δ)ᶜ) := by
+      Set.EqOn (fun x : E => ENNReal.ofReal (ψ x)) 0 ((Metric.ball (0 : E) deltaLoss)ᶜ) := by
     intro x hx
     simp [hψzero x hx]
   -- Expand `kernelMeasure` and note the density is identically `0` on the set.
   simp [kernelMeasure, MeasureTheory.withDensity_apply, hmeas,
     MeasureTheory.setLIntegral_eq_zero
       (μ := (volume : Measure E))
-      (s := (Metric.ball (0 : E) δ)ᶜ) hmeas hEq]
+      (s := (Metric.ball (0 : E) deltaLoss)ᶜ) hmeas hEq]
 
 theorem integral_norm_sq_translateL2_sub_le_sq_of_tsupport_subset_ball
     (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ) (hψ0 : ∀ x, 0 ≤ ψ x)
     (hψint : ∫ x, ψ x ∂(volume : Measure E) = 1)
-    {δ η : ℝ} (hη : 0 ≤ η) (hψsupp : tsupport ψ ⊆ Metric.ball (0 : E) δ)
+    {deltaLoss η : ℝ} (hη : 0 ≤ η) (hψsupp : tsupport ψ ⊆ Metric.ball (0 : E) deltaLoss)
     (F : (E →₂[(volume : Measure E)] ℝ))
     (hmod :
-      ∀ t : E, t ∈ Metric.ball (0 : E) δ →
+      ∀ t : E, t ∈ Metric.ball (0 : E) deltaLoss →
         ‖(translateL2 (μ := (volume : Measure E)) (-t)) F - F‖ ≤ η) :
     ∫ t,
         ‖(translateL2 (μ := (volume : Measure E)) (-t)) F - F‖ ^ 2
       ∂kernelMeasure (E := E) ψ ≤ η ^ 2 := by
   classical
   let μ : Measure E := kernelMeasure (E := E) ψ
-  haveI : MeasureTheory.IsProbabilityMeasure μ :=
+  have : MeasureTheory.IsProbabilityMeasure μ :=
     ⟨kernelMeasure_univ (E := E) (ψ := ψ) hψc hψcs hψ0 hψint⟩
-  have hμzero : μ ((Metric.ball (0 : E) δ)ᶜ) = 0 := by
+  have hμzero : μ ((Metric.ball (0 : E) deltaLoss)ᶜ) = 0 := by
     simpa [μ] using kernelMeasure_compl_ball_eq_zero_of_tsupport_subset (E := E) (ψ := ψ) hψsupp
-  have hAE_ball : (Metric.ball (0 : E) δ) ∈ MeasureTheory.ae μ :=
+  have hAE_ball : (Metric.ball (0 : E) deltaLoss) ∈ MeasureTheory.ae μ :=
     (MeasureTheory.mem_ae_iff.2 hμzero)
-  -- On `Metric.ball 0 δ`, the squared translation error is bounded by `η²`.
+  -- On `Metric.ball 0 deltaLoss`, the squared translation error is bounded by `η²`.
   have hAE_bound :
       ∀ᵐ t : E ∂μ,
         ‖‖(translateL2 (μ := (volume : Measure E)) (-t)) F - F‖ ^ 2‖ ≤ η ^ 2 := by
diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/Rellich.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/Rellich.lean
index 4cd9bb3..b133aa6 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/Rellich.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/Rellich.lean
@@ -1,19 +1,16 @@
-import Mathlib.Analysis.Normed.Operator.Compact
-import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
-import Mathlib.MeasureTheory.Function.LpSpace.Complete
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.TranslationEstimateH1
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.FrechetKolmogorov
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Kernels
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.TranslationIntegral
-
 /-
 Copyright (c) 2026 Adam Benenson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Benenson
 -/
 
-set_option linter.unusedTactic false
-set_option linter.unreachableTactic false
+import Mathlib.Analysis.Normed.Operator.Compact.Basic
+import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
+import Mathlib.MeasureTheory.Function.LpSpace.Complete
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.TranslationEstimateH1
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.FrechetKolmogorov
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Kernels
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.TranslationIntegral
 
 /-!
 # `RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.Rellich`
@@ -59,15 +56,16 @@ section Volume
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
   [CompleteSpace E]
 
-local instance instMeasurableSpaceE_SobolevEuclideanRellich : MeasurableSpace E := borel E
-local instance instBorelSpaceE_SobolevEuclideanRellich : BorelSpace E := ⟨rfl⟩
-local instance instOpensMeasurableSpaceE_SobolevEuclideanRellich : OpensMeasurableSpace E := by
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceRellich : MeasurableSpace E := borel E
+local instance instBorelSpaceRellich : BorelSpace E := ⟨rfl⟩
+local instance instOpensMeasurableSpaceRellich : OpensMeasurableSpace E := by
   infer_instance
-local instance instMeasurableAddE_SobolevEuclideanRellich : MeasurableAdd E := by
+local instance instMeasurableAddRellich : MeasurableAdd E := by
   infer_instance
-local instance instMeasurableNegE_SobolevEuclideanRellich : MeasurableNeg E := by
+local instance instMeasurableNegRellich : MeasurableNeg E := by
   infer_instance
-local instance instFactOneLeTwo_SobolevEuclideanRellich : Fact (1 ≤ (2 : ℝ≥0∞)) := ⟨by norm_num⟩
+local instance instFactOneLeTwoSobolevEuclideanRellich : Fact (1 ≤ (2 : ℝ≥0∞)) := ⟨by norm_num⟩
 
 /-! ### Supported `H¹` subspace -/
 
@@ -90,7 +88,6 @@ noncomputable def h1OnToL2 (K : Set E) (hKm : MeasurableSet K) :
 
 /-! ### Euclidean Rellich on fixed compact support -/
 
-set_option maxHeartbeats 2000000 in
 /-- Euclidean Rellich–Kondrachov compactness (Lebesgue): on a fixed compact support `K`, the
 inclusion `H¹ → L²` is a compact operator. -/
 theorem isCompactOperator_h1OnToL2 {K : Set E} (_hK : IsCompact K) (hKm : MeasurableSet K) :
@@ -105,10 +102,9 @@ theorem isCompactOperator_h1OnToL2 {K : Set E} (_hK : IsCompact K) (hKm : Measur
       L2Compactness.extendByZeroL2 (E := E) (K := K) hKm u ∈
         T '' Metric.closedBall (0 : ↥(h1On (E := E) K hKm)) 1}
   let C : ℝ :=
-    (h1ToL2 (μ := (volume : Measure E)) (E := E)).opNorm
+    ‖h1ToL2 (μ := (volume : Measure E)) (E := E)‖
   have hCnonneg : 0 ≤ C := by
-    dsimp [C]
-    exact (h1ToL2 (μ := (volume : Measure E)) (E := E)).opNorm_nonneg
+    exact norm_nonneg (h1ToL2 (μ := (volume : Measure E)) (E := E))
   have hA_ball :
       A ⊆
         Metric.closedBall
@@ -119,7 +115,7 @@ theorem isCompactOperator_h1OnToL2 {K : Set E} (_hK : IsCompact K) (hKm : Measur
     have hx' : ‖(x : H1vol)‖ ≤ (1 : ℝ) := by
       -- `h1On` inherits the ambient norm, so this is definitional.
       change ‖x‖ ≤ (1 : ℝ)
-      exact (mem_closedBall_zero_iff.mp hx)
+      simpa only [Metric.mem_closedBall,dist_zero_right x] using hx
     have hTx' : ‖T x‖ ≤ C := by
       have hTx : ‖T x‖ ≤ C * ‖(x : H1vol)‖ := by
         have h :=
@@ -150,20 +146,20 @@ theorem isCompactOperator_h1OnToL2 {K : Set E} (_hK : IsCompact K) (hKm : Measur
     have hδ : 0 < ε / 2 := by linarith
     rcases
         L2Compactness.exists_kernel_tsupport_subset_ball_integral_eq_one
-          (E := E) (δ := ε / 2) hδ with
+          (E := E) (deltaLoss := ε / 2) hδ with
       ⟨ψ, hψc, hψcs, hψ0, hψint, hψsupp⟩
     refine ⟨ψ, hψc, hψcs, hψ0, hψint, ?_⟩
     intro u huA
     rcases huA with ⟨x, hx, hxEq⟩
     have hxH1 : ‖(x : H1vol)‖ ≤ (1 : ℝ) := by
       change ‖x‖ ≤ (1 : ℝ)
-      exact (mem_closedBall_zero_iff.mp hx)
+      simpa only [Metric.mem_closedBall,dist_zero_right x] using hx
     have hmod :
         ∀ t : E, t ∈ Metric.ball (0 : E) (ε / 2) →
           ‖(translateL2 (μ := (volume : Measure E)) (-t)) (T x) - T x‖ ≤ ε / 2 := by
       intro t ht
       have ht' : ‖t‖ ≤ ε / 2 := le_of_lt (by
-        simpa [Metric.ball, dist_eq_norm, mem_setOf_eq] using ht)
+        simpa [Metric.ball, dist_eq_norm, mem_ofPred_eq] using ht)
       have hgrad_le :
           ‖h1ToL2Grad (μ := (volume : Measure E)) (E := E) (x : H1vol)‖ ≤ ‖(x : H1vol)‖ := by
         let V : Type _ := (E →₂[(volume : Measure E)] ℝ) × (E →₂[(volume : Measure E)] E)
@@ -192,7 +188,7 @@ theorem isCompactOperator_h1OnToL2 {K : Set E} (_hK : IsCompact K) (hKm : Measur
     have hη : 0 ≤ ε / 2 := le_of_lt hδ
     have hbound :=
       L2Compactness.integral_norm_sq_translateL2_sub_le_sq_of_tsupport_subset_ball
-        (E := E) (ψ := ψ) hψc hψcs hψ0 hψint (δ := ε / 2) (η := ε / 2) hη hψsupp (T x) hmod
+        (E := E) (ψ := ψ) hψc hψcs hψ0 hψint (deltaLoss := ε / 2) (η := ε / 2) hη hψsupp (T x) hmod
     simpa [hxEq] using hbound
   have hcomp : IsCompact (closure (T '' Metric.closedBall (0 : ↥(h1On (E := E) K hKm)) 1)) := by
     have hR : 0 ≤ C := hCnonneg
diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/Translation.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/Translation.lean
index c009eb8..f3b80d4 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/Translation.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/Translation.lean
@@ -1,15 +1,15 @@
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.H1
-import Mathlib.Analysis.Calculus.FDeriv.Add
-import Mathlib.MeasureTheory.Group.Measure
-import Mathlib.MeasureTheory.Function.LpSpace.Basic
-import Mathlib.Topology.Algebra.Group.Basic
-
 /-
 Copyright (c) 2026 Adam Benenson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Benenson
 -/
 
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.H1
+import Mathlib.Analysis.Calculus.FDeriv.Add
+import Mathlib.MeasureTheory.Group.Measure
+import Mathlib.MeasureTheory.Function.LpSpace.Basic
+import Mathlib.Topology.Algebra.Group.Basic
+
 /-!
 # `RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.Translation`
 
@@ -47,20 +47,21 @@ omit [CompleteSpace E] in
 lemma contDiff_translate {f : E → ℝ} (hf : ContDiff ℝ 1 f) (a : E) :
     ContDiff ℝ 1 (translate (E := E) a f) := by
   -- `x ↦ x + a` is `C^∞`; compose.
-  simpa [translate] using hf.comp (contDiff_id.add contDiff_const)
+  exact hf.comp (contDiff_id.add contDiff_const)
 
 omit [InnerProductSpace ℝ E] [CompleteSpace E] in
 lemma hasCompactSupport_translate {F : Type*} [Zero F] {f : E → F}
     (hf : HasCompactSupport f) (a : E) : HasCompactSupport (translate (E := E) a f) := by
-  simpa [translate] using hf.comp_homeomorph (Homeomorph.addRight a)
+  exact hf.comp_homeomorph (Homeomorph.addRight a)
 
 lemma grad_translate (a : E) (f : E → ℝ) (x : E) :
     grad (E := E) (translate (E := E) a f) x = grad (E := E) f (x + a) := by
   classical
   -- `fderiv` commutes with translation, hence so does `grad`.
-  simp [grad]
-  -- Reduce to the standard `fderiv` translation lemma.
-  simpa [translate] using (fderiv_comp_add_right (𝕜 := ℝ) (f := f) (x := x) a)
+  -- Reduce to the standard `fderiv` translation lemma, applied under the Riesz dual map.
+  have hfderiv : fderiv ℝ (translate (E := E) a f) x = fderiv ℝ f (x + a) :=
+    fderiv_comp_add_right (𝕜 := ℝ) (f := f) (x := x) a
+  simp only [grad, hfderiv]
 
 omit [CompleteSpace E] in
 lemma mem_C1c_translate {f : E → ℝ} (hf : f ∈ C1c (E := E)) (a : E) :
@@ -83,11 +84,12 @@ section Measure
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
 
-local instance instMeasurableSpaceE_SobolevEuclideanTranslation : MeasurableSpace E := borel E
-local instance instBorelSpaceE_SobolevEuclideanTranslation : BorelSpace E := ⟨rfl⟩
-local instance instOpensMeasurableSpaceE_SobolevEuclideanTranslation : OpensMeasurableSpace E := by
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceTranslation : MeasurableSpace E := borel E
+local instance instBorelSpaceTranslation : BorelSpace E := ⟨rfl⟩
+local instance instOpensMeasurableSpaceTranslation : OpensMeasurableSpace E := by
   infer_instance
-local instance instMeasurableAddE_SobolevEuclideanTranslation : MeasurableAdd E := by
+local instance instMeasurableAddTranslation : MeasurableAdd E := by
   infer_instance
 
 variable (μ : Measure E) [μ.IsAddRightInvariant]
@@ -106,7 +108,7 @@ lemma translateL2_ae_eq {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] (
     (translateL2 (μ := μ) (F := F) a g : E → F) =ᵐ[μ] fun x => (g : E → F) (x + a) := by
   classical
   -- Reduce to `Lp.coeFn_compMeasurePreserving`.
-  simpa [translateL2] using
+  exact
     (MeasureTheory.Lp.coeFn_compMeasurePreserving (g := (g : MeasureTheory.Lp F (2 : ENNReal) μ))
       (hf := MeasureTheory.measurePreserving_add_right μ a))
 
@@ -125,7 +127,7 @@ lemma translateL2_toL2 (a : E) (f : ↥(C1c (E := E))) :
     have hf' :
         (fun x => (toL2 (μ := μ) (E := E) f : E → ℝ) (x + a)) =ᵐ[μ] fun x => f.1 (x + a) := by
       -- Move the a.e. equality through a measure-preserving map.
-      simpa [Function.comp, Pi.add_apply] using
+      exact
         (Measure.QuasiMeasurePreserving.ae_eq_comp
           (MeasureTheory.measurePreserving_add_right μ a).quasiMeasurePreserving hf)
     exact (translateL2_ae_eq (μ := μ) (F := ℝ) a (toL2 (μ := μ) (E := E) f)).trans hf'
@@ -133,7 +135,7 @@ lemma translateL2_toL2 (a : E) (f : ↥(C1c (E := E))) :
       (toL2 (μ := μ) (E := E) (translateC1c (E := E) a f) : E → ℝ) =ᵐ[μ]
         fun x => f.1 (x + a) := by
     -- `toL2` agrees a.e. with the underlying translated function.
-    simpa [translateC1c, translate] using
+    exact
       (memLp_of_mem_C1c (μ := μ) (E := E) (translateC1c (E := E) a f).2).coeFn_toLp
   exact h₁.trans h₂.symm
 
@@ -150,7 +152,7 @@ lemma translateL2_toL2Grad (a : E) (f : ↥(C1c (E := E))) :
     have hf' :
         (fun x => (toL2Grad (μ := μ) (E := E) f : E → E) (x + a)) =ᵐ[μ]
           fun x => grad (E := E) f.1 (x + a) := by
-      simpa [Function.comp, Pi.add_apply] using
+      exact
         (Measure.QuasiMeasurePreserving.ae_eq_comp
           (MeasureTheory.measurePreserving_add_right μ a).quasiMeasurePreserving hf)
     exact
diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimate.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimate.lean
index fcec373..7556a69 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimate.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimate.lean
@@ -1,15 +1,15 @@
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.H1
-import Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
-import Mathlib.Analysis.Calculus.Deriv.Comp
-import Mathlib.Analysis.Calculus.Deriv.Mul
-import Mathlib.Analysis.Calculus.Deriv.Add
-
 /-
 Copyright (c) 2026 Adam Benenson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Benenson
 -/
 
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.H1
+import Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
+import Mathlib.Analysis.Calculus.Deriv.Comp
+import Mathlib.Analysis.Calculus.Deriv.Mul
+import Mathlib.Analysis.Calculus.Deriv.Add
+
 /-!
 # `RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.TranslationEstimate`
 
@@ -35,11 +35,12 @@ section
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
 
-local instance instMeasurableSpaceE_SobolevEuclideanTranslationEstimate :
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceTranslationEstimate :
     MeasurableSpace E := borel E
-local instance instBorelSpaceE_SobolevEuclideanTranslationEstimate :
+local instance instBorelSpaceTranslationEstimate :
     BorelSpace E := ⟨rfl⟩
-local instance instOpensMeasurableSpaceE_SobolevEuclideanTranslationEstimate :
+local instance instOpensMeasurableSpaceTranslationEstimate :
     OpensMeasurableSpace E := by
   infer_instance
 
@@ -85,10 +86,11 @@ lemma enorm_fderiv_apply_le_enorm_grad_mul (f : E → ℝ) (x a : E) :
   -- Use the operator norm bound, then identify `‖fderiv‖` with `‖grad‖` via the Riesz isometry.
   have h₁ :
       ‖fderiv ℝ f x a‖ₑ ≤ ‖fderiv ℝ f x‖ₑ * ‖a‖ₑ :=
-    (ContinuousLinearMap.le_opNorm_enorm (f := fderiv ℝ f x) a)
+    (ContinuousLinearMap.le_opENorm (f := fderiv ℝ f x) a)
   have h₂ : ‖grad (E := E) f x‖ₑ = ‖fderiv ℝ f x‖ₑ := by
     -- `grad f x = (toDual).symm (fderiv f x)` and `toDual.symm` is an isometry.
-    simpa [grad] using
+    simp only [grad]
+    exact
       (LinearIsometry.enorm_map
         (f := (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry)
         (fderiv ℝ f x))
@@ -108,10 +110,10 @@ lemma enorm_deriv_comp_line_le (x a : E) {f : E → ℝ} (hf : ContDiff ℝ 1 f)
 
 lemma enorm_sub_le_enorm_mul_lintegral_grad (x a : E) {f : E → ℝ} (hf : ContDiff ℝ 1 f) :
     ‖f (x + a) - f x‖ₑ ≤
-      ‖a‖ₑ * ∫⁻ t in Icc (0 : ℝ) 1, ‖grad (E := E) f (x + t • a)‖ₑ := by
+      ‖a‖ₑ * ∫⁻ t in Set.Icc (0 : ℝ) 1, ‖grad (E := E) f (x + t • a)‖ₑ := by
   -- Apply FTC along the segment `t ↦ x + t • a`, then bound the derivative pointwise.
   have hCont :
-      ContDiffOn ℝ 1 (fun t : ℝ => f (x + t • a)) (Icc (0 : ℝ) 1) := by
+      ContDiffOn ℝ 1 (fun t : ℝ => f (x + t • a)) (Set.Icc (0 : ℝ) 1) := by
     -- `t ↦ x + t • a` is `C^∞`; compose with `f`.
     have hInner : ContDiff ℝ ⊤ (fun t : ℝ => x + t • a) := by
       simpa [line] using
@@ -119,14 +121,14 @@ lemma enorm_sub_le_enorm_mul_lintegral_grad (x a : E) {f : E → ℝ} (hf : Cont
     have hInner' : ContDiff ℝ 1 (fun t : ℝ => x + t • a) := hInner.of_le (by simp)
     exact (hf.comp hInner').contDiffOn
   have hFTC :
-      ‖f (x + a) - f x‖ₑ ≤ ∫⁻ t in Icc (0 : ℝ) 1, ‖deriv (fun t : ℝ => f (x + t • a)) t‖ₑ := by
+      ‖f (x + a) - f x‖ₑ ≤ ∫⁻ t in Set.Icc (0 : ℝ) 1, ‖deriv (fun t : ℝ => f (x + t • a)) t‖ₑ := by
     simpa using
       (enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc (f := fun t : ℝ => f (x + t • a))
         (a := (0 : ℝ)) (b := 1) hCont (by exact zero_le_one))
   refine hFTC.trans ?_
   have hDerivBound :
       (fun t : ℝ => ‖deriv (fun t : ℝ => f (x + t • a)) t‖ₑ)
-        ≤ᵐ[Measure.restrict volume (Icc (0 : ℝ) 1)]
+        ≤ᵐ[Measure.restrict volume (Set.Icc (0 : ℝ) 1)]
           fun t : ℝ => ‖a‖ₑ * ‖grad (E := E) f (x + t • a)‖ₑ := by
     -- Pointwise bound holds everywhere.
     refine (ae_of_all _ fun t => ?_)
@@ -135,8 +137,8 @@ lemma enorm_sub_le_enorm_mul_lintegral_grad (x a : E) {f : E → ℝ} (hf : Cont
       (enorm_deriv_comp_line_le (x := x) (a := a) (f := f) hf (t := t))
   -- Pull out the constant `‖a‖ₑ`.
   have :
-      (∫⁻ t in Icc (0 : ℝ) 1, ‖deriv (fun t : ℝ => f (x + t • a)) t‖ₑ) ≤
-        ∫⁻ t in Icc (0 : ℝ) 1, ‖a‖ₑ * ‖grad (E := E) f (x + t • a)‖ₑ := by
+      (∫⁻ t in Set.Icc (0 : ℝ) 1, ‖deriv (fun t : ℝ => f (x + t • a)) t‖ₑ) ≤
+        ∫⁻ t in Set.Icc (0 : ℝ) 1, ‖a‖ₑ * ‖grad (E := E) f (x + t • a)‖ₑ := by
     exact lintegral_mono_ae hDerivBound
   refine this.trans ?_
   -- Pull out the constant factor.
@@ -151,10 +153,10 @@ lemma enorm_sub_le_enorm_mul_lintegral_grad (x a : E) {f : E → ℝ} (hf : Cont
       have : Continuous (fun t : ℝ => x + t • a) := by
         fun_prop
       exact this)).measurable.enorm
-  -- Now finish: `∫⁻ t in Icc, ‖a‖ * g t = ‖a‖ * ∫⁻ t in Icc, g t`.
+  -- Now finish: `∫⁻ t in Set.Icc, ‖a‖ * g t = ‖a‖ * ∫⁻ t in Set.Icc, g t`.
   exact le_of_eq <| by
     simpa [mul_assoc] using
-      (MeasureTheory.lintegral_const_mul (μ := volume.restrict (Icc (0 : ℝ) 1)) (r := ‖a‖ₑ)
+      (MeasureTheory.lintegral_const_mul (μ := volume.restrict (Set.Icc (0 : ℝ) 1)) (r := ‖a‖ₑ)
         (f := fun t : ℝ => ‖grad (E := E) f (x + t • a)‖ₑ) hMeas)
 
 end
diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimateH1.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimateH1.lean
index 6bac2f7..4e7144c 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimateH1.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimateH1.lean
@@ -1,12 +1,12 @@
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.TranslationEstimateL2
-import Mathlib.Topology.Order.OrderClosed
-
 /-
 Copyright (c) 2026 Adam Benenson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Benenson
 -/
 
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.TranslationEstimateL2
+import Mathlib.Topology.Order.OrderClosed
+
 /-!
 # `RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.TranslationEstimateH1`
 
@@ -33,14 +33,15 @@ section
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
 
-local instance instMeasurableSpaceE_SobolevEuclideanTranslationEstimateH1 :
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceTranslationEstimateH1 :
     MeasurableSpace E := borel E
-local instance instBorelSpaceE_SobolevEuclideanTranslationEstimateH1 :
+local instance instBorelSpaceTranslationEstimateH1 :
     BorelSpace E := ⟨rfl⟩
-local instance instOpensMeasurableSpaceE_SobolevEuclideanTranslationEstimateH1 :
+local instance instOpensMeasurableSpaceTranslationEstimateH1 :
     OpensMeasurableSpace E := by
   infer_instance
-local instance instMeasurableAddE_SobolevEuclideanTranslationEstimateH1 : MeasurableAdd E := by
+local instance instMeasurableAddTranslationEstimateH1 : MeasurableAdd E := by
   infer_instance
 
 variable (μ : Measure E) [μ.IsAddRightInvariant] [IsFiniteMeasureOnCompacts μ] [SFinite μ]
@@ -73,14 +74,14 @@ theorem norm_translateL2_sub_h1ToL2_le (a : E) (u : ↥(h1 (μ := μ) (E := E)))
       have hsub :
           Continuous fun v : V =>
             translateL2 (μ := μ) (F := ℝ) a v.1 - v.1 := by
-        simpa [sub_eq_add_neg] using htr.sub hfst
-      simpa using (continuous_norm.comp hsub)
+        exact htr.sub hfst
+      exact (continuous_norm.comp hsub)
     have hg :
         Continuous fun v : V =>
           ‖a‖ * ‖v.2‖ := by
       have hsnd : Continuous fun v : V => v.2 := continuous_snd
       have hnorm : Continuous fun v : V => ‖v.2‖ := continuous_norm.comp hsnd
-      simpa [mul_assoc] using (continuous_const.mul hnorm)
+      exact (continuous_const.mul hnorm)
     exact isClosed_le hf hg
   have hRange : (LinearMap.range (graph (μ := μ) (E := E)) : Set V) ⊆ S := by
     rintro v ⟨f, rfl⟩
diff --git a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimateL2.lean b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimateL2.lean
index 9a903af..0264ad8 100644
--- a/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimateL2.lean
+++ b/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimateL2.lean
@@ -1,14 +1,14 @@
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.Translation
-import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.TranslationEstimate
-import Mathlib.MeasureTheory.Integral.MeanInequalities
-import Mathlib.MeasureTheory.Measure.Prod
-
 /-
 Copyright (c) 2026 Adam Benenson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Benenson
 -/
 
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.Translation
+import RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.TranslationEstimate
+import Mathlib.MeasureTheory.Integral.MeanInequalities
+import Mathlib.MeasureTheory.Measure.Prod
+
 /-!
 # `RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.TranslationEstimateL2`
 
@@ -40,19 +40,20 @@ section
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
 
-local instance instMeasurableSpaceE_SobolevEuclideanTranslationEstimateL2 :
+/-- Borel σ-algebra on the model space `E`. -/
+local instance instMeasurableSpaceTranslationEstimateL2 :
     MeasurableSpace E := borel E
-local instance instBorelSpaceE_SobolevEuclideanTranslationEstimateL2 :
+local instance instBorelSpaceTranslationEstimateL2 :
     BorelSpace E := ⟨rfl⟩
-local instance instOpensMeasurableSpaceE_SobolevEuclideanTranslationEstimateL2 :
+local instance instOpensMeasurableSpaceTranslationEstimateL2 :
     OpensMeasurableSpace E := by
   infer_instance
-local instance instMeasurableAddE_SobolevEuclideanTranslationEstimateL2 : MeasurableAdd E := by
+local instance instMeasurableAddTranslationEstimateL2 : MeasurableAdd E := by
   infer_instance
 
 variable (μ : Measure E) [μ.IsAddRightInvariant] [IsFiniteMeasureOnCompacts μ] [SFinite μ]
 
-private abbrev μI : Measure ℝ := (volume.restrict (Icc (0 : ℝ) 1))
+private abbrev μI : Measure ℝ := (volume.restrict (Set.Icc (0 : ℝ) 1))
 
 private lemma μI_univ : (μI : Measure ℝ) Set.univ = (1 : ℝ≥0∞) := by
   simp [μI, Measure.restrict_apply, Real.volume_Icc]
@@ -92,7 +93,143 @@ private lemma lintegral_rpow_two_le_lintegral_rpow_two
         (∫⁻ t, g t ^ (2 : ℝ) ∂(μI : Measure ℝ))
         (1 / (2 : ℝ)) (2 : ℝ)).symm))
 
+omit [IsFiniteMeasureOnCompacts μ] in
 /-- `L²` translation estimate for `C¹_c` functions under a right-invariant measure. -/
+private lemma lintegral_enorm_sub_sq_le (a : E) (f : ↥(C1c (E := E))) :
+    (∫⁻ x, ‖f.1 (x + a) - f.1 x‖ₑ ^ (2 : ℝ) ∂μ) ≤
+      ‖a‖ₑ ^ (2 : ℝ) * (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) := by
+  -- Pointwise: Cauchy–Schwarz in `t`, then Tonelli in `(x,t)`.
+  have hpt :
+      ∀ x : E,
+        ‖f.1 (x + a) - f.1 x‖ₑ ^ (2 : ℝ) ≤
+          ‖a‖ₑ ^ (2 : ℝ) *
+            ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ) := by
+    intro x
+    have h0 := enorm_sub_le_enorm_mul_lintegral_grad (E := E) (x := x) (a := a) (f := f.1)
+      (hf := f.2.1)
+    -- Square both sides and apply Cauchy–Schwarz in `t`.
+    have h1 :
+        ‖f.1 (x + a) - f.1 x‖ₑ ^ (2 : ℝ) ≤
+          (‖a‖ₑ * ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ∂(μI : Measure ℝ)) ^ (2 : ℝ) := by
+      exact ENNReal.rpow_le_rpow h0 (by norm_num)
+    have hcs :
+        (∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ∂(μI : Measure ℝ)) ^ (2 : ℝ) ≤
+          ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ) := by
+      refine lintegral_rpow_two_le_lintegral_rpow_two (g := fun t : ℝ =>
+        ‖grad (E := E) f.1 (x + t • a)‖ₑ) ?_
+      -- measurability from continuity of `grad`.
+      have hgrad : Continuous (grad (E := E) f.1) := continuous_grad (E := E) (f := f.1) f.2.1
+      have hline : Continuous fun t : ℝ => x + t • a := by
+        fun_prop
+      exact (hgrad.comp hline).measurable.enorm.aemeasurable
+    -- Combine and rewrite.
+    calc
+      ‖f.1 (x + a) - f.1 x‖ₑ ^ (2 : ℝ)
+          ≤ (‖a‖ₑ * ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ∂(μI : Measure ℝ)) ^ (2 : ℝ) := h1
+      _ = ‖a‖ₑ ^ (2 : ℝ) *
+          (∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ
+            ∂(μI : Measure ℝ)) ^ (2 : ℝ) := by
+          simpa using
+            (ENNReal.mul_rpow_of_nonneg ‖a‖ₑ
+              (∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ
+                ∂(μI : Measure ℝ))
+              (show (0 : ℝ) ≤ (2 : ℝ) by norm_num))
+      _ ≤ ‖a‖ₑ ^ (2 : ℝ) *
+          ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ)
+            ∂(μI : Measure ℝ) := by
+          gcongr
+      _ = ‖a‖ₑ ^ (2 : ℝ) *
+          ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ)
+            ∂(μI : Measure ℝ) := rfl
+  -- Integrate over `x` and apply Tonelli to swap integrals.
+  let F : E × ℝ → ℝ≥0∞ :=
+    fun z => ‖grad (E := E) f.1 (z.1 + z.2 • a)‖ₑ ^ (2 : ℝ)
+  have hmeas :
+      AEMeasurable
+        F (μ.prod (μI : Measure ℝ)) := by
+    have hgrad : Continuous (grad (E := E) f.1) := continuous_grad (E := E) (f := f.1) f.2.1
+    have hcont : Continuous fun z : E × ℝ => z.1 + z.2 • a := by
+      fun_prop
+    have hbase : Measurable fun z : E × ℝ => ‖grad (E := E) f.1 (z.1 + z.2 • a)‖ₑ := by
+      exact (hgrad.comp hcont).measurable.enorm
+    have hpow : Measurable fun r : ℝ≥0∞ => r ^ (2 : ℝ) :=
+      (ENNReal.continuous_rpow_const (y := (2 : ℝ))).measurable
+    exact (hpow.comp hbase).aemeasurable
+  have hTonelli :
+      (∫⁻ x, ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ) ∂μ) =
+        ∫⁻ t, ∫⁻ x, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂μ ∂(μI : Measure ℝ) := by
+    -- Tonelli in both orders, via the product measure.
+    have hprod :
+        (∫⁻ z, F z ∂μ.prod (μI : Measure ℝ)) =
+          ∫⁻ x, ∫⁻ t, F (x, t) ∂(μI : Measure ℝ) ∂μ :=
+      MeasureTheory.lintegral_prod (μ := μ) (ν := (μI : Measure ℝ)) F hmeas
+    have hprod_symm :
+        (∫⁻ z, F z ∂μ.prod (μI : Measure ℝ)) =
+          ∫⁻ t, ∫⁻ x, F (x, t) ∂μ ∂(μI : Measure ℝ) :=
+      MeasureTheory.lintegral_prod_symm (μ := μ) (ν := (μI : Measure ℝ)) F hmeas
+    calc
+      (∫⁻ x, ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ) ∂μ)
+          = ∫⁻ z, F z ∂μ.prod (μI : Measure ℝ) := by
+              simpa [F] using hprod.symm
+      _ = ∫⁻ t, ∫⁻ x, F (x, t) ∂μ ∂(μI : Measure ℝ) := hprod_symm
+      _ = ∫⁻ t, ∫⁻ x, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂μ ∂(μI : Measure ℝ) := by
+              simp [F]
+  -- Now use measure-preserving translation in `x` and evaluate the `t`-integral.
+  have hShift :
+      (∫⁻ t, ∫⁻ x, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂μ ∂(μI : Measure ℝ)) =
+        ∫⁻ t, (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) ∂(μI : Measure ℝ) := by
+    refine MeasureTheory.lintegral_congr fun t => ?_
+    -- Change of variables `x ↦ x + t•a`.
+    have hmeas' : Measurable fun x : E => ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) := by
+      have hgrad : Continuous (grad (E := E) f.1) := continuous_grad (E := E) (f := f.1) f.2.1
+      have hbase : Measurable fun x : E => ‖grad (E := E) f.1 x‖ₑ := hgrad.measurable.enorm
+      have hpow : Measurable fun r : ℝ≥0∞ => r ^ (2 : ℝ) :=
+        (ENNReal.continuous_rpow_const (y := (2 : ℝ))).measurable
+      exact hpow.comp hbase
+    simpa [Function.comp, add_assoc] using
+      (MeasureTheory.measurePreserving_add_right μ (t • a)).lintegral_comp (μ := μ) (ν := μ)
+        (f := fun x : E => ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ)) hmeas'
+  have hEval :
+      (∫⁻ t, (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) ∂(μI : Measure ℝ)) =
+        (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) := by
+    -- `μI` has total mass `1`.
+    simp [μI, Measure.restrict_apply, Real.volume_Icc]
+  -- Put everything together.
+  have hInt :
+      (∫⁻ x, ‖f.1 (x + a) - f.1 x‖ₑ ^ (2 : ℝ) ∂μ) ≤
+        ‖a‖ₑ ^ (2 : ℝ) * (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) := by
+    calc
+      (∫⁻ x, ‖f.1 (x + a) - f.1 x‖ₑ ^ (2 : ℝ) ∂μ)
+          ≤ ∫⁻ x, ‖a‖ₑ ^ (2 : ℝ) *
+                ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ) ∂μ := by
+            refine MeasureTheory.lintegral_mono ?_
+            intro x
+            exact hpt x
+      _ = ‖a‖ₑ ^ (2 : ℝ) *
+            (∫⁻ x, ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ) ∂μ) := by
+            -- Pull out the constant using `lintegral_const_mul''`.
+            have hInner :
+                AEMeasurable
+                  (fun x : E =>
+                    ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ)) μ := by
+              -- Measurability of the inner integral follows
+              -- from `hmeas` via
+              -- `AEMeasurable.lintegral_prod_right'`.
+              simpa [F] using (hmeas.lintegral_prod_right' (μ := μ) (ν := (μI : Measure ℝ)))
+            simpa [mul_assoc] using
+              (MeasureTheory.lintegral_const_mul'' (μ := μ) (r := ‖a‖ₑ ^ (2 : ℝ))
+                (f := fun x : E =>
+                  ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ)) hInner)
+      _ = ‖a‖ₑ ^ (2 : ℝ) *
+            (∫⁻ t, ∫⁻ x, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂μ ∂(μI : Measure ℝ)) := by
+            exact congrArg (fun z => ‖a‖ₑ ^ (2 : ℝ) * z) hTonelli
+      _ = ‖a‖ₑ ^ (2 : ℝ) *
+            (∫⁻ t, (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) ∂(μI : Measure ℝ)) := by
+            exact congrArg (fun z => ‖a‖ₑ ^ (2 : ℝ) * z) hShift
+      _ = ‖a‖ₑ ^ (2 : ℝ) * (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) := by
+            exact congrArg (fun z => ‖a‖ₑ ^ (2 : ℝ) * z) hEval
+  exact hInt
+
 lemma enorm_translateL2_sub_toL2_le (a : E) (f : ↥(C1c (E := E))) :
     ‖translateL2 (μ := μ) (F := ℝ) a (toL2 (μ := μ) (E := E) f) -
         toL2 (μ := μ) (E := E) f‖ₑ ≤
@@ -112,7 +249,7 @@ lemma enorm_translateL2_sub_toL2_le (a : E) (f : ↥(C1c (E := E))) :
         (memLp_of_mem_C1c (μ := μ) (E := E) f.2).coeFn_toLp
       have hf' :
           (fun x => (toL2 (μ := μ) (E := E) f : E → ℝ) (x + a)) =ᵐ[μ] fun x => f.1 (x + a) := by
-        simpa [Function.comp, Pi.add_apply] using
+        exact
           (Measure.QuasiMeasurePreserving.ae_eq_comp
             (MeasureTheory.measurePreserving_add_right μ a).quasiMeasurePreserving hf)
       exact (translateL2_ae_eq (μ := μ) (F := ℝ) a (toL2 (μ := μ) (E := E) f)).trans hf'
@@ -159,144 +296,23 @@ lemma enorm_translateL2_sub_toL2_le (a : E) (f : ↥(C1c (E := E))) :
         ‖a‖ₑ * MeasureTheory.eLpNorm (fun x : E => grad (E := E) f.1 x) (2 : ℝ≥0∞) μ := by
     -- Expand the definition of `eLpNorm` at exponent `2`.
     have h2_ne0 : (2 : ℝ≥0∞) ≠ 0 := by simp
-    have h2_netop : (2 : ℝ≥0∞) ≠ ∞ := by simp
-    simp_rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
-      h2_ne0 h2_netop, ENNReal.toReal_ofNat] at *
+    have h2_netop : (2 : ℝ≥0∞) ≠ (⊤ : ℝ≥0∞) := by simp
+    have hf_meas : MeasureTheory.AEStronglyMeasurable (fun x : E => f.1 x) μ :=
+      (memLp_of_mem_C1c (μ := μ) (E := E) f.2).aestronglyMeasurable
+    have hshift_meas :
+        MeasureTheory.AEStronglyMeasurable (fun x : E => f.1 (x + a) - f.1 x) μ := by
+      have hshift : MeasureTheory.AEStronglyMeasurable (fun x : E => f.1 (x + a)) μ :=
+        hf_meas.comp_quasiMeasurePreserving
+          (MeasureTheory.measurePreserving_add_right μ a).quasiMeasurePreserving
+      exact hshift.sub hf_meas
+    have hgrad_meas :
+        MeasureTheory.AEStronglyMeasurable (fun x : E => grad (E := E) f.1 x) μ :=
+      (memLp_grad_of_mem_C1c (μ := μ) (E := E) f.2).aestronglyMeasurable
+    rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal h2_ne0 h2_netop hshift_meas,
+      MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal h2_ne0 h2_netop hgrad_meas,
+      ENNReal.toReal_ofNat]
     -- It suffices to compare the squared integrals.
-    have hsq :
-        (∫⁻ x, ‖f.1 (x + a) - f.1 x‖ₑ ^ (2 : ℝ) ∂μ) ≤
-          ‖a‖ₑ ^ (2 : ℝ) * (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) := by
-      -- Pointwise: Cauchy–Schwarz in `t`, then Tonelli in `(x,t)`.
-      have hpt :
-          ∀ x : E,
-            ‖f.1 (x + a) - f.1 x‖ₑ ^ (2 : ℝ) ≤
-              ‖a‖ₑ ^ (2 : ℝ) *
-                ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ) := by
-        intro x
-        have h0 := enorm_sub_le_enorm_mul_lintegral_grad (E := E) (x := x) (a := a) (f := f.1)
-          (hf := f.2.1)
-        -- Square both sides and apply Cauchy–Schwarz in `t`.
-        have h1 :
-            ‖f.1 (x + a) - f.1 x‖ₑ ^ (2 : ℝ) ≤
-              (‖a‖ₑ * ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ∂(μI : Measure ℝ)) ^ (2 : ℝ) := by
-          exact ENNReal.rpow_le_rpow h0 (by norm_num)
-        have hcs :
-            (∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ∂(μI : Measure ℝ)) ^ (2 : ℝ) ≤
-              ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ) := by
-          refine lintegral_rpow_two_le_lintegral_rpow_two (g := fun t : ℝ =>
-            ‖grad (E := E) f.1 (x + t • a)‖ₑ) ?_
-          -- measurability from continuity of `grad`.
-          have hgrad : Continuous (grad (E := E) f.1) := continuous_grad (E := E) (f := f.1) f.2.1
-          have hline : Continuous fun t : ℝ => x + t • a := by
-            fun_prop
-          exact (hgrad.comp hline).measurable.enorm.aemeasurable
-        -- Combine and rewrite.
-        calc
-          ‖f.1 (x + a) - f.1 x‖ₑ ^ (2 : ℝ)
-              ≤ (‖a‖ₑ * ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ∂(μI : Measure ℝ)) ^ (2 : ℝ) := h1
-          _ = ‖a‖ₑ ^ (2 : ℝ) *
-              (∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ
-                ∂(μI : Measure ℝ)) ^ (2 : ℝ) := by
-              simpa using
-                (ENNReal.mul_rpow_of_nonneg ‖a‖ₑ
-                  (∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ
-                    ∂(μI : Measure ℝ))
-                  (show (0 : ℝ) ≤ (2 : ℝ) by norm_num))
-          _ ≤ ‖a‖ₑ ^ (2 : ℝ) *
-              ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ)
-                ∂(μI : Measure ℝ) := by
-              gcongr
-          _ = ‖a‖ₑ ^ (2 : ℝ) *
-              ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ)
-                ∂(μI : Measure ℝ) := rfl
-      -- Integrate over `x` and apply Tonelli to swap integrals.
-      let F : E × ℝ → ℝ≥0∞ :=
-        fun z => ‖grad (E := E) f.1 (z.1 + z.2 • a)‖ₑ ^ (2 : ℝ)
-      have hmeas :
-          AEMeasurable
-            F (μ.prod (μI : Measure ℝ)) := by
-        have hgrad : Continuous (grad (E := E) f.1) := continuous_grad (E := E) (f := f.1) f.2.1
-        have hcont : Continuous fun z : E × ℝ => z.1 + z.2 • a := by
-          fun_prop
-        have hbase : Measurable fun z : E × ℝ => ‖grad (E := E) f.1 (z.1 + z.2 • a)‖ₑ := by
-          exact (hgrad.comp hcont).measurable.enorm
-        have hpow : Measurable fun r : ℝ≥0∞ => r ^ (2 : ℝ) :=
-          (ENNReal.continuous_rpow_const (y := (2 : ℝ))).measurable
-        simpa [F] using (hpow.comp hbase).aemeasurable
-      have hTonelli :
-          (∫⁻ x, ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ) ∂μ) =
-            ∫⁻ t, ∫⁻ x, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂μ ∂(μI : Measure ℝ) := by
-        -- Tonelli in both orders, via the product measure.
-        have hprod :
-            (∫⁻ z, F z ∂μ.prod (μI : Measure ℝ)) =
-              ∫⁻ x, ∫⁻ t, F (x, t) ∂(μI : Measure ℝ) ∂μ :=
-          MeasureTheory.lintegral_prod (μ := μ) (ν := (μI : Measure ℝ)) F hmeas
-        have hprod_symm :
-            (∫⁻ z, F z ∂μ.prod (μI : Measure ℝ)) =
-              ∫⁻ t, ∫⁻ x, F (x, t) ∂μ ∂(μI : Measure ℝ) :=
-          MeasureTheory.lintegral_prod_symm (μ := μ) (ν := (μI : Measure ℝ)) F hmeas
-        calc
-          (∫⁻ x, ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ) ∂μ)
-              = ∫⁻ z, F z ∂μ.prod (μI : Measure ℝ) := by
-                  simpa [F] using hprod.symm
-          _ = ∫⁻ t, ∫⁻ x, F (x, t) ∂μ ∂(μI : Measure ℝ) := hprod_symm
-          _ = ∫⁻ t, ∫⁻ x, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂μ ∂(μI : Measure ℝ) := by
-                  simp [F]
-      -- Now use measure-preserving translation in `x` and evaluate the `t`-integral.
-      have hShift :
-          (∫⁻ t, ∫⁻ x, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂μ ∂(μI : Measure ℝ)) =
-            ∫⁻ t, (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) ∂(μI : Measure ℝ) := by
-        refine MeasureTheory.lintegral_congr fun t => ?_
-        -- Change of variables `x ↦ x + t•a`.
-        have hmeas' : Measurable fun x : E => ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) := by
-          have hgrad : Continuous (grad (E := E) f.1) := continuous_grad (E := E) (f := f.1) f.2.1
-          have hbase : Measurable fun x : E => ‖grad (E := E) f.1 x‖ₑ := hgrad.measurable.enorm
-          have hpow : Measurable fun r : ℝ≥0∞ => r ^ (2 : ℝ) :=
-            (ENNReal.continuous_rpow_const (y := (2 : ℝ))).measurable
-          exact hpow.comp hbase
-        simpa [Function.comp, add_assoc] using
-          (MeasureTheory.measurePreserving_add_right μ (t • a)).lintegral_comp (μ := μ) (ν := μ)
-            (f := fun x : E => ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ)) hmeas'
-      have hEval :
-          (∫⁻ t, (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) ∂(μI : Measure ℝ)) =
-            (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) := by
-        -- `μI` has total mass `1`.
-        simp [μI, Measure.restrict_apply, Real.volume_Icc]
-      -- Put everything together.
-      have hInt :
-          (∫⁻ x, ‖f.1 (x + a) - f.1 x‖ₑ ^ (2 : ℝ) ∂μ) ≤
-            ‖a‖ₑ ^ (2 : ℝ) * (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) := by
-        calc
-          (∫⁻ x, ‖f.1 (x + a) - f.1 x‖ₑ ^ (2 : ℝ) ∂μ)
-              ≤ ∫⁻ x, ‖a‖ₑ ^ (2 : ℝ) *
-                    ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ) ∂μ := by
-                refine MeasureTheory.lintegral_mono ?_
-                intro x
-                exact hpt x
-          _ = ‖a‖ₑ ^ (2 : ℝ) *
-                (∫⁻ x, ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ) ∂μ) := by
-                -- Pull out the constant using `lintegral_const_mul''`.
-                have hInner :
-                    AEMeasurable
-                      (fun x : E =>
-                        ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ)) μ := by
-                  -- Measurability of the inner integral follows
-                  -- from `hmeas` via
-                  -- `AEMeasurable.lintegral_prod_right'`.
-                  simpa [F] using (hmeas.lintegral_prod_right' (μ := μ) (ν := (μI : Measure ℝ)))
-                simpa [mul_assoc] using
-                  (MeasureTheory.lintegral_const_mul'' (μ := μ) (r := ‖a‖ₑ ^ (2 : ℝ))
-                    (f := fun x : E =>
-                      ∫⁻ t, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂(μI : Measure ℝ)) hInner)
-          _ = ‖a‖ₑ ^ (2 : ℝ) *
-                (∫⁻ t, ∫⁻ x, ‖grad (E := E) f.1 (x + t • a)‖ₑ ^ (2 : ℝ) ∂μ ∂(μI : Measure ℝ)) := by
-                exact congrArg (fun z => ‖a‖ₑ ^ (2 : ℝ) * z) hTonelli
-          _ = ‖a‖ₑ ^ (2 : ℝ) *
-                (∫⁻ t, (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) ∂(μI : Measure ℝ)) := by
-                exact congrArg (fun z => ‖a‖ₑ ^ (2 : ℝ) * z) hShift
-          _ = ‖a‖ₑ ^ (2 : ℝ) * (∫⁻ x, ‖grad (E := E) f.1 x‖ₑ ^ (2 : ℝ) ∂μ) := by
-                exact congrArg (fun z => ‖a‖ₑ ^ (2 : ℝ) * z) hEval
-      exact hInt
+    have hsq := lintegral_enorm_sub_sq_le (μ := μ) a f
     -- Take the `1/2` power on both sides and simplify.
     have hsq' :
         (∫⁻ x, ‖f.1 (x + a) - f.1 x‖ₑ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) ≤
@@ -333,12 +349,12 @@ lemma norm_translateL2_sub_toL2_le (a : E) (f : ↥(C1c (E := E))) :
   have h := enorm_translateL2_sub_toL2_le (μ := μ) (E := E) a f
   have hA_ne_top :
       (‖translateL2 (μ := μ) (F := ℝ) a (toL2 (μ := μ) (E := E) f) -
-            toL2 (μ := μ) (E := E) f‖ₑ : ℝ≥0∞) ≠ ∞ := by
+            toL2 (μ := μ) (E := E) f‖ₑ : ℝ≥0∞) ≠ (⊤ : ℝ≥0∞) := by
     simp [enorm]
   have hGrad_ne_top :
-      (‖toL2Grad (μ := μ) (E := E) f‖ₑ : ℝ≥0∞) ≠ ∞ := by
+      (‖toL2Grad (μ := μ) (E := E) f‖ₑ : ℝ≥0∞) ≠ (⊤ : ℝ≥0∞) := by
     simp [enorm]
-  have hB_ne_top : (‖a‖ₑ * ‖toL2Grad (μ := μ) (E := E) f‖ₑ : ℝ≥0∞) ≠ ∞ := by
+  have hB_ne_top : (‖a‖ₑ * ‖toL2Grad (μ := μ) (E := E) f‖ₑ : ℝ≥0∞) ≠ (⊤ : ℝ≥0∞) := by
     refine ENNReal.mul_ne_top ?_ hGrad_ne_top
     simp [enorm]
   have h' :
@@ -346,7 +362,7 @@ lemma norm_translateL2_sub_toL2_le (a : E) (f : ↥(C1c (E := E))) :
             toL2 (μ := μ) (E := E) f‖ₑ).toReal ≤
         (‖a‖ₑ * ‖toL2Grad (μ := μ) (E := E) f‖ₑ).toReal := by
     exact (ENNReal.toReal_le_toReal hA_ne_top hB_ne_top).2 h
-  simpa [ENNReal.toReal_mul, toReal_enorm'] using h'
+  simpa only [ENNReal.toReal_mul, toReal_enorm] using h'
 
 end
 
diff --git a/RellichKondrachov/MeasureTheory/Function/LpSpace/Restrict.lean b/RellichKondrachov/MeasureTheory/Function/LpSpace/Restrict.lean
index bb9c6e5..5d1561e 100644
--- a/RellichKondrachov/MeasureTheory/Function/LpSpace/Restrict.lean
+++ b/RellichKondrachov/MeasureTheory/Function/LpSpace/Restrict.lean
@@ -1,16 +1,16 @@
-import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import Mathlib.MeasureTheory.Function.LpSpace.Basic
-
 /-
 Copyright (c) 2026 Adam Benenson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Benenson
 -/
 
+import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+import Mathlib.MeasureTheory.Function.LpSpace.Basic
+
 /-!
 # `RellichKondrachov.MeasureTheory.Function.LpSpace.Restrict`
 
-`L^p` extension-by-zero maps for restricted measures.
+`«L»^p` extension-by-zero maps for restricted measures.
 
 Mathlib provides the equivalence
 
@@ -42,7 +42,8 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
 variable {p : ℝ≥0∞} [Fact (1 ≤ p)]
 variable {s : Set α} (hs : MeasurableSet s)
 
-private noncomputable def extendByZeroFun (f : Lp E p (μ.restrict s)) : Lp E p μ :=
+/-- Extend an Lp function from a restricted measure by zero outside the set. -/
+noncomputable def extendByZeroFun (f : Lp E p (μ.restrict s)) : Lp E p μ :=
   let hf : MemLp (fun x : α => f x) p (μ.restrict s) := Lp.memLp f
   let hfi : MemLp (s.indicator fun x : α => f x) p μ :=
     (memLp_indicator_iff_restrict (μ := μ) (p := p) (s := s) (f := fun x : α => f x) hs).2 hf
@@ -63,7 +64,7 @@ noncomputable def extendByZeroₗ : Lp E p (μ.restrict s) →ₗ[ℝ] Lp E p μ
     refine Lp.ext ?_
     have h_add_restrict :
         (fun x : α => (f + g) x) =ᵐ[μ.restrict s] fun x : α => f x + g x := by
-      simpa using (Lp.coeFn_add (μ := μ.restrict s) f g)
+      exact (Lp.coeFn_add (μ := μ.restrict s) f g)
     have h_add_on :
         ∀ᵐ x : α ∂μ, x ∈ s → (f + g) x = f x + g x :=
       (ae_restrict_iff' (μ := μ) (s := s) hs).1 h_add_restrict
@@ -95,8 +96,7 @@ noncomputable def extendByZeroₗ : Lp E p (μ.restrict s) →ₗ[ℝ] Lp E p μ
             simp [hf, hg]
         _ = (extendByZeroFun (μ := μ) (p := p) (s := s) hs f +
               extendByZeroFun (μ := μ) (p := p) (s := s) hs g) x := hadd'
-    ·
-      have hadd' :
+    · have hadd' :
           extendByZeroFun (μ := μ) (p := p) (s := s) hs f x +
               extendByZeroFun (μ := μ) (p := p) (s := s) hs g x =
             (extendByZeroFun (μ := μ) (p := p) (s := s) hs f +
@@ -117,7 +117,7 @@ noncomputable def extendByZeroₗ : Lp E p (μ.restrict s) →ₗ[ℝ] Lp E p μ
     refine Lp.ext ?_
     have h_smul_restrict :
         (fun x : α => (c • f) x) =ᵐ[μ.restrict s] fun x : α => c • f x := by
-      simpa using (Lp.coeFn_smul (μ := μ.restrict s) c f)
+      exact (Lp.coeFn_smul (μ := μ.restrict s) c f)
     have h_smul_on :
         ∀ᵐ x : α ∂μ, x ∈ s → (c • f) x = c • f x :=
       (ae_restrict_iff' (μ := μ) (s := s) hs).1 h_smul_restrict
@@ -141,8 +141,7 @@ noncomputable def extendByZeroₗ : Lp E p (μ.restrict s) →ₗ[ℝ] Lp E p μ
         _ = c • s.indicator (fun x : α => f x) x := by simp [Set.indicator_of_mem, hx]
         _ = c • extendByZeroFun (μ := μ) (p := p) (s := s) hs f x := by simp [hf]
         _ = (c • extendByZeroFun (μ := μ) (p := p) (s := s) hs f) x := hsmul'
-    ·
-      have hsmul' :
+    · have hsmul' :
           c • extendByZeroFun (μ := μ) (p := p) (s := s) hs f x =
             (c • extendByZeroFun (μ := μ) (p := p) (s := s) hs f) x := by
         simpa [Pi.smul_apply] using hsmul.symm