diff --git a/LeanPool/NashEmbedding.lean b/LeanPool/NashEmbedding.lean
index 5a4a10dc5c..fad6e6f599 100644
--- a/LeanPool/NashEmbedding.lean
+++ b/LeanPool/NashEmbedding.lean
@@ -6,6 +6,8 @@ Authors: David Wiygul
 module
 
 
+-- Preserve the entry point's tactic re-exports for downstream users.
+public import Mathlib.Tactic -- shake: keep
 public import LeanPool.NashEmbedding.NashEmbedding
 public import LeanPool.NashEmbedding.NashEmbedding.Compact.AmbientMetric
 public import LeanPool.NashEmbedding.NashEmbedding.Compact.Main
diff --git a/LeanPool/NashEmbedding/Imports.lean b/LeanPool/NashEmbedding/Imports.lean
index 5de5c8e6d1..2adbf75fe4 100644
--- a/LeanPool/NashEmbedding/Imports.lean
+++ b/LeanPool/NashEmbedding/Imports.lean
@@ -62,3 +62,4 @@ public import LeanPool.NashEmbedding.NashEmbeddingTest.NashCompact
 public import LeanPool.NashEmbedding.NashEmbeddingTest.NashTorus
 public import LeanPool.NashEmbedding.NashEmbeddingTest.RealizableMetrics
 public import LeanPool.NashEmbedding.Solution
+public import LeanPool.NashEmbedding.Tactics
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Compact/AmbientMetric.lean b/LeanPool/NashEmbedding/NashEmbedding/Compact/AmbientMetric.lean
index bc88ce48a6..33c51d5bf7 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Compact/AmbientMetric.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Compact/AmbientMetric.lean
@@ -20,7 +20,7 @@ public import Mathlib.Geometry.Manifold.Algebra.LieGroup
 public import Mathlib.Geometry.Manifold.Sheaf.Basic
 public import Mathlib.Geometry.Manifold.VectorBundle.Riemannian
 public import Mathlib.Geometry.Manifold.VectorField.Pullback
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 
 /-!
 # The ambient metric along an immersion
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Compact/Main.lean b/LeanPool/NashEmbedding/NashEmbedding/Compact/Main.lean
index a6f158991d..7df056c3b3 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Compact/Main.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Compact/Main.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import Mathlib.Geometry.Manifold.Riemannian.Basic
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Main
 public import LeanPool.NashEmbedding.NashEmbedding.Compact.WhitneyExtension
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Compact/WhitneyExtension.lean b/LeanPool/NashEmbedding/NashEmbedding/Compact/WhitneyExtension.lean
index 03b3ec7478..60771c5625 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Compact/WhitneyExtension.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Compact/WhitneyExtension.lean
@@ -12,7 +12,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
 -/
 module
 
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import Mathlib.Geometry.Manifold.WhitneyEmbedding
 import all Mathlib.Geometry.Manifold.WhitneyEmbedding
 
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Riemannian/Pullback.lean b/LeanPool/NashEmbedding/NashEmbedding/Riemannian/Pullback.lean
index f00ef97eed..b05fa4a46e 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Riemannian/Pullback.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Riemannian/Pullback.lean
@@ -382,6 +382,13 @@ theorem prodForm_contMDiff (g : ContMDiffRiemannianMetric I ∞ E (TangentSpace
   have hsnd : ContMDiff (I.prod I') I' ∞ (Prod.snd : M × M' → M') := contMDiff_snd
   have hA := pullbackForm_contMDiff (I := I.prod I') (J := I) g hfst
   have hB := pullbackForm_contMDiff (I := I.prod I') (J := I') g' hsnd
+  -- Fix the bundle instances before asking for smoothness of the sum of sections.
+  let : ∀ p : M × M', AddCommGroup
+      (TangentSpace (I.prod I') p →L[ℝ] TangentSpace (I.prod I') p →L[ℝ] ℝ) :=
+    fun _ => inferInstance
+  let : ∀ p : M × M', Module ℝ
+      (TangentSpace (I.prod I') p →L[ℝ] TangentSpace (I.prod I') p →L[ℝ] ℝ) :=
+    fun _ => inferInstance
   refine (hA.add_section hB).congr fun p => ?_
   have hp : prodFormT g g' p =
       (fun p => pullbackFormT (I := I.prod I') (J := I) Prod.fst g p) p +
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Basic.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Basic.lean
index a6bb85351e..ec44d43d4c 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Basic.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Basic.lean
@@ -19,7 +19,7 @@ public import Mathlib.Analysis.InnerProductSpace.Basic
 public import Mathlib.Analysis.LocallyConvex.AbsConvexOpen
 public import Mathlib.Analysis.SpecialFunctions.ExpDeriv
 public import Mathlib.Analysis.SpecialFunctions.Pow.Real
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 
 /-!
 # Sobolev spaces on the torus — definitions
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/CoeffTransport.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/CoeffTransport.lean
index d4231fb108..0f34957c8c 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/CoeffTransport.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/CoeffTransport.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Periodization
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.SynthesisRegularity
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.ConvolutionAlgebra
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/CompactInclusion.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/CompactInclusion.lean
index 6266b0d32b..fbcc30d60c 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/CompactInclusion.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/CompactInclusion.lean
@@ -13,8 +13,9 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
   — at the request of David Wiygul
 -/
 public import Mathlib.Algebra.Order.Ring.Star
+public import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
 public import Mathlib.Data.Pi.Interval
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Limits
 
 /-!
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Convolution.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Convolution.lean
index dc707de9c9..f027a9b860 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Convolution.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Convolution.lean
@@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
   — at the request of David Wiygul
 -/
 public import Mathlib.MeasureTheory.Measure.Haar.NormedSpace
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Distribution
 
 /-!
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/ConvolutionAlgebra.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/ConvolutionAlgebra.lean
index 1e39a07131..6a8eabb222 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/ConvolutionAlgebra.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/ConvolutionAlgebra.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Differentiation
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.FourierSynthesis
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Differentiation.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Differentiation.lean
index 407936eb67..e5951b57b4 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Differentiation.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Differentiation.lean
@@ -14,7 +14,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
 -/
 public import Mathlib.Analysis.Normed.Group.Tannery
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Summability
 
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Distribution.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Distribution.lean
index 7fea9c9998..44c4925ee9 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Distribution.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Distribution.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.CompactInclusion
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Summability
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/FourierSynthesis.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/FourierSynthesis.lean
index 9615ad1e8d..9f4cdfe4b5 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/FourierSynthesis.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/FourierSynthesis.lean
@@ -14,7 +14,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
 -/
 public import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
 public import Mathlib.MeasureTheory.Integral.Pi
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Summability
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Differentiation
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Inequalities.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Inequalities.lean
index dea099daef..a2231c7c01 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Inequalities.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Inequalities.lean
@@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
   — at the request of David Wiygul
 -/
 public import Mathlib.Data.Finsupp.Notation
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Distribution
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Periodization
 
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/IntegrationByParts.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/IntegrationByParts.lean
index f9bea18ed2..64c004ddc3 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/IntegrationByParts.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/IntegrationByParts.lean
@@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
   — at the request of David Wiygul
 -/
 public import Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Convolution
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Periodization
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.RiemannSum
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Limits.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Limits.lean
index 490a07cade..e9d1a3963f 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Limits.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Limits.lean
@@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
   — at the request of David Wiygul
 -/
 public import Mathlib.Algebra.Order.Chebyshev
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Differentiation
 
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Mollifier.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Mollifier.lean
index 25aabfc5d7..f6d15fd65e 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Mollifier.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Mollifier.lean
@@ -15,7 +15,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
 public import Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
 public import Mathlib.Analysis.Calculus.BumpFunction.Normed
 public import Mathlib.Analysis.Real.Pi.Bounds
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.RiemannSum
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.IntegrationByParts
 
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Multiplication.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Multiplication.lean
index 82277860fa..7ca3463548 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Multiplication.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Multiplication.lean
@@ -15,7 +15,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
 public import Mathlib.Algebra.Ring.IsFormallyReal
 public import Mathlib.Data.Int.Star
 public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import Mathlib.Topology.Separation.CompletelyRegular
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Distribution
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/MultiplicationBootstrap.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/MultiplicationBootstrap.lean
index 982e05ed80..68da07dbf3 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/MultiplicationBootstrap.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/MultiplicationBootstrap.lean
@@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
   — at the request of David Wiygul
 -/
 public import Mathlib.Analysis.Complex.ExponentialBounds
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Summability
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Distribution
@@ -89,24 +89,24 @@ For k ≥ 1 and |ρ| ≤ 1/(2k), we have (1+ρ)^k ≤ 2.
 lemma one_add_pow_le_two {k : ℕ} (hk : 1 ≤ k) {ρ : ℝ}
     (hρ : |ρ| ≤ 1 / (2 * (k : ℝ))) :
     (1 + ρ) ^ k ≤ 2 := by
-  by_cases hρ_neg : ρ < 0;
-  · exact le_trans ( pow_le_one₀ ( by
-    linarith [ abs_le.mp hρ, show ( 1 : ℝ ) / ( 2 * k ) ≤ 1 by
-      rw [ div_le_iff₀ ] <;> norm_cast <;> linarith ] ) ( by
-    linarith [ abs_le.mp hρ, show ( 1 : ℝ ) / ( 2 * k ) ≤ 1 by
-      rw [ div_le_iff₀ ] <;> norm_cast <;> linarith ] ) ) ( by
-    norm_num );
-  · -- For ρ ≥ 0, use (1+ρ) ≤ exp(ρ), so (1+ρ)^k ≤ exp(kρ) ≤ exp(1/2) < 2.
-    have h_exp : (1 + ρ) ^ k ≤ Real.exp (k * ρ) := by
-      rw [ ← Real.rpow_natCast, Real.rpow_def_of_pos ( by linarith ) ]; norm_num; ring_nf;
-      exact mul_le_mul_of_nonneg_right ( le_trans ( Real.log_le_sub_one_of_pos ( by
-        linarith ) ) ( by
-        linarith ) ) ( Nat.cast_nonneg _ );
-    refine le_trans h_exp ?_;
-    rw [ ← Real.log_le_log_iff ( by positivity ) ( by positivity ), Real.log_exp ];
-    exact le_trans ( mul_le_mul_of_nonneg_left ( le_of_abs_le hρ ) ( Nat.cast_nonneg _ ) ) ( by
-      rw [ mul_div, div_le_iff₀ ] <;> nlinarith [ Real.log_two_gt_d9, show ( k : ℝ ) ≥ 1 by
-        norm_cast ] )
+  have hk1 : (1 : ℝ) ≤ k := by exact_mod_cast hk
+  have hkpos : (0 : ℝ) < k := lt_of_lt_of_le zero_lt_one hk1
+  have hbound : (1 : ℝ) / (2 * k) ≤ 1 := by
+    apply (div_le_iff₀ (by positivity)).2
+    linarith only [hk1]
+  have hbase : 0 ≤ 1 + ρ := by linarith only [(abs_le.mp hρ).1, hbound]
+  have hproduct : (k : ℝ) * ρ ≤ 1 / 2 := by
+    have h := (le_div_iff₀ (show (0 : ℝ) < 2 * k by positivity)).mp (le_of_abs_le hρ)
+    linarith only [h]
+  calc
+    (1 + ρ) ^ k ≤ (Real.exp ρ) ^ k :=
+      pow_le_pow_left₀ hbase (by simpa only [add_comm] using Real.add_one_le_exp ρ) k
+    _ = Real.exp (k * ρ) := (Real.exp_nat_mul ρ k).symm
+    _ ≤ Real.exp (1 / 2) := Real.exp_le_exp.mpr hproduct
+    _ ≤ 2 := by
+      apply (Real.log_le_log_iff (by positivity) (by norm_num)).mp
+      rw [Real.log_exp]
+      linarith only [Real.log_two_gt_d9]
 
 /-
 Case B of the refined weight inequality:
@@ -116,41 +116,52 @@ Case B of the refined weight inequality:
 lemma refined_weight_case_b {k : ℕ} (hk : 1 ≤ k) (i j : Fin n → ℤ)
     (hsmall : ∑ l, (j l : ℝ) ^ 2 ≤ ∑ l, (i l : ℝ) ^ 2 / (64 * (k : ℝ) ^ 2)) :
     weight n (k : ℝ) (i + j) ≤ 2 * weight n (k : ℝ) i := by
-  -- Applying the inequality $(1 + \rho)^k \leq 2$ to $\rho$.
-  have h_rho : (1 + (2 * (∑ l, (i l : ℝ) * (j l : ℝ)) + (∑ l, ((j l : ℝ) ^ 2))) / (1 + (∑ l, ((i
-      l : ℝ) ^ 2)))) ^ k ≤ 2 := by
-    refine one_add_pow_le_two hk ?_;
-    -- We have $|2 \cdot \sum i_l \cdot j_l| \leq 2 \cdot \sqrt{S_i} \cdot \sqrt{S_j}$
-    -- (Cauchy-Schwarz).
-    have h_cauchy_schwarz : |2 * ∑ l : Fin n, ((i l : ℝ) * (j l : ℝ))| ≤ 2 * Real.sqrt (∑ l :
-        Fin n, ((i l : ℝ) ^ 2)) * Real.sqrt (∑ l : Fin n, ((j l : ℝ) ^ 2)) := by
-      -- By the Cauchy-Schwarz inequality, we have that for any vectors $u$ and $v$ of
-      -- equal length, $(∑ l, u l * v l)^2 ≤ (∑ l, u l^2) * (∑ l, v l^2)$.
-      have h_cauchy_schwarz : ∀ (u v : Fin n → ℝ), (∑ l, u l * v l)^2 ≤ (∑ l, u l^2) * (∑ l, v
-          l^2) := by
-        exact fun u v => Finset.sum_mul_sq_le_sq_mul_sq Finset.univ u v;
-      rw [ abs_mul, abs_two ];
-      rw [ mul_assoc ]; exact mul_le_mul_of_nonneg_left ( Real.abs_le_sqrt <| by
-        simpa using h_cauchy_schwarz _ _ ) zero_le_two |> le_trans <| by
-        rw [ Real.sqrt_mul <| Finset.sum_nonneg fun _ _ => sq_nonneg _ ];
-    generalize_proofs at *; (
-    -- We have $\sqrt{S_j} \leq \sqrt{S_i / (64k^2)} = \sqrt{S_i} / (8k)$.
-    have h_sqrt_bound : Real.sqrt (∑ l : Fin n, ((j l : ℝ) ^ 2)) ≤ Real.sqrt (∑ l : Fin n, ((i l
-        : ℝ) ^ 2)) / (8 * k) := by
-      convert Real.sqrt_le_sqrt hsmall using 1; ring_nf; norm_num [ show k ≠ 0 by linarith ];
-      norm_num [ ← Finset.mul_sum _ _ _, ← Finset.sum_mul ]; ring
-    generalize_proofs at *; (
-    rw [ abs_div, abs_of_nonneg ( by
-      positivity : ( 0 : ℝ ) ≤ 1 + ∑ l : Fin n, ( i l : ℝ ) ^ 2 ) ]; rw [ div_le_div_iff₀ ] <;>
-        try positivity;
-    rw [ le_div_iff₀ ( by positivity ) ] at h_sqrt_bound;
-    cases abs_cases ( 2 * ∑ l : Fin n, ( i l : ℝ ) * j l + ∑ l : Fin n, ( j l : ℝ ) ^ 2 ) <;>
-      cases abs_cases ( 2 * ∑ l : Fin n, ( i l : ℝ ) * j l ) <;> nlinarith [ show ( k : ℝ ) ≥ 1 by
-      norm_cast, Real.sqrt_nonneg ( ∑ l : Fin n, ( i l : ℝ ) ^ 2 ), Real.sqrt_nonneg ( ∑ l : Fin
-        n, ( j l : ℝ ) ^ 2 ), Real.mul_self_sqrt ( show 0 ≤ ∑ l : Fin n, ( i l : ℝ ) ^ 2 by
-      exact Finset.sum_nonneg fun _ _ => sq_nonneg _ ), Real.mul_self_sqrt ( show 0 ≤ ∑ l : Fin
-        n, ( j l : ℝ ) ^ 2 by
-      exact Finset.sum_nonneg fun _ _ => sq_nonneg _ ) ]));
+  have hi : 0 ≤ ∑ l, (i l : ℝ) ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _
+  have hj : 0 ≤ ∑ l, (j l : ℝ) ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _
+  have hk1 : (1 : ℝ) ≤ k := by exact_mod_cast hk
+  have hkpos : (0 : ℝ) < k := lt_of_lt_of_le zero_lt_one hk1
+  have hsmall' : 64 * (k : ℝ) ^ 2 * (∑ l, (j l : ℝ) ^ 2) ≤ ∑ l, (i l : ℝ) ^ 2 := by
+    rw [← Finset.sum_div] at hsmall
+    simpa only [mul_comm] using (le_div_iff₀ (by positivity)).mp hsmall
+  -- A weighted sum-of-squares bound avoids introducing square roots of both norms.
+  have hcross : 4 * (k : ℝ) * |2 * ∑ l, (i l : ℝ) * (j l : ℝ)| ≤
+      (∑ l, (i l : ℝ) ^ 2) + 16 * (k : ℝ) ^ 2 * (∑ l, (j l : ℝ) ^ 2) := by
+    calc
+      _ = |∑ l, 2 * (i l : ℝ) * ((j l : ℝ) * (4 * (k : ℝ)))| := by
+        have heq : (∑ l, 2 * (i l : ℝ) * ((j l : ℝ) * (4 * (k : ℝ)))) =
+            8 * (k : ℝ) * ∑ l, (i l : ℝ) * (j l : ℝ) := by
+          rw [Finset.mul_sum]
+          apply Finset.sum_congr rfl
+          intro l _
+          ring
+        rw [heq]
+        norm_num [abs_mul, abs_of_pos hkpos]
+        ring
+      _ ≤ ∑ l, |2 * (i l : ℝ) * ((j l : ℝ) * (4 * (k : ℝ)))| :=
+        Finset.abs_sum_le_sum_abs _ _
+      _ ≤ ∑ l, ((i l : ℝ) ^ 2 + ((j l : ℝ) * (4 * (k : ℝ))) ^ 2) := by
+        apply Finset.sum_le_sum
+        intro l _
+        rw [abs_mul, abs_mul, abs_two]
+        simpa only [sq_abs] using
+          two_mul_le_add_sq |(i l : ℝ)| |(j l : ℝ) * (4 * (k : ℝ))|
+      _ = _ := by
+        norm_num [mul_pow, Finset.sum_add_distrib, ← Finset.sum_mul]
+        ring
+  have hkb : (k : ℝ) * (∑ l, (j l : ℝ) ^ 2) ≤
+      (k : ℝ) ^ 2 * (∑ l, (j l : ℝ) ^ 2) :=
+    mul_le_mul_of_nonneg_right (by nlinarith only [hk1]) hj
+  have h_rho : (1 + (2 * (∑ l, (i l : ℝ) * (j l : ℝ)) + (∑ l, ((j l : ℝ) ^ 2))) /
+      (1 + (∑ l, ((i l : ℝ) ^ 2)))) ^ k ≤ 2 := by
+    apply one_add_pow_le_two hk
+    rw [abs_div, abs_of_pos (show 0 < 1 + ∑ l, (i l : ℝ) ^ 2 from
+      add_pos_of_pos_of_nonneg zero_lt_one hi),
+      div_le_div_iff₀ (by positivity) (show (0 : ℝ) < 2 * k by positivity)]
+    have htriangle := mul_le_mul_of_nonneg_right
+      (abs_add_le (2 * ∑ l, (i l : ℝ) * (j l : ℝ)) (∑ l, (j l : ℝ) ^ 2))
+      (show (0 : ℝ) ≤ 2 * k by positivity)
+    rw [abs_of_nonneg hj] at htriangle
+    nlinarith only [htriangle, hcross, hsmall', hkb, hi]
   -- By definition of `weight`, we know that `weight n k (i + j) = (1 + ∑ l, (i l + j l : ℝ) ^
   -- 2) ^ k`.
   simp only [weight, Pi.add_apply, Int.cast_add, rpow_natCast, ge_iff_le];
@@ -176,75 +187,82 @@ lemma refined_weight_ineq {k : ℕ} (hk : 1 ≤ k) (i j : Fin n → ℤ) :
       2 * (weight n (k : ℝ) i + weight n (k : ℝ) j) +
       mt3BStar k * (weight n ((k : ℝ) - 1) i * weight n 1 j +
                      weight n 1 i * weight n ((k : ℝ) - 1) j) := by
-  by_cases hB : ∑ l, (j l : ℝ) ^ 2 ≤ ∑ l, (i l : ℝ) ^ 2 / (64 * (k : ℝ) ^ 2);
-  · refine le_add_of_le_of_nonneg ?_ ?_;
-    · exact le_trans ( refined_weight_case_b hk i j hB ) ( by
-      linarith [ show 0 ≤ weight n ( k : ℝ ) j from weight_nonneg _ _ ] );
-    · exact mul_nonneg ( mt3BStar_nonneg hk ) ( add_nonneg ( mul_nonneg ( weight_nonneg _ _ ) (
-        weight_nonneg _ _ ) ) ( mul_nonneg ( weight_nonneg _ _ ) ( weight_nonneg _ _ ) ) );
-  · by_cases hA : ∑ l, (i l : ℝ) ^ 2 ≤ ∑ l, (j l : ℝ) ^ 2 / (64 * (k : ℝ) ^ 2);
-    · -- Apply the refined weight case b to (j, i) instead.
-      have h_case_b : weight n (k : ℝ) (j + i) ≤ 2 * weight n (k : ℝ) j := by
-        apply refined_weight_case_b hk j i hA;
-      rw [ add_comm ] at h_case_b;
-      refine le_add_of_le_of_nonneg ?_ ?_;
-      · exact h_case_b.trans ( mul_le_mul_of_nonneg_left ( le_add_of_nonneg_left <| by
-        exact Real.rpow_nonneg ( add_nonneg zero_le_one <| Finset.sum_nonneg fun _ _ =>
-          sq_nonneg _ ) _ ) zero_le_two );
-      · exact mul_nonneg ( mt3BStar_nonneg hk ) ( add_nonneg ( mul_nonneg ( weight_nonneg _ _ )
-          ( weight_nonneg _ _ ) ) ( mul_nonneg ( weight_nonneg _ _ ) ( weight_nonneg _ _ ) ) );
-    · -- Case C: S_j > S_i/(64k²) AND S_i > S_j/(64k²). Then:
-      -- S_i < 64k²*S_j, so X = 1+S_i ≤ 1+64k²*S_j ≤ 64k²*(1+S_j) = 64k²*Y (using 1 ≤ 64k²
-      -- since k ≥ 1).
-      -- Similarly Y ≤ 64k²*X.
-      have hX : (1 + ∑ l, (i l : ℝ) ^ 2) ≤ 64 * (k : ℝ) ^ 2 * (1 + ∑ l, (j l : ℝ) ^ 2) := by
-        norm_num [ ← Finset.sum_div _ _ _ ] at *;
-        rw [ div_lt_iff₀ ] at hB <;> nlinarith [ show ( k : ℝ ) ^ 2 ≥ 1 by norm_cast; nlinarith ]
-      have hY : (1 + ∑ l, (j l : ℝ) ^ 2) ≤ 64 * (k : ℝ) ^ 2 * (1 + ∑ l, (i l : ℝ) ^ 2) := by
-        norm_num [ ← Finset.sum_div _ _ _ ] at *;
-        rw [ div_lt_iff₀ ] at hA <;> nlinarith [ show ( k : ℝ ) ^ 2 ≥ 1 by norm_cast; nlinarith ];
-      -- Step C1: 1+S_{i+j} ≤ 2(X+Y). Since S_{i+j} = ∑(i_l+j_l)² ≤ 2S_i+2S_j (by (a+b)² ≤
-      -- 2a²+2b²), we get 1+S_{i+j} ≤ 1+2S_i+2S_j ≤ 2(1+S_i)+2(1+S_j) = 2X+2Y = 2(X+Y).
-      have hC1 : 1 + ∑ l, ((i l + j l) : ℝ) ^ 2 ≤ 2 * (1 + ∑ l, (i l : ℝ) ^ 2 + 1 + ∑ l, (j l :
-          ℝ) ^ 2) := by
-        have hC1 : ∑ l, ((i l + j l) : ℝ) ^ 2 ≤ 2 * (∑ l, (i l : ℝ) ^ 2 + ∑ l, (j l : ℝ) ^ 2) := by
-          rw [ ← Finset.sum_add_distrib, Finset.mul_sum _ _ _ ];
-          exact Finset.sum_le_sum fun _ _ => by linarith [ sq_nonneg ( i ‹_› - j ‹_› : ℝ ) ];
-        linarith;
-      -- Step C2: Use add_pow_le for Nat.pow. (X+Y)^k ≤ 2^{k-1}*(X^k+Y^k). So (2(X+Y))^k =
-      -- 2^k*(X+Y)^k ≤ 2^k*2^{k-1}*(X^k+Y^k) = 2^{2k-1}*(X^k+Y^k).
-      have hC2 : (1 + ∑ l, ((i l + j l) : ℝ) ^ 2) ^ k ≤ 2 ^ (2 * k - 1) * ((1 + ∑ l, (i l : ℝ) ^
-          2) ^ k + (1 + ∑ l, (j l : ℝ) ^ 2) ^ k) := by
-        have hC2 : (1 + ∑ l, (i l : ℝ) ^ 2 + 1 + ∑ l, (j l : ℝ) ^ 2) ^ k ≤ 2 ^ (k - 1) * ((1 + ∑
-            l, (i l : ℝ) ^ 2) ^ k + (1 + ∑ l, (j l : ℝ) ^ 2) ^ k) := by
-          have hC2 : ∀ (x y : ℝ), 0 ≤ x → 0 ≤ y → (x + y) ^ k ≤ 2 ^ (k - 1) * (x ^ k + y ^ k) := by
-            exact fun x y a a_1 => add_pow_le a a_1 k;
-          convert hC2 ( 1 + ∑ l, ( i l : ℝ ) ^ 2 ) ( 1 + ∑ l, ( j l : ℝ ) ^ 2 ) ( by
-            exact add_nonneg zero_le_one <| Finset.sum_nonneg fun _ _ => sq_nonneg _ ) ( by
-            exact add_nonneg zero_le_one <| Finset.sum_nonneg fun _ _ => sq_nonneg _ ) using 1;
-              ring;
-        refine le_trans ( pow_le_pow_left₀ ( by
-          exact add_nonneg zero_le_one <| Finset.sum_nonneg fun _ _ => sq_nonneg _ ) hC1 _ ) ?_;
-        rw [ mul_pow ];
-        convert mul_le_mul_of_nonneg_left hC2 ( pow_nonneg zero_le_two k ) using 1; rw [ show 2
-          * k - 1 = k - 1 + k by
-          omega ]; ring;
-      -- Step C4: Since X ≤ 64k²*Y, X^k = X^{k-1}*X ≤ 64k²*X^{k-1}*Y. Similarly Y^k ≤
-      -- 64k²*X*Y^{k-1}. So (X^k+Y^k) ≤ 64k²*(X^{k-1}*Y + X*Y^{k-1}).
-      have hC4 : (1 + ∑ l, (i l : ℝ) ^ 2) ^ k + (1 + ∑ l, (j l : ℝ) ^ 2) ^ k ≤ 64 * (k : ℝ) ^ 2
-          * ((1 + ∑ l, (i l : ℝ) ^ 2) ^ (k - 1) * (1 + ∑ l, (j l : ℝ) ^ 2) + (1 + ∑ l, (i l : ℝ)
-          ^ 2) * (1 + ∑ l, (j l : ℝ) ^ 2) ^ (k - 1)) := by
-        rcases k with ( _ | k ) <;> simp_all +decide [ pow_succ' ];
-        nlinarith [ pow_nonneg ( show 0 ≤ 1 + ∑ x : Fin n, ( i x : ℝ ) * i x by
-          exact add_nonneg zero_le_one <| Finset.sum_nonneg fun _ _ => mul_self_nonneg _ ) k,
-            pow_nonneg ( show 0 ≤ 1 + ∑ x : Fin n, ( j x : ℝ ) * j x by
-          exact add_nonneg zero_le_one <| Finset.sum_nonneg fun _ _ => mul_self_nonneg _ ) k ];
-      unfold weight mt3BStar;
-      rcases k with ( _ | k ) <;> norm_num [ Nat.mul_succ, pow_succ' ] at *;
-      norm_cast at *; norm_num [ Nat.mul_succ, pow_succ' ] at *;
-      rw [ Int.subNatNat_of_le ( by
-        linarith ) ]; norm_cast; norm_num [ Nat.mul_succ, pow_succ' ] at *;
-      rw [ Int.subNatNat_eq_coe ]; push_cast; nlinarith [ pow_pos ( zero_lt_two' ℤ ) ( 2 * k ) ]
+  have hrest : 0 ≤ mt3BStar k * (weight n ((k : ℝ) - 1) i * weight n 1 j +
+      weight n 1 i * weight n ((k : ℝ) - 1) j) :=
+    mul_nonneg (mt3BStar_nonneg hk)
+      (add_nonneg (mul_nonneg (weight_nonneg _ _) (weight_nonneg _ _))
+        (mul_nonneg (weight_nonneg _ _) (weight_nonneg _ _)))
+  by_cases hB : ∑ l, (j l : ℝ) ^ 2 ≤ ∑ l, (i l : ℝ) ^ 2 / (64 * (k : ℝ) ^ 2)
+  · exact le_add_of_le_of_nonneg
+      ((refined_weight_case_b hk i j hB).trans
+        (mul_le_mul_of_nonneg_left (le_add_of_nonneg_right (weight_nonneg _ _)) zero_le_two))
+      hrest
+  by_cases hA : ∑ l, (i l : ℝ) ^ 2 ≤ ∑ l, (j l : ℝ) ^ 2 / (64 * (k : ℝ) ^ 2)
+  · rw [add_comm i j]
+    exact le_add_of_le_of_nonneg
+      ((refined_weight_case_b hk j i hA).trans
+        (mul_le_mul_of_nonneg_left (le_add_of_nonneg_left (weight_nonneg _ _)) zero_le_two))
+      hrest
+  rw [← Finset.sum_div] at hB hA
+  let X : ℝ := 1 + ∑ l, (i l : ℝ) ^ 2
+  let Y : ℝ := 1 + ∑ l, (j l : ℝ) ^ 2
+  have hX0 : 0 ≤ X := add_nonneg zero_le_one (Finset.sum_nonneg fun _ _ => sq_nonneg _)
+  have hY0 : 0 ≤ Y := add_nonneg zero_le_one (Finset.sum_nonneg fun _ _ => sq_nonneg _)
+  have hk1 : (1 : ℝ) ≤ k := by exact_mod_cast hk
+  have hD : (1 : ℝ) ≤ 64 * (k : ℝ) ^ 2 := by nlinarith only [hk1, sq_nonneg (k : ℝ)]
+  have hDpos : 0 < 64 * (k : ℝ) ^ 2 := lt_of_lt_of_le zero_lt_one hD
+  have hX : X ≤ 64 * (k : ℝ) ^ 2 * Y := by
+    have h := (div_lt_iff₀ hDpos).mp
+      (show (∑ l, (i l : ℝ) ^ 2) / (64 * (k : ℝ) ^ 2) < ∑ l, (j l : ℝ) ^ 2
+        from lt_of_not_ge hB)
+    dsimp [X, Y]
+    nlinarith only [h, hD]
+  have hY : Y ≤ 64 * (k : ℝ) ^ 2 * X := by
+    have h := (div_lt_iff₀ hDpos).mp
+      (show (∑ l, (j l : ℝ) ^ 2) / (64 * (k : ℝ) ^ 2) < ∑ l, (i l : ℝ) ^ 2
+        from lt_of_not_ge hA)
+    dsimp [X, Y]
+    nlinarith only [h, hD]
+  have hsum : 1 + ∑ l, ((i l + j l) : ℝ) ^ 2 ≤ 2 * (X + Y) := by
+    have h := Finset.sum_le_sum (s := Finset.univ) fun l _ =>
+      (show ((i l + j l) : ℝ) ^ 2 ≤ 2 * ((i l : ℝ) ^ 2 + (j l : ℝ) ^ 2) by
+        nlinarith only [sq_nonneg ((i l : ℝ) - j l)])
+    rw [← Finset.mul_sum, Finset.sum_add_distrib] at h
+    dsimp [X, Y]
+    linarith only [h]
+  have hpower : (1 + ∑ l, ((i l + j l) : ℝ) ^ 2) ^ k ≤
+      2 ^ (2 * k - 1) * (X ^ k + Y ^ k) := by
+    calc
+      _ ≤ (2 * (X + Y)) ^ k := pow_le_pow_left₀ (by positivity) hsum k
+      _ = 2 ^ k * (X + Y) ^ k := mul_pow _ _ _
+      _ ≤ 2 ^ k * (2 ^ (k - 1) * (X ^ k + Y ^ k)) :=
+        mul_le_mul_of_nonneg_left (add_pow_le hX0 hY0 k) (by positivity)
+      _ = _ := by
+        rw [show 2 * k - 1 = k - 1 + k by omega]
+        ring
+  have hcross : X ^ k + Y ^ k ≤ 64 * (k : ℝ) ^ 2 *
+      (X ^ (k - 1) * Y + X * Y ^ (k - 1)) := by
+    have hXi := mul_le_mul_of_nonneg_left hX (pow_nonneg hX0 (k - 1))
+    have hYi := mul_le_mul_of_nonneg_left hY (pow_nonneg hY0 (k - 1))
+    rw [← pow_succ, Nat.sub_add_cancel hk] at hXi hYi
+    nlinarith only [hXi, hYi]
+  have hk2 : 2 ≤ 2 * k := by simpa only [Nat.mul_one] using Nat.mul_le_mul_left 2 hk
+  have hexponent : ((2 * k - 1 : ℕ) : ℝ) = 2 * (k : ℝ) - 1 := by
+    rw [Nat.cast_sub ((Nat.le_succ 1).trans hk2)]
+    norm_num
+  have hcoefficient : 0 ≤ (2 : ℝ) ^ (2 * k - 1) - 2 := by
+    have h := pow_le_pow_right₀ (show (1 : ℝ) ≤ 2 by norm_num)
+      (show 1 ≤ 2 * k - 1 from Nat.sub_le_sub_right hk2 1)
+    apply sub_nonneg.mpr
+    simpa only [pow_one] using h
+  have hscaled := mul_le_mul_of_nonneg_left hcross hcoefficient
+  have hcast : (k : ℝ) - 1 = ((k - 1 : ℕ) : ℝ) := by rw [Nat.cast_sub hk]; norm_num
+  simp only [weight, mt3BStar, Pi.add_apply, Int.cast_add, hcast, ← hexponent,
+    Real.rpow_natCast, Real.rpow_one]
+  change (1 + ∑ l, ((i l + j l) : ℝ) ^ 2) ^ k ≤
+    2 * (X ^ k + Y ^ k) + 64 * (k : ℝ) ^ 2 * (2 ^ (2 * k - 1) - 2) *
+      (X ^ (k - 1) * Y + X * Y ^ (k - 1))
+  nlinarith only [hpower, hscaled]
 
 /-! ## Half-power form of the refined weight inequality -/
 
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/MultiplicationSharp.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/MultiplicationSharp.lean
index 79ff2d0b3c..9476293b1d 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/MultiplicationSharp.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/MultiplicationSharp.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Summability
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Distribution
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Periodicity.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Periodicity.lean
index 598ff0fe35..1f26ea1e07 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Periodicity.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Periodicity.lean
@@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
   — at the request of David Wiygul
 -/
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 
 /-!
 # Periodicity on ℝⁿ
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Periodization.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Periodization.lean
index 54ce982356..e642b450d3 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Periodization.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Periodization.lean
@@ -16,7 +16,7 @@ public import Mathlib.Analysis.Fourier.AddCircleMulti
 public import Mathlib.Analysis.Real.Pi.Bounds
 public import Mathlib.MeasureTheory.Integral.DivergenceTheorem
 public import Mathlib.MeasureTheory.Measure.Haar.NormedSpace
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import Mathlib.Topology.Separation.CompletelyRegular
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Distribution
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Periodicity
@@ -174,6 +174,33 @@ lemma periodicExtension_contDiff {φ : (Fin n → ℝ) → ℂ}
   exact h_cont_diff.contDiffAt ( hU_open.mem_nhds hxU ) |> fun h => h.congr_of_eventuallyEq (
       Filter.eventuallyEq_of_mem ( hU_open.mem_nhds hxU ) fun y hy => hS y hy ▸ rfl )
 
+/-- A translate with a bounded norm has bounded lattice coordinates. -/
+lemma periodicShift_index_le (x : Fin n → ℝ) (k : Fin n → ℤ) (i : Fin n) :
+    |(k i : ℝ)| ≤ (‖x + periodicShift n k‖ + ‖x‖) / (2 * Real.pi) := by
+  apply (le_div_iff₀ (mul_pos zero_lt_two Real.pi_pos)).2
+  calc
+    |(k i : ℝ)| * (2 * Real.pi) = |(x + periodicShift n k) i - x i| := by
+      simp only [Pi.add_apply, periodicShift, add_sub_cancel_left, abs_mul,
+        abs_of_pos Real.pi_pos, abs_two]
+      ring
+    _ ≤ |(x + periodicShift n k) i| + |x i| := abs_sub _ _
+    _ ≤ ‖x + periodicShift n k‖ + ‖x‖ :=
+      add_le_add (by simpa only [Real.norm_eq_abs] using norm_le_pi_norm (x + periodicShift n k) i)
+        (by simpa only [Real.norm_eq_abs] using norm_le_pi_norm x i)
+
+/-- The lattice coordinates of a translate meeting a ball are uniformly bounded. -/
+lemma periodicShift_index_le_of_mem_ball {R : ℝ} {x y : Fin n → ℝ} (k : Fin n → ℤ)
+    (i : Fin n) (hy : y ∈ Metric.ball x 1) (hshift : ‖y + periodicShift n k‖ ≤ R) :
+    |(k i : ℝ)| ≤ (R + ‖x‖ + 1) / (2 * Real.pi) := by
+  have hdist : ‖y - x‖ < 1 := by
+    rw [← dist_eq_norm]
+    exact hy
+  have hnorm : ‖y‖ ≤ ‖y - x‖ + ‖x‖ := by
+    simpa only [sub_add_cancel] using norm_add_le (y - x) x
+  refine (periodicShift_index_le y k i).trans ?_
+  apply div_le_div_of_nonneg_right _ (by positivity)
+  linarith only [hshift, hdist, hnorm]
+
 /-
 If `φ` has pointwise non-negative real part, its periodic extension does too.
 The nonsummable case follows from the zero convention for `tsum`.
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/PositionSpace.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/PositionSpace.lean
index 47099aff02..6c29318d8f 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/PositionSpace.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/PositionSpace.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Periodization
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Mollifier
 
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Resolvent.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Resolvent.lean
index 228e8e4166..9130d177c3 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Resolvent.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Resolvent.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Differentiation
 
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/RiemannSum.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/RiemannSum.lean
index 0d737b6e89..9f20a6a5c8 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/RiemannSum.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/RiemannSum.lean
@@ -14,7 +14,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
 -/
 public import Mathlib.Data.Int.Star
 public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import Mathlib.Topology.Separation.CompletelyRegular
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Convolution
 
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Summability.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Summability.lean
index 6581d59e13..2b1d06b88d 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Summability.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/Summability.lean
@@ -14,9 +14,10 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
 -/
 public import Mathlib.Algebra.Order.Ring.Star
 public import Mathlib.Analysis.MeanInequalities
+public import Mathlib.Analysis.Normed.Group.FunctionSeries
 public import Mathlib.Analysis.PSeries
 public import Mathlib.Analysis.RCLike.Lemmas
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
 
 /-!
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/SynthesisRegularity.lean b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/SynthesisRegularity.lean
index d42e603dc2..e3de25d594 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Sobolev/SynthesisRegularity.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Sobolev/SynthesisRegularity.lean
@@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
   — at the request of David Wiygul
 -/
 public import Mathlib.Analysis.Calculus.SmoothSeries
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Summability
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Differentiation
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/Approximation/BumpConstruction.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/Approximation/BumpConstruction.lean
index e7379dc386..73ecd8feac 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/Approximation/BumpConstruction.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/Approximation/BumpConstruction.lean
@@ -17,7 +17,7 @@ public import Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
 public import Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
 public import Mathlib.Analysis.Matrix.PosDef
 public import Mathlib.MeasureTheory.Integral.Pi
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import Mathlib.Topology.UniformSpace.Uniformizable
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Basic
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Basic
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/Approximation/RealizeMetric.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/Approximation/RealizeMetric.lean
index 626e0e392f..c0ac56a6a0 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/Approximation/RealizeMetric.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/Approximation/RealizeMetric.lean
@@ -14,7 +14,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
 -/
 public import Mathlib.Algebra.Order.Archimedean.Real.Hom
 public import Mathlib.Algebra.Order.Chebyshev
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Approximation.SmoothMetricApprox
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Approximation.BumpConstruction
 
@@ -66,22 +66,7 @@ lemma exists_finset_periodicExtension {φ : (Fin n → ℝ) → ℂ} (hsupp : Ha
     obtain ⟨y, hy_ball, hy_nonzero⟩ := hk
     have h_bound : ‖y + NashEmbedding.Sobolev.periodicShift n k‖ < R := by
       exact lt_of_not_ge fun h => hy_nonzero <| hR _ h;
-    have h_bound : |(y i + 2 * Real.pi * (k i : ℝ))| ≤ R := by
-      exact le_trans ( by
-        simpa [NashEmbedding.Sobolev.periodicShift] using norm_le_pi_norm ( y +
-          NashEmbedding.Sobolev.periodicShift n k ) i ) h_bound.le;
-    have h_bound : |y i| ≤ ‖x‖ + 1 := by
-      have h_bound : |y i - x i| ≤ ‖y - x‖ := by
-        exact norm_le_pi_norm ( y - x ) i;
-      exact abs_le.mpr ⟨ by
-        linarith [ abs_le.mp h_bound, abs_le.mp ( norm_le_pi_norm x i ), abs_le.mp (
-          norm_le_pi_norm ( y - x ) i ), show ‖y - x‖ < 1 from by
-          rw [← dist_eq_norm]; exact hy_ball ], by
-        linarith [ abs_le.mp h_bound, abs_le.mp ( norm_le_pi_norm x i ), abs_le.mp (
-          norm_le_pi_norm ( y - x ) i ), show ‖y - x‖ < 1 from by
-          rw [← dist_eq_norm]; exact hy_ball ] ⟩;
-    rw [ le_div_iff₀ ] <;> cases abs_cases ( k i : ℝ ) <;> cases abs_cases ( y i + 2 * Real.pi *
-        ( k i : ℝ ) ) <;> cases abs_cases ( y i ) <;> nlinarith [ Real.pi_gt_three ];
+    exact NashEmbedding.Sobolev.periodicShift_index_le_of_mem_ball k i hy_ball h_bound.le
   have h_finite_k : Set.Finite {k : Fin n → ℤ | ∀ i : Fin n, |(k i : ℝ)| ≤ (R + ‖x‖ + 1) / (2 *
       Real.pi)} := by
     have h_finite_k : ∀ i : Fin n, Set.Finite {k : ℤ | |(k : ℝ)| ≤ (R + ‖x‖ + 1) / (2 *
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/Approximation/SmoothMetricApprox.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/Approximation/SmoothMetricApprox.lean
index 909dc4da3e..324b00de4f 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/Approximation/SmoothMetricApprox.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/Approximation/SmoothMetricApprox.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Periodization
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Mollifier
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.PositionSpace
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/Assembly.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/Assembly.lean
index 572397b7ab..0e0fee2a9e 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/Assembly.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/Assembly.lean
@@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
   — at the request of David Wiygul
 -/
 public import Mathlib.LinearAlgebra.Matrix.FiniteDimensional
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Perturbation.Main
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.RealizableMetrics
 
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/Basic.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/Basic.lean
index 101b8cad5d..ea948e32e0 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/Basic.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/Basic.lean
@@ -12,11 +12,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
+public import Mathlib.Analysis.InnerProductSpace.Basic
 public import Mathlib.Analysis.Calculus.ContDiff.Defs
 public import Mathlib.Analysis.LocallyConvex.AbsConvexOpen
 public import Mathlib.Analysis.RCLike.Lemmas
 public import Mathlib.LinearAlgebra.Matrix.PosDef
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Periodicity
 
 /-!
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/FreeEmbedding.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/FreeEmbedding.lean
index f23226a935..8547435f4b 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/FreeEmbedding.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/FreeEmbedding.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Perturbation.Main
 
 /-!
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/Main.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/Main.lean
index ff7d3bb88d..de85a1dd15 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/Main.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/Main.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Approximation.RealizeMetric
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Perturbation.Main
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.FreeEmbedding
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/DualFrame.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/DualFrame.lean
index 362490d465..14d415cea4 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/DualFrame.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/DualFrame.lean
@@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
   — at the request of David Wiygul
 -/
 public import Mathlib.Analysis.Calculus.ContDiff.Operations
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Basic
 
 /-!
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherIdentity.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherIdentity.lean
index 3d4100d7e7..75e336670a 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherIdentity.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherIdentity.lean
@@ -13,7 +13,7 @@ Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anth
   — at the request of David Wiygul
 -/
 public import Mathlib.Analysis.Calculus.FDeriv.Symmetric
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Basic
 
 /-!
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherIdentitySeq.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherIdentitySeq.lean
index f81882b4eb..5eb35caf8e 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherIdentitySeq.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherIdentitySeq.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Perturbation.GuntherIdentity
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Perturbation.GuntherOperator
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.CoeffTransport
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherIteration.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherIteration.lean
index 1ccd2b5818..17bd097144 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherIteration.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherIteration.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Perturbation.SeqVector
 
 /-!
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherOperator.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherOperator.lean
index 8403825bd8..3a927ec850 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherOperator.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/GuntherOperator.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Perturbation.GuntherIteration
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.ConvolutionAlgebra
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.MultiplicationBootstrap
@@ -108,12 +108,9 @@ lemma vecNormSq_mul_le_top {r k : ℕ} (hk : r ≤ k) {v w : VecSeq n N}
     (hv : VMem n N k v) :
     vecNormSq n N r v * vecNormSq n N r w ≤ top n N r k v w := by
   unfold top
-  have hrk : ((r : ℕ) : ℝ) ≤ ((k : ℕ) : ℝ) := by exact_mod_cast hk
-  have hvm : vecNormSq n N r v ≤ vecNormSq n N k v := vecNormSq_mono hv hrk
-  have hv0 : 0 ≤ vecNormSq n N ((r : ℕ) : ℝ) v := vecNormSq_nonneg _ _
-  have hw0 : 0 ≤ vecNormSq n N ((r : ℕ) : ℝ) w := vecNormSq_nonneg _ _
-  have hwk : 0 ≤ vecNormSq n N ((k : ℕ) : ℝ) w := vecNormSq_nonneg _ _
-  nlinarith
+  exact (mul_le_mul_of_nonneg_right (vecNormSq_mono hv (by exact_mod_cast hk))
+    (vecNormSq_nonneg _ _)).trans
+      (le_add_of_nonneg_right (mul_nonneg (vecNormSq_nonneg _ _) (vecNormSq_nonneg _ _)))
 
 /-- Monotonicity of the lower bucket in `k` (for `r ≤ k`). -/
 lemma lower_mono {r k : ℕ} {v w : VecSeq n N}
@@ -121,7 +118,7 @@ lemma lower_mono {r k : ℕ} {v w : VecSeq n N}
     lower n N r k v w ≤ lower n N r (k + 1) v w := by
   unfold lower
   simp only [Nat.add_sub_cancel]
-  have hkk : ((k : ℕ) : ℝ) ≤ ((k + 1 : ℕ) : ℝ) := by push_cast; linarith
+  have hkk : ((k : ℕ) : ℝ) ≤ ((k + 1 : ℕ) : ℝ) := by exact_mod_cast Nat.le_succ k
   have hvk : VMem n N ((k : ℕ) : ℝ) v := hv.mono hkk
   have hwk : VMem n N ((k : ℕ) : ℝ) w := hw.mono hkk
   have hsub : ((k - 1 : ℕ) : ℝ) ≤ ((k : ℕ) : ℝ) := by exact_mod_cast Nat.sub_le k 1
@@ -131,16 +128,15 @@ lemma lower_mono {r k : ℕ} {v w : VecSeq n N}
     vecNormSq_mono hwk hsub
   have hv0 : 0 ≤ vecNormSq n N ((r : ℕ) : ℝ) v := vecNormSq_nonneg _ _
   have hw0 : 0 ≤ vecNormSq n N ((r : ℕ) : ℝ) w := vecNormSq_nonneg _ _
-  nlinarith
+  exact add_le_add (add_le_add (mul_le_mul_of_nonneg_right hv1 hw0)
+    (mul_le_mul_of_nonneg_left hw1 hv0)) le_rfl
 
 /-- `top_k ≤ lower_{k+1}`. -/
 lemma top_le_lower_succ (r k : ℕ) (v w : VecSeq n N) :
     top n N r k v w ≤ lower n N r (k + 1) v w := by
   unfold top lower
   simp only [Nat.add_sub_cancel]
-  have hv0 : 0 ≤ vecNormSq n N ((r : ℕ) : ℝ) v := vecNormSq_nonneg _ _
-  have hw0 : 0 ≤ vecNormSq n N ((r : ℕ) : ℝ) w := vecNormSq_nonneg _ _
-  nlinarith
+  exact le_add_of_nonneg_right (mul_nonneg (vecNormSq_nonneg _ _) (vecNormSq_nonneg _ _))
 
 /-! ## Derivative operators -/
 
@@ -444,12 +440,13 @@ theorem ScalarTame.smulSeq (hn : 0 < n) {r : ℕ} (hr : 1 + (n : ℝ) / 2 < r)
     VecTame n N r (fun v w => smulSeq (Q v w) a) (smulTopConst n N r a A')
       (smulLowConst n N r a A' Bk) := by
   have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
-  have hr1 : (1 : ℝ) < (r : ℝ) := by linarith
-  have h2r : (n : ℝ) < 2 * (r : ℝ) := by linarith
+  have hr1 : (1 : ℝ) < (r : ℝ) := by linarith only [hr, hn1]
+  have h2r : (n : ℝ) < 2 * (r : ℝ) := by linarith only [hr]
   have hA3 : 0 ≤ mt3AConstSq n (r : ℝ) := by
     have h0 : (0 : ℝ) ≤ mt3KSq n (r : ℝ) := by
       unfold mt3KSq; exact tsum_nonneg fun j => weight_nonneg _ _
-    unfold mt3AConstSq; linarith
+    unfold mt3AConstSq
+    linarith only [h0]
   have hB3 : ∀ j : ℕ, 0 ≤ mt3BConstSq n j (r : ℝ) := by
     intro j
     have hL : (0 : ℝ) ≤ mt3LSq n (r : ℝ) := by
@@ -468,11 +465,7 @@ theorem ScalarTame.smulSeq (hn : 0 < n) {r : ℕ} (hr : 1 + (n : ℝ) / 2 < r)
     refine mul_nonneg (mul_nonneg (add_nonneg hA3 (hB3 k)) ?_) ?_
     · exact add_nonneg (add_nonneg (vecNormSq_nonneg _ _) (vecNormSq_nonneg _ _))
         (vecNormSq_nonneg _ _)
-    · have h1 := h.Bk_nonneg k
-      have h2 := h.Bk_nonneg (k - 1)
-      have h3 := h.Bk_nonneg r
-      have h4 := h.A'_nonneg
-      linarith
+    · linarith only [h.Bk_nonneg k, h.Bk_nonneg (k - 1), h.Bk_nonneg r, h.A'_nonneg]
   · intro k hk v w hv hw α
     exact (third_multiplication_theorem_seq hn hr (by exact_mod_cast hk)
       (h.mem k hk v w hv hw) (ha k α)).1
@@ -497,7 +490,7 @@ theorem ScalarTame.smulSeq (hn : 0 < n) {r : ℕ} (hr : 1 + (n : ℝ) / 2 < r)
       have p2 : 0 ≤ vecNormSq n N (r : ℝ) v * vecNormSq n N ((k - 1 : ℕ) : ℝ) w :=
         mul_nonneg (vecNormSq_nonneg _ _) (vecNormSq_nonneg _ _)
       unfold lower
-      linarith
+      exact le_add_of_nonneg_left (add_nonneg p1 p2)
     have hQr : sobolevNormSq n (r : ℝ) (Q v w)
         ≤ (2 * A' + 3 * Bk r) * lower n N r k v w := by
       have hbr := h.bound r le_rfl v w hvr hwr
@@ -512,12 +505,13 @@ theorem ScalarTame.smulSeq (hn : 0 < n) {r : ℕ} (hr : 1 + (n : ℝ) / 2 < r)
         have p1 := vecNormSq_nonneg (n := n) (N := N) (r : ℝ) v
         have p2 := vecNormSq_nonneg (n := n) (N := N) (r : ℝ) w
         unfold lower
-        nlinarith
+        linarith only [mul_le_mul_of_nonneg_right e1 p2,
+          mul_le_mul_of_nonneg_left e2 p1]
       rw [htr] at hbr
       have hstep : sobolevNormSq n (r : ℝ) (Q v w)
           ≤ (2 * A' + 3 * Bk r) * (vecNormSq n N (r : ℝ) v * vecNormSq n N (r : ℝ) w) := by
-        nlinarith [mul_le_mul_of_nonneg_left hlr hBr]
-      exact hstep.trans (mul_le_mul_of_nonneg_left hXlow (by linarith))
+        linarith only [hbr, mul_le_mul_of_nonneg_left hlr hBr]
+      exact hstep.trans (mul_le_mul_of_nonneg_left hXlow (by linarith only [hA'0, hBr]))
     have hQk1 : sobolevNormSq n ((k - 1 : ℕ) : ℝ) (Q v w)
         ≤ (Bk (k - 1) + 3 * A' + 3 * Bk r) * lower n N r k v w := by
       rcases eq_or_lt_of_le hk with heq | hlt
@@ -527,8 +521,8 @@ theorem ScalarTame.smulSeq (hn : 0 < n) {r : ℕ} (hr : 1 + (n : ℝ) / 2 < r)
           have : (k - 1 : ℕ) ≤ r := by omega
           exact_mod_cast this
         have hextra : 0 ≤ (Bk (k - 1) + A') * lower n N r k v w :=
-          mul_nonneg (by linarith) hlow0
-        nlinarith [hmono, hQr, hextra]
+          mul_nonneg (by linarith only [hBk1, hA'0]) hlow0
+        linarith only [hmono, hQr, hextra]
       · have hkr1 : r ≤ k - 1 := by omega
         have hsucc : k - 1 + 1 = k := by omega
         have hvk1 : VMem n N ((k - 1 : ℕ) : ℝ) v :=
@@ -544,8 +538,10 @@ theorem ScalarTame.smulSeq (hn : 0 < n) {r : ℕ} (hr : 1 + (n : ℝ) / 2 < r)
           have hw' : VMem n N ((k - 1 + 1 : ℕ) : ℝ) w := by rw [hsucc]; exact hw
           have hl := lower_mono (n := n) (N := N) (r := r) hv' hw'
           rwa [hsucc] at hl
-        nlinarith [mul_le_mul_of_nonneg_left htl hA'0, mul_le_mul_of_nonneg_left hll hBk1,
-          mul_nonneg (show (0 : ℝ) ≤ 2 * A' + 3 * Bk r by linarith) hlow0]
+        linarith only [hb1, mul_le_mul_of_nonneg_left htl hA'0,
+          mul_le_mul_of_nonneg_left hll hBk1,
+          mul_nonneg (show (0 : ℝ) ≤ 2 * A' + 3 * Bk r by
+            linarith only [hA'0, hBr]) hlow0]
     have hper : ∀ α : Fin N, sobolevNormSq n (k : ℝ) (seqConv (Q v w) (a α)) ≤
         mt3AConstSq n (r : ℝ) * (sobolevNormSq n (k : ℝ) (Q v w) * sobolevNormSq n (r : ℝ) (a α)
           + sobolevNormSq n (r : ℝ) (Q v w) * sobolevNormSq n (k : ℝ) (a α))
@@ -592,12 +588,14 @@ theorem ScalarTame.smulSeq (hn : 0 < n) {r : ℕ} (hr : 1 + (n : ℝ) / 2 < r)
         ≤ mt3BConstSq n k (r : ℝ) * vecNormSq n N ((k - 1 : ℕ) : ℝ) a
             * ((2 * A' + 3 * Bk r) * lower n N r k v w) :=
       mul_le_mul_of_nonneg_left hQr (mul_nonneg hB3k hak1)
-    have hF1 : (0 : ℝ) ≤ (Bk k + Bk (k - 1) + 3 * A' + 3 * Bk r + 1) - Bk k := by linarith
+    have hF1 : (0 : ℝ) ≤ (Bk k + Bk (k - 1) + 3 * A' + 3 * Bk r + 1) - Bk k := by
+      linarith only [hBk1, hA'0, hBr]
     have hF2 : (0 : ℝ) ≤ (Bk k + Bk (k - 1) + 3 * A' + 3 * Bk r + 1)
-        - (Bk (k - 1) + 3 * A' + 3 * Bk r) := by linarith
+        - (Bk (k - 1) + 3 * A' + 3 * Bk r) := by linarith only [hBkk]
     have hF3 : (0 : ℝ) ≤ (Bk k + Bk (k - 1) + 3 * A' + 3 * Bk r + 1)
-        - (2 * A' + 3 * Bk r) := by linarith
-    have hF0 : (0 : ℝ) ≤ Bk k + Bk (k - 1) + 3 * A' + 3 * Bk r + 1 := by linarith
+        - (2 * A' + 3 * Bk r) := by linarith only [hBkk, hBk1, hA'0]
+    have hF0 : (0 : ℝ) ≤ Bk k + Bk (k - 1) + 3 * A' + 3 * Bk r + 1 := by
+      linarith only [hBkk, hBk1, hA'0, hBr]
     have hP : 0 ≤ mt3AConstSq n (r : ℝ) * vecNormSq n N (r : ℝ) a := mul_nonneg hA3 har
     have hR : 0 ≤ mt3BConstSq n k (r : ℝ) * vecNormSq n N (r : ℝ) a := mul_nonneg hB3k har
     have hS : 0 ≤ mt3AConstSq n (r : ℝ) * vecNormSq n N (k : ℝ) a := mul_nonneg hA3 hak
@@ -654,7 +652,7 @@ private theorem resolvent_dotConv_estimate (hn : 0 < n) {r : ℕ} (hr : 1 + (n :
           ≤ baseTopConst n N r * top n N r k v w
             + baseLowConst n N r k * lower n N r k v w := by
   have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
-  have hrR : (3 : ℝ) < (r : ℝ) := by linarith
+  have hrR : (3 : ℝ) < (r : ℝ) := by linarith only [hr, hn1]
   have hr4 : 4 ≤ r := by
     have h3 : 3 < r := by exact_mod_cast hrR
     omega
@@ -663,7 +661,7 @@ private theorem resolvent_dotConv_estimate (hn : 0 < n) {r : ℕ} (hr : 1 + (n :
   have hA3 : 0 ≤ mt3AConstSq n ((r : ℝ) - 2) := by
     have h0 : (0 : ℝ) ≤ mt3KSq n ((r : ℝ) - 2) := by
       unfold mt3KSq; exact tsum_nonneg fun j => weight_nonneg _ _
-    unfold mt3AConstSq; linarith
+    unfold mt3AConstSq; linarith only [h0]
   have hB3 : ∀ j : ℕ, 0 ≤ mt3BConstSq n j ((r : ℝ) - 2) := by
     intro j
     have hL : (0 : ℝ) ≤ mt3LSq n ((r : ℝ) - 2) := by
@@ -690,39 +688,41 @@ private theorem resolvent_dotConv_estimate (hn : 0 < n) {r : ℕ} (hr : 1 + (n :
   have hkm1 : ((k - 1 : ℕ) : ℝ) = (k : ℝ) - 1 := by
     have h1 : (1 : ℕ) ≤ k := by omega
     rw [Nat.cast_sub h1]; norm_num
-  have hvk1 : VMem n N ((k - 1 : ℕ) : ℝ) v := hv.mono (by rw [hkm1]; linarith)
-  have hwk1 : VMem n N ((k - 1 : ℕ) : ℝ) w := hw.mono (by rw [hkm1]; linarith)
+  have hvk1 : VMem n N ((k - 1 : ℕ) : ℝ) v := hv.mono (by rw [hkm1]; linarith only [])
+  have hwk1 : VMem n N ((k - 1 : ℕ) : ℝ) w := hw.mono (by rw [hkm1]; linarith only [])
   have hvr : VMem n N (r : ℝ) v := hv.mono hkR
   have hwr : VMem n N (r : ℝ) w := hw.mono hkR
   -- level `k - 2`
-  have hv_j : VMem n N (((k - 2 : ℕ) : ℝ) + (d₁ : ℝ)) v := hv.mono (by rw [hs]; linarith)
-  have hw_j : VMem n N (((k - 2 : ℕ) : ℝ) + (d₂ : ℝ)) w := hw.mono (by rw [hs]; linarith)
+  have hv_j : VMem n N (((k - 2 : ℕ) : ℝ) + (d₁ : ℝ)) v :=
+    hv.mono (by rw [hs]; linarith only [hd1R])
+  have hw_j : VMem n N (((k - 2 : ℕ) : ℝ) + (d₂ : ℝ)) w :=
+    hw.mono (by rw [hs]; linarith only [hd2R])
   have hD1j : VMem n N ((k - 2 : ℕ) : ℝ) (D₁ v) := h₁.mem _ v hv_j
   have hD2j : VMem n N ((k - 2 : ℕ) : ℝ) (D₂ w) := h₂.mem _ w hw_j
   have nD1j : vecNormSq n N ((k - 2 : ℕ) : ℝ) (D₁ v) ≤ vecNormSq n N (k : ℝ) v :=
-    le_trans (h₁.bound _ v hv_j) (vecNormSq_mono hv (by rw [hs]; linarith))
+    le_trans (h₁.bound _ v hv_j) (vecNormSq_mono hv (by rw [hs]; linarith only [hd1R]))
   have nD2j : vecNormSq n N ((k - 2 : ℕ) : ℝ) (D₂ w) ≤ vecNormSq n N (k : ℝ) w :=
-    le_trans (h₂.bound _ w hw_j) (vecNormSq_mono hw (by rw [hs]; linarith))
+    le_trans (h₂.bound _ w hw_j) (vecNormSq_mono hw (by rw [hs]; linarith only [hd2R]))
   -- level `r - 2`
-  have hv_r2 : VMem n N (((r : ℝ) - 2) + (d₁ : ℝ)) v := hv.mono (by linarith)
-  have hw_r2 : VMem n N (((r : ℝ) - 2) + (d₂ : ℝ)) w := hw.mono (by linarith)
+  have hv_r2 : VMem n N (((r : ℝ) - 2) + (d₁ : ℝ)) v := hv.mono (by linarith only [hd1R, hkR])
+  have hw_r2 : VMem n N (((r : ℝ) - 2) + (d₂ : ℝ)) w := hw.mono (by linarith only [hd2R, hkR])
   have nD1r2 : vecNormSq n N ((r : ℝ) - 2) (D₁ v) ≤ vecNormSq n N (r : ℝ) v :=
-    le_trans (h₁.bound _ v hv_r2) (vecNormSq_mono hvr (by linarith))
+    le_trans (h₁.bound _ v hv_r2) (vecNormSq_mono hvr (by linarith only [hd1R]))
   have nD2r2 : vecNormSq n N ((r : ℝ) - 2) (D₂ w) ≤ vecNormSq n N (r : ℝ) w :=
-    le_trans (h₂.bound _ w hw_r2) (vecNormSq_mono hwr (by linarith))
+    le_trans (h₂.bound _ w hw_r2) (vecNormSq_mono hwr (by linarith only [hd2R]))
   -- level `k - 3`
   have hv_s1 : VMem n N ((((k - 2 : ℕ) : ℝ) - 1) + (d₁ : ℝ)) v :=
-    hv.mono (by rw [hs]; linarith)
+    hv.mono (by rw [hs]; linarith only [hd1R])
   have hw_s1 : VMem n N ((((k - 2 : ℕ) : ℝ) - 1) + (d₂ : ℝ)) w :=
-    hw.mono (by rw [hs]; linarith)
+    hw.mono (by rw [hs]; linarith only [hd2R])
   have nD1s1 : vecNormSq n N (((k - 2 : ℕ) : ℝ) - 1) (D₁ v)
       ≤ vecNormSq n N ((k - 1 : ℕ) : ℝ) v :=
-    le_trans (h₁.bound _ v hv_s1) (vecNormSq_mono hvk1 (by rw [hs, hkm1]; linarith))
+    le_trans (h₁.bound _ v hv_s1) (vecNormSq_mono hvk1 (by rw [hs, hkm1]; linarith only [hd1R]))
   have nD2s1 : vecNormSq n N (((k - 2 : ℕ) : ℝ) - 1) (D₂ w)
       ≤ vecNormSq n N ((k - 1 : ℕ) : ℝ) w :=
-    le_trans (h₂.bound _ w hw_s1) (vecNormSq_mono hwk1 (by rw [hs, hkm1]; linarith))
+    le_trans (h₂.bound _ w hw_s1) (vecNormSq_mono hwk1 (by rw [hs, hkm1]; linarith only [hd2R]))
   -- the multiplication theorem, componentwise
-  have hkr2 : (r : ℝ) - 2 ≤ ((k - 2 : ℕ) : ℝ) := by rw [hs]; linarith
+  have hkr2 : (r : ℝ) - 2 ≤ ((k - 2 : ℕ) : ℝ) := by rw [hs]; linarith only [hkR]
   have mt : ∀ α : Fin N,
       MemSobolev n ((k - 2 : ℕ) : ℝ) (seqConv (D₁ v α) (D₂ w α))
       ∧ sobolevNormSq n ((k - 2 : ℕ) : ℝ) (seqConv (D₁ v α) (D₂ w α))
@@ -820,7 +820,7 @@ private theorem resolvent_dotConv_estimate (hn : 0 < n) {r : ℕ} (hr : 1 + (n :
         ≤ mt3AConstSq n ((r : ℝ) - 2) * top n N r k v w := by
       refine mul_le_mul_of_nonneg_left ?_ hA3
       unfold top
-      linarith
+      exact add_le_add p12 p34
     have hBb : mt3BConstSq n (k - 2) ((r : ℝ) - 2)
           * ((∑ α, sobolevNormSq n (((k - 2 : ℕ) : ℝ) - 1) (D₁ v α)
                 * sobolevNormSq n ((r : ℝ) - 2) (D₂ w α))
@@ -831,8 +831,8 @@ private theorem resolvent_dotConv_estimate (hn : 0 < n) {r : ℕ} (hr : 1 + (n :
       have hnn : 0 ≤ vecNormSq n N (r : ℝ) v * vecNormSq n N (r : ℝ) w :=
         mul_nonneg (vecNormSq_nonneg _ _) (vecNormSq_nonneg _ _)
       unfold lower
-      linarith
-    linarith [step1, step2.le, step2.ge, hA, hBb]
+      exact (add_le_add p52 p36).trans (le_add_of_nonneg_right hnn)
+    linarith only [step1, step2.le, step2.ge, hA, hBb]
   calc sobolevNormSq n (k : ℝ) (resolventCoeff (dotConv (D₁ v) (D₂ w)))
       = sobolevNormSq n ((k - 2 : ℕ) : ℝ) (dotConv (D₁ v) (D₂ w)) := hres_norm
     _ ≤ (N : ℝ) * ∑ α, sobolevNormSq n ((k - 2 : ℕ) : ℝ) (seqConv (D₁ v α) (D₂ w α)) := hsum1
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/Main.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/Main.lean
index 47494b53c5..18495a718e 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/Main.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/Main.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Perturbation.DualFrame
 public import LeanPool.NashEmbedding.NashEmbedding.Torus.Perturbation.GuntherIdentitySeq
 
diff --git a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/SeqVector.lean b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/SeqVector.lean
index ee6d429f25..fc2fd9dab8 100644
--- a/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/SeqVector.lean
+++ b/LeanPool/NashEmbedding/NashEmbedding/Torus/Perturbation/SeqVector.lean
@@ -12,7 +12,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aristotle (Harmonic), Claude Fable 5 (Anthropic), Claude Opus 4.7 (Anthropic)
   — at the request of David Wiygul
 -/
-public import Mathlib.Tactic
+public import LeanPool.NashEmbedding.Tactics
 public import LeanPool.NashEmbedding.NashEmbedding.Sobolev.Limits
 
 /-!
diff --git a/LeanPool/NashEmbedding/Tactics.lean b/LeanPool/NashEmbedding/Tactics.lean
new file mode 100644
index 0000000000..5c8106c2b7
--- /dev/null
+++ b/LeanPool/NashEmbedding/Tactics.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Lean Pool contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Pool contributors
+-/
+module -- shake: keep-all
+
+public import Aesop
+public import Mathlib.Tactic.Abel
+public import Mathlib.Tactic.ApplyCongr
+public import Mathlib.Tactic.CongrExclamation
+public import Mathlib.Tactic.Continuity
+public import Mathlib.Tactic.Convert
+public import Mathlib.Tactic.FieldSimp
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.FunProp
+public import Mathlib.Tactic.GCongr
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.LinearCombination
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Positivity
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.Ring
+public import Mathlib.Tactic.Tauto
+
+/-!
+# Tactics for the Nash embedding development
+
+Keep the tactic plugins together so individual proof modules avoid loading the full tactic library.
+-/