diff --git a/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/AffineModes.lean b/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/AffineModes.lean
index d9a2f54128..621340dd66 100644
--- a/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/AffineModes.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/AffineModes.lean
@@ -5,10 +5,8 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.Analysis.FourthOrderODE.SmoothKernel
 public import Mathlib.Analysis.Complex.RealDeriv
-public import Mathlib.Tactic
 
 /-!
 # Explicit affine zero modes of the free--free beam
diff --git a/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/ComplexGreenIdentity.lean b/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/ComplexGreenIdentity.lean
index f42d200b97..a164a38309 100644
--- a/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/ComplexGreenIdentity.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/ComplexGreenIdentity.lean
@@ -5,12 +5,11 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
 public import Mathlib.Analysis.Calculus.Deriv.Mul
 public import Mathlib.Analysis.Calculus.Deriv.Star
 public import Mathlib.Analysis.Complex.Basic
-public import Mathlib.Tactic
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-!
 # Complex smooth-core Green identities for the free--free beam
diff --git a/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/SmoothGreenIdentity.lean b/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/SmoothGreenIdentity.lean
index 316fe99539..5148d15666 100644
--- a/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/SmoothGreenIdentity.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/SmoothGreenIdentity.lean
@@ -5,10 +5,10 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
 public import Mathlib.Analysis.Calculus.Deriv.Mul
-public import Mathlib.Tactic
+import Mathlib.Tactic.Linarith -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-!
 # Smooth-core Green identities for the free--free beam
diff --git a/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/SmoothKernel.lean b/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/SmoothKernel.lean
index f740f6abcc..ae8aac5787 100644
--- a/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/SmoothKernel.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Analysis/FourthOrderODE/SmoothKernel.lean
@@ -5,11 +5,11 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.Analysis.FourthOrderODE.SmoothGreenIdentity
 public import LeanPool.DavisKahan.DavisKahan.Analysis.FourthOrderODE.ComplexGreenIdentity
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
-public import Mathlib.Tactic
+import Mathlib.Tactic.Abel -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-!
 # The smooth kernel of the free--free fourth derivative
diff --git a/LeanPool/DavisKahan/DavisKahan/FiniteDimensional/DoubleAngle/TanTheta.lean b/LeanPool/DavisKahan/DavisKahan/FiniteDimensional/DoubleAngle/TanTheta.lean
index 2f4a0c25a8..7995bbb49d 100644
--- a/LeanPool/DavisKahan/DavisKahan/FiniteDimensional/DoubleAngle/TanTheta.lean
+++ b/LeanPool/DavisKahan/DavisKahan/FiniteDimensional/DoubleAngle/TanTheta.lean
@@ -345,14 +345,14 @@ theorem eigenvalue_notMem_gap_of_diagonal_form (hS : S.IsSymmetric)
     have hle := hUa x hxU
     rw [hval x, inner_self_eq_norm_sq] at hle
     have hxpos : (0 : ℝ) < ‖x‖ ^ 2 := pow_pos (norm_pos_iff.mpr hx) 2
-    nlinarith [hle, hxpos]
+    nlinarith only [hle, hxpos, hle, hxpos]
   rcases eq_or_ne m 0 with hm0 | hm0n
   · right
     have hxU : x ∈ U := by rw [hsplit, hm0, add_zero]; exact hpU
     have hle := hUb x hxU
     rw [hval x, inner_self_eq_norm_sq] at hle
     have hxpos : (0 : ℝ) < ‖x‖ ^ 2 := pow_pos (norm_pos_iff.mpr hx) 2
-    nlinarith [hle, hxpos]
+    nlinarith only [hle, hxpos, hle, hxpos]
   -- Both blocks nonzero.
   have hp2 : (0 : ℝ) < ‖p‖ ^ 2 := pow_pos (norm_pos_iff.mpr hp0n) 2
   have hq2 : (0 : ℝ) < ‖m‖ ^ 2 := pow_pos (norm_pos_iff.mpr hm0n) 2
@@ -377,9 +377,9 @@ theorem eigenvalue_notMem_gap_of_diagonal_form (hS : S.IsSymmetric)
   have heq_m : μ * ‖m‖ ^ 2 = RCLike.re ⟪S p, m⟫_𝕜 + RCLike.re ⟪S m, m⟫_𝕜 := by
     rw [← decomp_m, hval_m]
   have hr_le : RCLike.re ⟪S p, m⟫_𝕜 ≤ (μ - b) * ‖p‖ ^ 2 := by
-    nlinarith [hUb p hpU, heq_p]
+    nlinarith only [hUb, hpU, hval_p, decomp_p, hUb p hpU, heq_p]
   have hr_ge : (μ - a) * ‖m‖ ^ 2 ≤ RCLike.re ⟪S p, m⟫_𝕜 := by
-    nlinarith [hUa m hmU, heq_m]
+    nlinarith only [hUa, hmU, hval_m, decomp_m, hUa m hmU, heq_m]
   by_contra hc
   push Not at hc
   nlinarith [hr_le, hr_ge, mul_pos (show (0 : ℝ) < μ - a by linarith [hc.1]) hq2,
@@ -1068,7 +1068,7 @@ theorem tan_two_theta_norm_sub_le (hT : T.IsSymmetric) (hS : S.IsSymmetric)
       have h0 : (0:ℝ) ≤ 2 * ε * (1 - 2 * (0:ℝ) ^ 2) := by
         norm_num
         positivity
-      nlinarith [h0]
+      nlinarith only [hε0, h0]
   · -- spectral apparatus for `Y := X ∘ X`
     have hXsym' : ∀ v w, ⟪X v, w⟫_𝕜 = ⟪v, X w⟫_𝕜 := by
       intro v w
diff --git a/LeanPool/DavisKahan/DavisKahan/FiniteDimensional/Sharpness.lean b/LeanPool/DavisKahan/DavisKahan/FiniteDimensional/Sharpness.lean
index f473147b21..35d8f91855 100644
--- a/LeanPool/DavisKahan/DavisKahan/FiniteDimensional/Sharpness.lean
+++ b/LeanPool/DavisKahan/DavisKahan/FiniteDimensional/Sharpness.lean
@@ -5,6 +5,8 @@ Authors: Jon Crall, GPT 5.6 High
 -/
 module
 
+import Mathlib.Analysis.Matrix.Hermitian
+
 public import LeanPool.DavisKahan.DavisKahan.Sources.Davis1963.RotationEnergy
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.AngleGeometry
 public import LeanPool.DavisKahan.DavisKahan.FiniteDimensional.Core.AngleOperatorBlockSum
@@ -490,8 +492,6 @@ private theorem modelSinThetaPerturbation_sq (a b θ : ℝ) :
       | linear_combination ((((b : 𝕜) - (a : 𝕜)) ^ 2 *
           ((Real.sin θ : 𝕜)) ^ 2 * x.ofLp 1) * hpy)
 
--- Elaboration got slower across the Mathlib bump and this proof no longer fits the default
--- budget.  Raised to the same level the three declarations lower in this file already use.
 private theorem singularValues_sinThetaMap_model
     {θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ Real.pi / 2) :
     (sinThetaMap (modelSubspace (𝕜 := 𝕜))
@@ -502,32 +502,28 @@ private theorem singularValues_sinThetaMap_model
     have h := congrArg (fun r : ℝ => (r : 𝕜)) (Real.sin_sq_add_cos_sq θ)
     push_cast at h
     exact h
-  rw [sinThetaMap_model_eq_matrix]
-  apply singularValues_eq_pair_of_gram_eq finrank_euclideanSpace_fin
-    (EuclideanSpace.basisFun (Fin 2) 𝕜) _ hsin (by norm_num) hsin
-  -- compute the adjoint as a matrix; `adjoint_inner_left` cannot reduce an
-  -- adjoint *composition* into matrix form
-  have hadj : (Matrix.toEuclideanLin
-      !![((Real.sin θ ^ 2 : ℝ) : 𝕜), 0;
-         ((-Real.sin θ * Real.cos θ : ℝ) : 𝕜), 0]).adjoint =
-      Matrix.toEuclideanLin
-      !![((Real.sin θ ^ 2 : ℝ) : 𝕜), ((-Real.sin θ * Real.cos θ : ℝ) : 𝕜);
-         0, 0] := by
-    rw [← Matrix.toEuclideanLin_conjTranspose_eq_adjoint]
-    congr 1
+  let A : Matrix (Fin 2) (Fin 2) 𝕜 :=
+    !![((Real.sin θ ^ 2 : ℝ) : 𝕜), 0; ((-Real.sin θ * Real.cos θ : ℝ) : 𝕜), 0]
+  let B : Matrix (Fin 2) (Fin 2) 𝕜 := !![0, 0; (Real.sin θ : 𝕜), 0]
+  have hmatrix : A.conjTranspose * A = B.conjTranspose * B := by
     ext i j
     fin_cases i <;> fin_cases j <;>
-      simp [Matrix.conjTranspose_apply, RCLike.conj_ofReal]
-  rw [hadj]
-  refine (EuclideanSpace.basisFun (Fin 2) 𝕜).toBasis.ext fun i => ?_
-  rw [OrthonormalBasis.coe_toBasis]
-  fin_cases i <;>
-    rw [diagOp_apply_basis] <;>
-    ext j <;> fin_cases j <;>
-    simp [LinearMap.comp_apply, Matrix.toLpLin_apply,
-      Matrix.vecHead, Matrix.vecTail, EuclideanSpace.basisFun_apply]
-  ring_nf
-  linear_combination (((Real.sin θ : 𝕜)) ^ 2) * hpy
+      simp [A, B, Matrix.mul_apply, Fin.sum_univ_two,
+        Matrix.conjTranspose_apply, RCLike.conj_ofReal]
+    linear_combination ((Real.sin θ : 𝕜) ^ 2) * hpy
+  have hgram : (Matrix.toEuclideanLin A).adjoint ∘ₗ Matrix.toEuclideanLin A =
+      (Matrix.toEuclideanLin B).adjoint ∘ₗ Matrix.toEuclideanLin B := by
+    rw [← Matrix.toEuclideanLin_conjTranspose_eq_adjoint,
+      ← Matrix.toEuclideanLin_conjTranspose_eq_adjoint]
+    simpa only [Matrix.toLpLin_mul_same] using
+      congrArg (Matrix.toLpLin 2 2) hmatrix
+  rw [sinThetaMap_model_eq_matrix]
+  calc
+    (Matrix.toEuclideanLin A).singularValues = (Matrix.toEuclideanLin B).singularValues :=
+      singularValues_eq_of_gram_eq hgram
+    _ = pairSingularValues (Real.sin θ) 0 := by
+      simpa only [B, abs_of_nonneg hsin] using
+        singularValues_lowerLeft_two_by_two (𝕜 := 𝕜) (Real.sin θ)
 
 private theorem singularValues_projection_sub_model
     {θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ Real.pi / 2) :
diff --git a/LeanPool/DavisKahan/DavisKahan/Geometry/Angle/OperatorAngleComplex.lean b/LeanPool/DavisKahan/DavisKahan/Geometry/Angle/OperatorAngleComplex.lean
index b1f1521de8..79980699b7 100644
--- a/LeanPool/DavisKahan/DavisKahan/Geometry/Angle/OperatorAngleComplex.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Geometry/Angle/OperatorAngleComplex.lean
@@ -555,7 +555,7 @@ theorem norm_cosAngleExtendedC_apply_ge (U V : Submodule ℂ E)
         (mul_nonneg hc0 (norm_nonneg _)) hlow1
       rw [sq, sq]
       exact h
-    have h2 : c ^ 2 ≤ 1 := by nlinarith
+    have h2 : c ^ 2 ≤ 1 := by nlinarith only [hc0, hc1]
     have hb2 : (0:ℝ) ≤ ‖Uᗮ.starProjection x‖ ^ 2 := sq_nonneg _
     nlinarith [h1, h2, hb2, hsq2, sq_nonneg ‖x‖,
       sq_nonneg ‖U.starProjection x‖]
@@ -588,7 +588,7 @@ theorem cosAngleExtendedC_ker_bot_range_top (U V : Submodule ℂ E)
     have hx0 : cosAngleExtendedC U V x = 0 := hx
     have h := hlow x
     rw [hx0, norm_zero] at h
-    have : ‖x‖ ≤ 0 := by nlinarith
+    have : ‖x‖ ≤ 0 := by nlinarith only [hcpos, h]
     exact norm_eq_zero.mp (le_antisymm this (norm_nonneg x))
   refine ⟨hker, ?_⟩
   -- closed range from the antilipschitz bound
@@ -633,7 +633,7 @@ theorem cosAngleExtendedC_ker_bot_range_top (U V : Submodule ℂ E)
     exact inner_self_eq_zero.mp h
   have h := hlow y
   rw [hTy, norm_zero] at h
-  have : ‖y‖ ≤ 0 := by nlinarith
+  have : ‖y‖ ≤ 0 := by nlinarith only [hcpos, h]
   exact norm_eq_zero.mp (le_antisymm this (norm_nonneg y))
 
 /-- The extended cosine as a continuous linear equivalence, in the acute
@@ -683,7 +683,7 @@ theorem ker_bot_range_top_of_isSelfAdjoint_of_bounded_below
     have hx0 : T x = 0 := hx
     have h := hlow x
     rw [hx0, norm_zero] at h
-    have : ‖x‖ ≤ 0 := by nlinarith
+    have : ‖x‖ ≤ 0 := by nlinarith only [hcpos, h]
     exact norm_eq_zero.mp (le_antisymm this (norm_nonneg x))
   refine ⟨hker, ?_⟩
   have hanti : AntilipschitzWith (⟨c, hcpos.le⟩ : NNReal)⁻¹ T := by
@@ -719,7 +719,7 @@ theorem ker_bot_range_top_of_isSelfAdjoint_of_bounded_below
     exact inner_self_eq_zero.mp h
   have h := hlow y
   rw [hTy, norm_zero] at h
-  have : ‖y‖ ≤ 0 := by nlinarith
+  have : ‖y‖ ≤ 0 := by nlinarith only [hcpos, h]
   exact norm_eq_zero.mp (le_antisymm this (norm_nonneg y))
 
 omit [CompleteSpace E] in
@@ -767,7 +767,7 @@ theorem norm_add_starProjection_orthogonal_apply_ge
         (mul_nonneg hc0 (norm_nonneg _)) hlow1
       rw [sq, sq]
       exact h
-    have h2 : c ^ 2 ≤ 1 := by nlinarith
+    have h2 : c ^ 2 ≤ 1 := by nlinarith only [hc0, hc1]
     have hb2 : (0:ℝ) ≤ ‖Uᗮ.starProjection x‖ ^ 2 := sq_nonneg _
     nlinarith [h1, h2, hb2, hsq2, sq_nonneg ‖x‖,
       sq_nonneg ‖U.starProjection x‖]
diff --git a/LeanPool/DavisKahan/DavisKahan/InfiniteDimensional/Sylvester/Basic.lean b/LeanPool/DavisKahan/DavisKahan/InfiniteDimensional/Sylvester/Basic.lean
index 550c406c11..99968518f0 100644
--- a/LeanPool/DavisKahan/DavisKahan/InfiniteDimensional/Sylvester/Basic.lean
+++ b/LeanPool/DavisKahan/DavisKahan/InfiniteDimensional/Sylvester/Basic.lean
@@ -5,6 +5,8 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
+import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
+
 public import LeanPool.DavisKahan.DavisKahan.InfiniteDimensional.Ideals.Symmetric
 public import LeanPool.DavisKahan.DavisKahan.InfiniteDimensional.Ideals.CompactIntegral
 public import LeanPool.DavisKahan.DavisKahan.InfiniteDimensional.Sylvester.FourierSemigroup
diff --git a/LeanPool/DavisKahan/DavisKahan/Riccati/UnboundedAdjointRiccati.lean b/LeanPool/DavisKahan/DavisKahan/Riccati/UnboundedAdjointRiccati.lean
index fcdf1507f4..28cd5f1ad5 100644
--- a/LeanPool/DavisKahan/DavisKahan/Riccati/UnboundedAdjointRiccati.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Riccati/UnboundedAdjointRiccati.lean
@@ -1001,7 +1001,7 @@ theorem norm_riccatiGramCommutator_le
     refine (ContinuousLinearMap.opNorm_comp_le _ _).trans ?_
     have hc : ‖(ContinuousLinearMap.adjoint X) ∘L X‖ ≤ 1 := by
       refine (ContinuousLinearMap.opNorm_comp_le _ _).trans ?_
-      rw [hXa]; nlinarith
+      rw [hXa]; nlinarith only [hX, hX0]
     nlinarith [norm_nonneg (H.B01 ∘L X), norm_nonneg
       ((ContinuousLinearMap.adjoint X) ∘L X)]
   have h3 : ‖(ContinuousLinearMap.adjoint X) ∘L H.B10‖ ≤ ‖H.B10‖ := by
@@ -1012,7 +1012,7 @@ theorem norm_riccatiGramCommutator_le
     refine (ContinuousLinearMap.opNorm_comp_le _ _).trans ?_
     have hc : ‖(ContinuousLinearMap.adjoint X) ∘L X‖ ≤ 1 := by
       refine (ContinuousLinearMap.opNorm_comp_le _ _).trans ?_
-      rw [hXa]; nlinarith
+      rw [hXa]; nlinarith only [hX, hX0]
     nlinarith [norm_nonneg ((ContinuousLinearMap.adjoint X) ∘L H.B10),
       norm_nonneg ((ContinuousLinearMap.adjoint X) ∘L X)]
   refine (norm_sub_le _ _).trans ?_
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/DomainLimitation.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/DomainLimitation.lean
index de3b99847b..b68c4bab26 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/DomainLimitation.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/DomainLimitation.lean
@@ -348,7 +348,7 @@ theorem geometricTrial_hasSum_sq {μ : ℝ} (hμ0 : 0 ≤ μ) (hμ1 : μ < 1) :
     funext n
     rw [geometricTrial_apply, ← pow_mul, ← pow_mul, mul_comm]
   rw [h]
-  exact hasSum_geometric_of_lt_one (by positivity) (by nlinarith)
+  exact hasSum_geometric_of_lt_one (by positivity) (by nlinarith only [hμ0, hμ1])
 
 /-! ### The truncations repair the domain defect, and arbitrarily little is lost
 
@@ -372,7 +372,7 @@ theorem truncatedTrial_sub_geometricTrial_hasSum_sq {μ : ℝ} (hμ0 : 0 ≤ μ)
     HasSum (fun n =>
         ((truncatedTrial μ N - geometricTrial hμ0 hμ1 : DomainLimitationSpace) : ℕ → ℝ) n ^ 2)
       ((μ ^ 2) ^ N * (1 - μ ^ 2)⁻¹) := by
-  have hlt : μ ^ 2 < 1 := by nlinarith
+  have hlt : μ ^ 2 < 1 := by nlinarith only [hμ0, hμ1]
   have hnn : (0 : ℝ) ≤ μ ^ 2 := by positivity
   set d : ℕ → ℝ := fun n => if n < N then 0 else (μ ^ 2) ^ n with hd
   have hcoord : (fun n =>
@@ -400,7 +400,7 @@ theorem truncatedTrial_sub_geometricTrial_hasSum_sq {μ : ℝ} (hμ0 : 0 ≤ μ)
 theorem tendsto_norm_truncatedTrial_sub_geometricTrial {μ : ℝ} (hμ0 : 0 ≤ μ) (hμ1 : μ < 1) :
     Filter.Tendsto
       (fun N => ‖truncatedTrial μ N - geometricTrial hμ0 hμ1‖) Filter.atTop (nhds 0) := by
-  have hlt : μ ^ 2 < 1 := by nlinarith
+  have hlt : μ ^ 2 < 1 := by nlinarith only [hμ0, hμ1]
   have hnn : (0 : ℝ) ≤ μ ^ 2 := by positivity
   have hsq : ∀ N, ‖truncatedTrial μ N - geometricTrial hμ0 hμ1‖ ^ 2
       = (μ ^ 2) ^ N * (1 - μ ^ 2)⁻¹ := by
@@ -479,7 +479,7 @@ theorem geometricTrial_rayleighQuotient {μ : ℝ} (hμ0 : 0 < μ) (hμ1 : μ <
       / ‖geometricTrial hμ0.le hμ1‖ ^ 2 = 1 + μ := by
   have h1 : (1 : ℝ) - μ ≠ 0 := ne_of_gt (by linarith)
   rw [(geometricTrial_hasSum_form hμ0 hμ1).tsum_eq, geometricTrial_norm_sq hμ0.le hμ1]
-  have h2 : (1 : ℝ) - μ ^ 2 ≠ 0 := ne_of_gt (by nlinarith)
+  have h2 : (1 : ℝ) - μ ^ 2 ≠ 0 := ne_of_gt (by nlinarith only [hμ0, hμ1])
   field_simp
   ring
 
@@ -489,7 +489,7 @@ theorem geometricTrial_normalizedForm_apply {μ : ℝ} (hμ0 : 0 < μ) (hμ1 : 
         ((geometricTrial hμ0.le hμ1 : DomainLimitationSpace) : ℕ → ℝ) n ^ 2
       / ‖geometricTrial hμ0.le hμ1‖ ^ 2 = μ ^ n * (1 - μ ^ 2) := by
   have hne : μ ^ n ≠ 0 := ne_of_gt (pow_pos hμ0 n)
-  have h2 : (1 : ℝ) - μ ^ 2 ≠ 0 := ne_of_gt (by nlinarith)
+  have h2 : (1 : ℝ) - μ ^ 2 ≠ 0 := ne_of_gt (by nlinarith only [hμ0, hμ1])
   rw [geometricTrial_norm_sq hμ0.le hμ1, geometricTrial_apply, diagonalMultiplier]
   field_simp
 
@@ -610,7 +610,7 @@ vector and the first eigenvector. -/
 theorem sin_angle_geometricTrial {μ : ℝ} (hμ0 : 0 < μ) (hμ1 : μ < 1) :
     Real.sin (InnerProductGeometry.angle (geometricTrial hμ0.le hμ1)
         (firstEigenvector : DomainLimitationSpace)) = μ := by
-  have hpos : (0 : ℝ) ≤ 1 - μ ^ 2 := by nlinarith
+  have hpos : (0 : ℝ) ≤ 1 - μ ^ 2 := by nlinarith only [hμ0, hμ1]
   rw [Real.sin_eq_sqrt_one_sub_cos_sq (InnerProductGeometry.angle_nonneg _ _)
       (InnerProductGeometry.angle_le_pi _ _),
     cos_angle_geometricTrial hμ0 hμ1, Real.sq_sqrt hpos,
@@ -635,17 +635,17 @@ theorem geometricTrial_weinberger_sin_sq_le {μ αcheck₁ αcheck₂ : ℝ}
     Real.sin (InnerProductGeometry.angle (geometricTrial hμ0.le hμ1)
         (firstEigenvector : DomainLimitationSpace)) ^ 2
       ≤ (1 + μ - αcheck₁) / (αcheck₂ - αcheck₁) := by
-  have hsq : (0 : ℝ) ≤ 1 - μ ^ 2 := by nlinarith
+  have hsq : (0 : ℝ) ≤ 1 - μ ^ 2 := by nlinarith only [hμ0, hμ1]
   have hinvmul : μ⁻¹ * μ ^ 2 = μ := by
     field_simp
   have hhigh' : αcheck₂ * μ ^ 2 ≤ μ + μ ^ 2 := by
     have hstep : αcheck₂ * μ ^ 2 ≤ μ⁻¹ * μ ^ 2 :=
       mul_le_mul_of_nonneg_right hhigh (by positivity)
-    nlinarith [sq_nonneg μ]
+    nlinarith only [hinvmul, hstep, sq_nonneg μ]
   rw [sin_angle_geometricTrial hμ0 hμ1]
   exact weinberger_sine_sq_le_of_coupled_energy (s := μ) (alphaCheck := αcheck₁)
     (alphaHat := 1 + μ) (gamma := αcheck₂) (lowEnergy := 1 - μ ^ 2)
-    (highEnergy := μ + μ ^ 2) hgap (by ring) (by nlinarith) hhigh'
+    (highEnergy := μ + μ ^ 2) hgap (by ring) (by nlinarith only [hμ0, hμ1, hlow, hsq]) hhigh'
 
 /-- **The source's best-lower-bound simplification, squared.**  With
 `alphaCheck₁ = λ₁ = 1` and `alphaCheck₂ = λ₂ = μ⁻¹` the estimate reads `sin²θ ≤ μ²/(1-μ)`. -/
@@ -655,7 +655,7 @@ theorem geometricTrial_weinberger_best_sin_sq_le {μ : ℝ} (hμ0 : 0 < μ) (hμ
       ≤ μ ^ 2 / (1 - μ) := by
   have hmul : μ⁻¹ * μ = 1 := inv_mul_cancel₀ (ne_of_gt hμ0)
   have hinvpos : (0 : ℝ) < μ⁻¹ := inv_pos.mpr hμ0
-  have hinv : (1 : ℝ) < μ⁻¹ := by nlinarith
+  have hinv : (1 : ℝ) < μ⁻¹ := by nlinarith only [hμ0, hμ1, hmul]
   have h := geometricTrial_weinberger_sin_sq_le hμ0 hμ1 (αcheck₁ := 1) (αcheck₂ := μ⁻¹)
     le_rfl le_rfl hinv
   have h1 : (1 : ℝ) - μ ≠ 0 := ne_of_gt (by linarith)
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/ExactData.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/ExactData.lean
index b09899617d..fc7c532cc1 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/ExactData.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/ExactData.lean
@@ -126,7 +126,7 @@ lemma inv_sqrt_three_eq : (Real.sqrt 3)⁻¹ = Real.sqrt 3 / 3 := by
   have hn : Real.sqrt (3 : ℝ) ≠ 0 := ne_of_gt (Real.sqrt_pos.2 (by norm_num))
   apply (eq_div_iff (by norm_num : (3 : ℝ) ≠ 0)).2
   field_simp [hn]
-  nlinarith
+  nlinarith only [hs]
 
 /-- The two Ritz values sum to `ε`: the pair is centred on `ε / 2`. -/
 lemma ritzLow_add_ritzHigh (ε : ℝ) : ritzLow ε + ritzHigh ε = ε := by
@@ -203,7 +203,7 @@ lemma orthogonalResidualGram_nonzero_charAt (ε : ℝ) :
 /-- `√76 ≤ 11`.  This keeps `11 - √76` nonnegative, which is what makes the lower
 residual Gram eigenvalue nonnegative. -/
 lemma sqrt76_le_eleven : Real.sqrt 76 ≤ 11 := by
-  nlinarith [Real.sqrt_nonneg (76 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 76)]
+  nlinarith only [Real.sqrt_nonneg (76 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 76)]
 
 /-- The lower residual Gram eigenvalue is nonnegative, so it is the square of a real
 singular value. -/
@@ -244,7 +244,7 @@ lemma orthogonalResidualSingularValue_sq (ε : ℝ) :
   have hs : Real.sqrt (15 : ℝ) ^ 2 = 15 := Real.sq_sqrt (by norm_num)
   unfold orthogonalResidualSingularValue
   rw [mul_pow, sq_abs]
-  nlinarith
+  nlinarith only [hs]
 
 /-- Each orthogonal-residual column has squared norm `ε² / 30` — half the nonzero
 singular value squared, the two columns splitting it evenly. -/
@@ -253,7 +253,7 @@ lemma orthogonalResidualColumnNorm_sq (ε : ℝ) :
   have hs : Real.sqrt (30 : ℝ) ^ 2 = 30 := Real.sq_sqrt (by norm_num)
   unfold orthogonalResidualColumnNorm
   rw [mul_pow, sq_abs]
-  nlinarith
+  nlinarith only [hs]
 
 end
 
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamCharacteristic.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamCharacteristic.lean
index 6fd4b14156..21293ed713 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamCharacteristic.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamCharacteristic.lean
@@ -5,12 +5,16 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import Mathlib.Analysis.Calculus.IteratedDeriv.Defs
+-- Preserve the real normed-space instance in the exported derivative statements.
+public import Mathlib.Analysis.InnerProductSpace.Basic -- shake: keep
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
-public import Mathlib.Tactic
+import Mathlib.Tactic.Linarith -- shake: keep
+import Mathlib.Tactic.LinearCombination -- shake: keep
+import Mathlib.Tactic.NormNum -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-!
 # Characteristic equation for the free--free beam
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamCharacteristicConverse.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamCharacteristicConverse.lean
index e8550cdef5..40ce4326e2 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamCharacteristicConverse.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamCharacteristicConverse.lean
@@ -5,9 +5,10 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamCharacteristic
-public import Mathlib.Tactic
+import Mathlib.Tactic.Linarith -- shake: keep
+import Mathlib.Tactic.NormNum -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-!
 # Converse characteristic construction for the free--free beam
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamEigenmodeReduction.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamEigenmodeReduction.lean
index d147a3e975..f8e6e58fda 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamEigenmodeReduction.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamEigenmodeReduction.lean
@@ -5,10 +5,8 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamCharacteristicConverse
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamAnalyticFoundation
-public import Mathlib.Tactic
 
 /-!
 # Reduction of positive free-beam eigenvalues to the characteristic equation
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamFoundationAssembler.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamFoundationAssembler.lean
index 8dace99a40..dc3f8e7b86 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamFoundationAssembler.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamFoundationAssembler.lean
@@ -5,12 +5,10 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.MaximalDomainTransport
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.GraphClosedness
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.CompactGraphEmbedding
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamAnalyticFoundation
-public import Mathlib.Tactic
 
 /-!
 # Assembly of the paper-facing free-beam analytic foundation
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamModeData.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamModeData.lean
index fe45446824..29d950fe6d 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamModeData.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamModeData.lean
@@ -5,10 +5,10 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamCharacteristicConverse
 public import LeanPool.DavisKahan.DavisKahan.Analysis.FourthOrderODE.SmoothGreenIdentity
-public import Mathlib.Tactic
+import Mathlib.Tactic.NormNum -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-!
 # Classical characteristic modes as fourth-order derivative data
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamModeUniqueness.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamModeUniqueness.lean
index c7592decb9..4f1fa09a14 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamModeUniqueness.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamModeUniqueness.lean
@@ -5,11 +5,12 @@ Authors: Jon Crall, Claude Fable 5
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamCharacteristic
 public import Mathlib.Analysis.ODE.ExistUnique
 public import Mathlib.Analysis.Calculus.Deriv.Prod
-public import Mathlib.Tactic
+import Mathlib.Tactic.FieldSimp -- shake: keep
+import Mathlib.Tactic.Positivity -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-!
 # Every solution of the free-beam ODE is a classical mode
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamRootExclusion.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamRootExclusion.lean
index dfdcd9485a..68b8ad8388 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamRootExclusion.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamRootExclusion.lean
@@ -95,7 +95,7 @@ private theorem cosMulCosh_deriv_neg {b : ℝ} (hb : 0 < b) (hle : b ≤ π / 2)
     have hs : 0 < Real.sin x :=
       Real.sin_pos_of_pos_of_lt_pi hx.1 (by linarith [Real.pi_pos, hx.2])
     have hh : 0 < Real.sinh x := Real.sinh_pos_iff.mpr hx.1
-    nlinarith
+    nlinarith only [hs, hh]
   have h0 : (0 : ℝ) ∈ Set.Icc (0 : ℝ) (π / 2) := ⟨le_refl _, by positivity⟩
   have hbmem : b ∈ Set.Icc (0 : ℝ) (π / 2) := ⟨hb.le, hle⟩
   have h := hanti h0 hbmem hb
@@ -127,7 +127,7 @@ theorem cos_mul_cosh_lt_one_of_le_three_pi_div_two {b : ℝ} (hb : 0 < b)
   · have hcos : Real.cos b ≤ 0 :=
       Real.cos_nonpos_of_pi_div_two_le_of_le h.le (by linarith)
     have hcosh : 0 < Real.cosh b := Real.cosh_pos b
-    nlinarith
+    nlinarith only [hcos, hcosh]
 
 /-! ## The thin interval `(3π/2, 4.73]`
 
@@ -240,7 +240,7 @@ theorem cos_mul_cosh_lt_one_of_le_four_seventy_three {b : ℝ} (hb : 0 < b)
       rw [Real.cosh_le_cosh, abs_of_pos hb, abs_of_pos (by norm_num)]
       exact hle
     rcases le_or_gt (Real.cos b) 0 with hc | hc
-    · nlinarith [Real.cosh_pos b]
+    · nlinarith only [hcos, hcosh, Real.cosh_pos b]
     · calc Real.cos b * Real.cosh b < 0.017612 * Real.cosh b :=
             mul_lt_mul_of_pos_right hcos (Real.cosh_pos b)
         _ < 0.017612 * 56.66 := mul_lt_mul_of_pos_left hcosh (by norm_num)
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamRootLocalization.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamRootLocalization.lean
index b21951d555..83959d6865 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamRootLocalization.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/FreeBeamRootLocalization.lean
@@ -5,10 +5,10 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamCharacteristic
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamRootExclusion
-public import Mathlib.Tactic
+import Mathlib.Tactic.Linarith -- shake: keep
+import Mathlib.Tactic.NormNum -- shake: keep
 
 /-!
 # Reduction of free-beam root localization to scalar certificates
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/IndividualAngles.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/IndividualAngles.lean
index ccbccea5bc..2db5616bb5 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/IndividualAngles.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/IndividualAngles.lean
@@ -47,7 +47,7 @@ lemma combined_individual_coefficient_sq :
   have h3 : Real.sqrt (3 : ℝ) ^ 2 = 3 := Real.sq_sqrt (by norm_num)
   have h15 : Real.sqrt (15 : ℝ) ^ 2 = 15 := Real.sq_sqrt (by norm_num)
   unfold halfTanTwoPsiCoefficient tanEtaCoefficient
-  nlinarith
+  nlinarith only [h3, h15]
 
 /-- The combined coefficient itself, the nonnegative square root of the previous. -/
 lemma combined_individual_coefficient :
@@ -81,10 +81,10 @@ theorem individual_angle_le_exact_envelope
     positivity
   have hpsq : psi ^ 2 ≤
       (halfTanTwoPsiCoefficient * ε / denominator) ^ 2 := by
-    nlinarith
+    nlinarith only [hpsi0, hpsi]
   have hetasq : eta ^ 2 ≤
       (tanEtaCoefficient * ε / denominator) ^ 2 := by
-    nlinarith
+    nlinarith only [heta0, heta]
   have hcoeff := combined_individual_coefficient_sq
   have htargetsq : omega ^ 2 ≤
       ((Real.sqrt 7 / 10) * ε / denominator) ^ 2 := by
@@ -95,9 +95,9 @@ theorem individual_angle_le_exact_envelope
       _ = ((Real.sqrt 7 / 10) * ε / denominator) ^ 2 := by
         have h7 : Real.sqrt (7 : ℝ) ^ 2 = 7 := Real.sq_sqrt (by norm_num)
         field_simp [ne_of_gt hden]
-        nlinarith
+        nlinarith only [hcoeff, h7]
   have hright0 : 0 ≤ (Real.sqrt 7 / 10) * ε / denominator := by positivity
-  nlinarith
+  nlinarith only [htargetsq, hright0]
 
 /-! ## The two angles are controlled by their tangents
 
@@ -146,11 +146,11 @@ theorem arccos_ratio_lt_pi_div_four {p q : ℝ} (hq : 0 ≤ q) (hqp : q < p) :
       sq_nonneg (Real.sqrt 2 * Real.sqrt (p ^ 2 + q ^ 2) - 2 * p)]
   have hle : p / Real.sqrt (p ^ 2 + q ^ 2) ≤ 1 := by
     rw [div_le_one hs]
-    nlinarith [hsq, Real.sqrt_nonneg (p ^ 2 + q ^ 2)]
+    nlinarith only [hq, hqp, hs, hsq, hsq, Real.sqrt_nonneg (p ^ 2 + q ^ 2)]
   have h4 : Real.arccos (Real.sqrt 2 / 2) = Real.pi / 4 := by
     rw [← Real.cos_pi_div_four, Real.arccos_cos (by positivity) (by linarith [Real.pi_pos])]
   rw [← h4]
-  exact Real.arccos_lt_arccos (by nlinarith [Real.sqrt_nonneg 2]) hkey hle
+  exact Real.arccos_lt_arccos (by nlinarith only [Real.sqrt_nonneg 2]) hkey hle
 
 /-- Half the tangent of the doubled angle, in the two coordinates.  This is the
 exact `tan (2 psi) / 2` the Schur-complement reduction has to bound. -/
@@ -166,11 +166,11 @@ theorem half_tan_two_arccos_ratio {p q : ℝ} (hq : 0 ≤ q) (hqp : q < p) :
     have h1 : 1 - (p / Real.sqrt (p ^ 2 + q ^ 2)) ^ 2
         = (q / Real.sqrt (p ^ 2 + q ^ 2)) ^ 2 := by
       field_simp
-      nlinarith [hsq]
+      nlinarith only [hsq, hsq]
     rw [h1, Real.sqrt_sq (by positivity)]
     field_simp
   rw [Real.tan_two_mul, htan]
-  have hne : p ^ 2 - q ^ 2 ≠ 0 := by nlinarith
+  have hne : p ^ 2 - q ^ 2 ≠ 0 := by nlinarith only [hq, hqp]
   field_simp
 
 /-- **The individual-eigenvector envelope, from the spherical identity and the
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/NumericalBounds.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/NumericalBounds.lean
index ee76ba5c0b..332f8dcc6a 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/NumericalBounds.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/NumericalBounds.lean
@@ -27,57 +27,50 @@ namespace Section9
 
 private lemma sqrt76_lt_4359_div_500 :
     Real.sqrt 76 < (4359 : ℝ) / 500 := by
-  nlinarith [Real.sqrt_nonneg (76 : ℝ),
-    Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 76)]
+  nlinarith only [Real.sqrt_nonneg (76 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 76)]
 
 private lemma sqrt76_gt_87_div_10 :
     (87 : ℝ) / 10 < Real.sqrt 76 := by
-  nlinarith [Real.sqrt_nonneg (76 : ℝ),
-    Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 76)]
+  nlinarith only [Real.sqrt_nonneg (76 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 76)]
 
 private lemma sqrt3_lt_8661_div_5000 :
     Real.sqrt 3 < (8661 : ℝ) / 5000 := by
-  nlinarith [Real.sqrt_nonneg (3 : ℝ),
-    Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)]
+  nlinarith only [Real.sqrt_nonneg (3 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)]
 
 private lemma sqrt3_gt_17319_div_10000 :
     (17319 : ℝ) / 10000 < Real.sqrt 3 := by
-  nlinarith [Real.sqrt_nonneg (3 : ℝ),
-    Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)]
+  nlinarith only [Real.sqrt_nonneg (3 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)]
 
 private lemma sqrt15_lt_3873_div_1000 :
     Real.sqrt 15 < (3873 : ℝ) / 1000 := by
-  nlinarith [Real.sqrt_nonneg (15 : ℝ),
-    Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 15)]
+  nlinarith only [Real.sqrt_nonneg (15 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 15)]
 
 private lemma sqrt30_lt_2739_div_500 :
     Real.sqrt 30 < (2739 : ℝ) / 500 := by
-  nlinarith [Real.sqrt_nonneg (30 : ℝ),
-    Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 30)]
+  nlinarith only [Real.sqrt_nonneg (30 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 30)]
 
 private lemma sqrt7_lt_53_div_20 :
     Real.sqrt 7 < (53 : ℝ) / 20 := by
-  nlinarith [Real.sqrt_nonneg (7 : ℝ),
-    Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 7)]
+  nlinarith only [Real.sqrt_nonneg (7 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 7)]
 
 /-- The upper Ritz coefficient is below the printed `0.7887`. -/
 lemma ritzHighCoefficient_lt_printed :
     ritzHighCoefficient < (7887 : ℝ) / 10000 := by
   unfold ritzHighCoefficient
-  nlinarith [sqrt3_lt_8661_div_5000]
+  nlinarith only [sqrt3_lt_8661_div_5000]
 
 /-- The lower Ritz coefficient is below the printed `0.21135`. -/
 lemma ritzLowCoefficient_lt_printed :
     ritzLowCoefficient < (4227 : ℝ) / 20000 := by
   unfold ritzLowCoefficient
-  nlinarith [sqrt3_gt_17319_div_10000]
+  nlinarith only [sqrt3_gt_17319_div_10000]
 
 /-- The top residual root `√((11 + √76)/30)` is below the printed `0.811`. -/
 lemma residualTopRoot_lt_printed :
     Real.sqrt ((11 + Real.sqrt 76) / 30) < (811 : ℝ) / 1000 := by
   have hq : 0 ≤ (11 + Real.sqrt 76) / 30 := by positivity
   have hs := Real.sq_sqrt hq
-  nlinarith [sqrt76_lt_4359_div_500, Real.sqrt_nonneg ((11 + Real.sqrt 76) / 30)]
+  nlinarith only [hs, sqrt76_lt_4359_div_500, Real.sqrt_nonneg ((11 + Real.sqrt 76) / 30)]
 
 /-- The bottom residual root `√((11 - √76)/30)` is below the printed `0.279`. -/
 lemma residualBottomRoot_lt_printed :
@@ -85,13 +78,13 @@ lemma residualBottomRoot_lt_printed :
   have h76 := sqrt76_le_eleven
   have hq : 0 ≤ (11 - Real.sqrt 76) / 30 := by positivity
   have hs := Real.sq_sqrt hq
-  nlinarith [sqrt76_gt_87_div_10, Real.sqrt_nonneg ((11 - Real.sqrt 76) / 30)]
+  nlinarith only [hs, sqrt76_gt_87_div_10, Real.sqrt_nonneg ((11 - Real.sqrt 76) / 30)]
 
 /-- The initial `sin Θ` estimate is below the printed decimal, for every `ε > 0`. -/
 lemma initial_sin_exact_lt_printed (ε : ℝ) (hε : 0 < ε) :
     residualTopSingularValue ε / 500 < (811 : ℝ) / 500000 * ε := by
   rw [residualTopSingularValue, abs_of_pos hε]
-  nlinarith [residualTopRoot_lt_printed]
+  nlinarith only [hε, residualTopRoot_lt_printed]
 
 /-- The initial Ky Fan 2-norm estimate is below the printed decimal, for every
 `ε > 0`. -/
@@ -99,7 +92,7 @@ lemma initial_kyFanTwo_exact_lt_printed (ε : ℝ) (hε : 0 < ε) :
     residualKyFanTwo ε / 500 < (109 : ℝ) / 50000 * ε := by
   rw [residualKyFanTwo, residualTopSingularValue, residualBottomSingularValue,
     abs_of_pos hε]
-  nlinarith [residualTopRoot_lt_printed, residualBottomRoot_lt_printed]
+  nlinarith only [hε, residualTopRoot_lt_printed, residualBottomRoot_lt_printed]
 
 /-- Exact normalized tangent bound obtained from the recentered residual. -/
 noncomputable def tangentThetaExactBound (ε : ℝ) : ℝ :=
@@ -138,14 +131,14 @@ private theorem ratio_strict_mono
     (hc : c ≤ C) (hC : C * ε < 1) :
     (a * ε) / (1 - c * ε) < (A * ε) / (1 - C * ε) := by
   have hdC : 0 < 1 - C * ε := by linarith
-  have hdc : 0 < 1 - c * ε := by nlinarith
+  have hdc : 0 < 1 - c * ε := by nlinarith only [hε, hc, hC]
   have hnum : a * ε < A * ε := mul_lt_mul_of_pos_right ha hε
   have hfirst : (a * ε) / (1 - c * ε) < (A * ε) / (1 - c * ε) :=
     div_lt_div_of_pos_right hnum hdc
   have hA0 : 0 ≤ A * ε := by
     have hA : 0 < A := lt_of_le_of_lt ha0 ha
     exact (mul_pos hA hε).le
-  have hden : 1 - C * ε ≤ 1 - c * ε := by nlinarith
+  have hden : 1 - C * ε ≤ 1 - c * ε := by nlinarith only [hε, hc]
   have hsecond : (A * ε) / (1 - c * ε) ≤ (A * ε) / (1 - C * ε) := by
     apply (div_le_div_iff₀ hdc hdC).2
     exact mul_le_mul_of_nonneg_left hden hA0
@@ -160,9 +153,9 @@ lemma tangentThetaExactBound_lt_printed (ε : ℝ)
         (1 - (7887 : ℝ) / 5000000 * ε) := by
   unfold tangentThetaExactBound
   apply ratio_strict_mono hε (by positivity)
-  · nlinarith [sqrt15_lt_3873_div_1000]
-  · nlinarith [ritzHighCoefficient_lt_printed]
-  · nlinarith
+  · nlinarith only [sqrt15_lt_3873_div_1000]
+  · nlinarith only [ritzHighCoefficient_lt_printed]
+  · nlinarith only [hε100]
 
 /-- The exact `tan 2Θ` bound is below the printed rational bound — twice the
 `tan Θ` numerator over the same denominator, so it needs the same `ε < 100`. -/
@@ -173,9 +166,9 @@ lemma tangentTwoThetaExactBound_lt_printed (ε : ℝ)
         (1 - (7887 : ℝ) / 5000000 * ε) := by
   unfold tangentTwoThetaExactBound
   apply ratio_strict_mono hε (by positivity)
-  · nlinarith [sqrt15_lt_3873_div_1000]
-  · nlinarith [ritzHighCoefficient_lt_printed]
-  · nlinarith
+  · nlinarith only [sqrt15_lt_3873_div_1000]
+  · nlinarith only [ritzHighCoefficient_lt_printed]
+  · nlinarith only [hε100]
 
 /-- The exact lower individual-angle tangent bound is below its printed rational
 bound, on `0 < ε < 100`. -/
@@ -186,9 +179,9 @@ lemma lowerIndividualTangentExactBound_lt_printed (ε : ℝ)
         (1 - (4227 : ℝ) / 10000000 * ε) := by
   unfold lowerIndividualTangentExactBound
   apply ratio_strict_mono hε (by positivity)
-  · nlinarith [sqrt30_lt_2739_div_500]
-  · nlinarith [ritzLowCoefficient_lt_printed]
-  · nlinarith
+  · nlinarith only [sqrt30_lt_2739_div_500]
+  · nlinarith only [ritzLowCoefficient_lt_printed]
+  · nlinarith only [hε100]
 
 /-- The exact upper individual-angle tangent bound is below its printed rational
 bound, on `0 < ε < 100`. -/
@@ -199,9 +192,9 @@ lemma upperIndividualTangentExactBound_lt_printed (ε : ℝ)
         (1 - (7887 : ℝ) / 5000000 * ε) := by
   unfold upperIndividualTangentExactBound
   apply ratio_strict_mono hε (by positivity)
-  · nlinarith [sqrt30_lt_2739_div_500]
-  · nlinarith [ritzHighCoefficient_lt_printed]
-  · nlinarith
+  · nlinarith only [sqrt30_lt_2739_div_500]
+  · nlinarith only [ritzHighCoefficient_lt_printed]
+  · nlinarith only [hε100]
 
 /-- The exact lower individual-angle bound is below its printed rational bound, on
 `0 < ε < 100`. -/
@@ -212,9 +205,9 @@ lemma lowerIndividualAngleExactBound_lt_printed (ε : ℝ)
         (1 - (43 : ℝ) / 100000 * ε) := by
   unfold lowerIndividualAngleExactBound
   apply ratio_strict_mono hε (by positivity)
-  · nlinarith [sqrt7_lt_53_div_20]
-  · nlinarith [ritzLowCoefficient_lt_printed]
-  · nlinarith
+  · nlinarith only [sqrt7_lt_53_div_20]
+  · nlinarith only [ritzLowCoefficient_lt_printed]
+  · nlinarith only [hε100]
 
 /-- The exact upper individual-angle bound is below its printed rational bound, on
 `0 < ε < 100`. -/
@@ -225,9 +218,9 @@ lemma upperIndividualAngleExactBound_lt_printed (ε : ℝ)
         (1 - (1 : ℝ) / 625 * ε) := by
   unfold upperIndividualAngleExactBound
   apply ratio_strict_mono hε (by positivity)
-  · nlinarith [sqrt7_lt_53_div_20]
-  · nlinarith [ritzHighCoefficient_lt_printed]
-  · nlinarith
+  · nlinarith only [sqrt7_lt_53_div_20]
+  · nlinarith only [ritzHighCoefficient_lt_printed]
+  · nlinarith only [hε100]
 
 /-! ## Printed equations as consequences of exact theorem outputs -/
 
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/SchurComplement.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/SchurComplement.lean
index 6950924501..799257561d 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/SchurComplement.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/SchurComplement.lean
@@ -172,7 +172,7 @@ theorem norm_lower_coordinate_le {b w y : F} {lam β : ℝ}
   · rw [← hy0, mul_zero]
     exact norm_nonneg b
   · have : (β - lam) * ‖y‖ ^ 2 ≤ ‖b‖ * ‖y‖ := le_trans h1 h2
-    nlinarith
+    nlinarith only [h1, h2, hypos]
 
 /-- **The Schur coefficient is nonnegative.**  The scalar that the substituted
 upper block contributes, `-re ⟪B x, y⟫`, is the value of the positive form
@@ -199,7 +199,7 @@ theorem schurCoefficient_le {b w y : F} {lam β : ℝ}
   obtain ⟨-, h2⟩ := lower_block_test (𝕜 := 𝕜) hbottom hform
   have hy := norm_lower_coordinate_le (𝕜 := 𝕜) hbottom hform hlt
   have hb0 : 0 ≤ ‖b‖ := norm_nonneg b
-  nlinarith
+  nlinarith only [hlt, h2, hy, hb0]
 
 /-- **Nondegeneracy: the trial coordinate of a block eigenvector cannot
 vanish.**  If `B x = 0` — in particular if `x = 0` — then the complementary
@@ -213,7 +213,7 @@ theorem lower_coordinate_eq_zero_of_residual_eq_zero {b w y : F} {lam β : ℝ}
     y = 0 := by
   have h := norm_lower_coordinate_le (𝕜 := 𝕜) hbottom hform hlt
   rw [hb, norm_zero] at h
-  have : ‖y‖ ≤ 0 := by nlinarith [norm_nonneg y]
+  have : ‖y‖ ≤ 0 := by nlinarith only [hlt, h, norm_nonneg y]
   exact norm_eq_zero.1 (le_antisymm this (norm_nonneg y))
 
 end BlockEstimates
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/TrialSubspace.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/TrialSubspace.lean
index 5037c1e27d..a52d9c679b 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/TrialSubspace.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/TrialSubspace.lean
@@ -85,7 +85,7 @@ private lemma sqrt75_eq_five_mul_sqrt3 :
   have h3 : Real.sqrt (3 : ℝ) ^ 2 = 3 := Real.sq_sqrt (by norm_num)
   have h75nonneg := Real.sqrt_nonneg (75 : ℝ)
   have h3nonneg := Real.sqrt_nonneg (3 : ℝ)
-  nlinarith [sq_nonneg (Real.sqrt 75 - 5 * Real.sqrt 3)]
+  nlinarith only [h75, h3, h75nonneg, h3nonneg, sq_nonneg (Real.sqrt 75 - 5 * Real.sqrt 3)]
 
 /-- The first trial function is a unit vector in `L²(0,1)`. -/
 lemma trialOne_norm_sq : CenteredAffine.inner trialOne trialOne = 1 := by
@@ -93,7 +93,7 @@ lemma trialOne_norm_sq : CenteredAffine.inner trialOne trialOne = 1 := by
   have h3 : Real.sqrt (3 : ℝ) ^ 2 = 3 := Real.sq_sqrt (by norm_num)
   unfold CenteredAffine.inner trialOne
   dsimp
-  nlinarith
+  nlinarith only [h2, h3]
 
 /-- The second trial function is a unit vector in `L²(0,1)`. -/
 lemma trialTwo_norm_sq : CenteredAffine.inner trialTwo trialTwo = 1 := by
@@ -101,16 +101,15 @@ lemma trialTwo_norm_sq : CenteredAffine.inner trialTwo trialTwo = 1 := by
   have h3 : Real.sqrt (3 : ℝ) ^ 2 = 3 := Real.sq_sqrt (by norm_num)
   unfold CenteredAffine.inner trialTwo
   dsimp
-  nlinarith
+  nlinarith only [h2, h3]
 
 /-- The two trial functions are orthogonal, so together they form an orthonormal
 basis of the trial subspace. -/
 lemma trialOne_inner_trialTwo : CenteredAffine.inner trialOne trialTwo = 0 := by
-  have h2 : Real.sqrt (2 : ℝ) ^ 2 = 2 := Real.sq_sqrt (by norm_num)
   have h3 : Real.sqrt (3 : ℝ) ^ 2 = 3 := Real.sq_sqrt (by norm_num)
   unfold CenteredAffine.inner trialOne trialTwo
   dsimp
-  nlinarith
+  linear_combination -(Real.sqrt 2 ^ 2 / 12) * h3
 
 /-- The `t`-form is diagonalised by the trial pair, and its first diagonal entry is
 the lower Ritz coefficient — this is where the Ritz value of equation (9.5)
@@ -140,11 +139,10 @@ lemma trialTwo_tInner_trialTwo :
 trial pair a Ritz basis. -/
 lemma trialOne_tInner_trialTwo :
     CenteredAffine.tInner trialOne trialTwo = 0 := by
-  have h2 : Real.sqrt (2 : ℝ) ^ 2 = 2 := Real.sq_sqrt (by norm_num)
   have h3 : Real.sqrt (3 : ℝ) ^ 2 = 3 := Real.sq_sqrt (by norm_num)
   unfold CenteredAffine.tInner trialOne trialTwo
   dsimp
-  nlinarith
+  linear_combination -(Real.sqrt 2 ^ 2 / 24) * h3
 
 /-- First diagonal entry of the `t²`-form: `(11 - √75) / 30`. -/
 lemma trialOne_tSqInner_trialOne :
@@ -178,7 +176,7 @@ lemma trialOne_tSqInner_trialTwo :
   have h3 : Real.sqrt (3 : ℝ) ^ 2 = 3 := Real.sq_sqrt (by norm_num)
   unfold CenteredAffine.tSqInner trialOne trialTwo
   dsimp
-  nlinarith
+  nlinarith only [h2, h3]
 
 /-- The multiplication-by-`epsilon t` compression is the diagonal Ritz matrix
 from equation (9.5). -/
diff --git a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/WeinbergerComparison.lean b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/WeinbergerComparison.lean
index 4098dbaeda..a2b8c4986d 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/WeinbergerComparison.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sources/DavisKahan1970/Section9/WeinbergerComparison.lean
@@ -107,11 +107,11 @@ theorem tangent_sq_le_of_weinberger_sine_sq
       (alphaHat - alphaCheck) / (gap - alphaHat) := by
   have hgapCheck : 0 < gap - alphaCheck := by linarith
   have hgapHat : 0 < gap - alphaHat := by linarith
-  have hsden : 0 < 1 - s ^ 2 := by nlinarith [sq_nonneg s]
+  have hsden : 0 < 1 - s ^ 2 := by nlinarith only [hs0, hs1, sq_nonneg s]
   have hcross : s ^ 2 * (gap - alphaCheck) ≤ alphaHat - alphaCheck :=
     (le_div_iff₀ hgapCheck).mp hweinberger
   apply (div_le_div_iff₀ hsden hgapHat).2
-  nlinarith
+  nlinarith only [hcross]
 
 /-- Exact normalized envelope for the first historical comparison bound. -/
 noncomputable def weinbergerLowerTangentExactBound (ε : ℝ) : ℝ :=
@@ -128,18 +128,17 @@ private theorem historical_ratio_bound
     (((Real.sqrt 15 / 15) / 500) * ε) / (1 - c * ε) <
       ((1291 : ℝ) / 2500000 * ε) / (1 - C * ε) := by
   have hs15 : Real.sqrt 15 < (3873 : ℝ) / 1000 := by
-    nlinarith [Real.sqrt_nonneg (15 : ℝ),
-      Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 15)]
+    nlinarith only [Real.sqrt_nonneg (15 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 15)]
   have ha : (Real.sqrt 15 / 15) / 500 < (1291 : ℝ) / 2500000 := by
-    nlinarith
+    nlinarith only [hs15]
   have hdC : 0 < 1 - C * ε := by linarith
-  have hdc : 0 < 1 - c * ε := by nlinarith
+  have hdc : 0 < 1 - c * ε := by nlinarith only [hε, hc, hC]
   have hfirst :
       (((Real.sqrt 15 / 15) / 500) * ε) / (1 - c * ε) <
         ((1291 : ℝ) / 2500000 * ε) / (1 - c * ε) := by
     apply div_lt_div_of_pos_right _ hdc
     exact mul_lt_mul_of_pos_right ha hε
-  have hden : 1 - C * ε ≤ 1 - c * ε := by nlinarith
+  have hden : 1 - C * ε ≤ 1 - c * ε := by nlinarith only [hε, hc]
   have hnum0 : 0 ≤ (1291 : ℝ) / 2500000 * ε := by positivity
   have hsecond :
       ((1291 : ℝ) / 2500000 * ε) / (1 - c * ε) ≤
@@ -158,8 +157,8 @@ theorem equation_9_8_lower
   apply h.trans_lt
   unfold weinbergerLowerTangentExactBound
   apply historical_ratio_bound hε
-  · nlinarith [ritzLowCoefficient_lt_printed]
-  · nlinarith
+  · nlinarith only [ritzLowCoefficient_lt_printed]
+  · nlinarith only [hε100]
 
 /-- Second line of equation (9.8), conditional on the exact comparison bound. -/
 theorem equation_9_8_upper
@@ -188,12 +187,11 @@ within `ε²/7500` of the lower Ritz value, and that is exactly the margin the
 first line of (9.8) needs. -/
 
 private lemma sqrt_three_gt : (17 : ℝ) / 10 < Real.sqrt 3 := by
-  nlinarith [Real.sqrt_nonneg (3 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)]
+  nlinarith only [Real.sqrt_nonneg (3 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)]
 
 private lemma ritzLowCoefficient_pos : 0 < ritzLowCoefficient := by
   unfold ritzLowCoefficient
-  nlinarith [Real.sqrt_nonneg (3 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3),
-    sqrt_three_gt]
+  nlinarith only [Real.sqrt_nonneg (3 : ℝ), Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3), sqrt_three_gt]
 
 private lemma continuous_charAt (ε : ℝ) :
     Continuous fun lam => (weinbergerComparisonMatrix ε).charAt lam := by
@@ -238,30 +236,30 @@ theorem exists_weinbergerLowerRootCertificate (ε : ℝ) (hε : 0 < ε) (hε100
   have hapos : 0 < a := by rw [ha, ritzLow]; positivity
   have halt : a < 25 := by
     rw [ha, ritzLow]
-    nlinarith
+    nlinarith only [hε, hε100, hc0, hc1]
   have hgap : ε * (Real.sqrt 3 / 3) = b - a := (ritzHigh_sub_ritzLow ε).symm
   have hgappos : ε * (17 / 30 : ℝ) ≤ b - a := by
     rw [← hgap]
-    nlinarith [sqrt_three_gt]
-  have hab : a < b := by nlinarith
+    nlinarith only [hε, sqrt_three_gt]
+  have hab : a < b := by nlinarith only [hε, hgappos]
   have hba : (0 : ℝ) ≤ b - a := by linarith
   have hc1pos : 0 < ritzHighCoefficient := by
     unfold ritzHighCoefficient
     positivity
   have hblt : b < 100 := by
     rw [hb, ritzHigh]
-    nlinarith [ritzHighCoefficient_lt_printed]
+    nlinarith only [hε, hε100, hc0, hc1, ritzHighCoefficient_lt_printed]
   have htpos : 0 < t := by rw [ht]; positivity
   -- the three sign evaluations
   have hva : (weinbergerComparisonMatrix ε).charAt a ≤ 0 := by
     rw [ha, charAt_ritzLow]
-    nlinarith
+    nlinarith only [hε, hgappos]
   have hvb : 0 ≤ (weinbergerComparisonMatrix ε).charAt b := by
     rw [hb, charAt_ritzHigh]
-    nlinarith
+    nlinarith only [hε, hgappos]
   have hkey : 500 * t ≤ 150 * (b - a) := by
     rw [ht]
-    nlinarith
+    nlinarith only [hε, hε100, ht, hgappos, htpos]
   have hvat : 0 ≤ (weinbergerComparisonMatrix ε).charAt (a - t) := by
     rw [weinbergerComparisonMatrix_charAt, ← ha, ← hb]
     have hk : ε ^ 2 / 30 = 250 * t := by rw [ht]; ring
@@ -272,16 +270,16 @@ theorem exists_weinbergerLowerRootCertificate (ε : ℝ) (hε : 0 < ε) (hε100
     rw [hgoal]
     have hA : t * (b - a) * 400 ≤ t * (b - a + t) * (500 - a + t) := by
       refine mul_le_mul ?_ (by linarith) (by norm_num) (by positivity)
-      nlinarith
-    have hB : 500 * t * t ≤ 150 * t * (b - a) := by nlinarith
-    nlinarith [hA, hB]
+      nlinarith only [ht]
+    have hB : 500 * t * t ≤ 150 * t * (b - a) := by nlinarith only [ht, hkey, hgoal]
+    nlinarith only [hA, hB, hA, hB]
   -- the two roots
   obtain ⟨r₀, hr₀mem, hr₀⟩ :=
     intermediate_value_Icc' (by linarith : a - t ≤ a)
       ((continuous_charAt ε).continuousOn) (Set.mem_Icc.2 ⟨hva, hvat⟩)
   have htsmall : t ≤ b - a := by
     rw [ht]
-    nlinarith
+    nlinarith only [ht, htpos, hkey]
   have hvbt : (weinbergerComparisonMatrix ε).charAt (b - t) ≤ 0 := by
     rw [weinbergerComparisonMatrix_charAt, ← ha, ← hb]
     have hk : ε ^ 2 / 30 = 250 * t := by rw [ht]; ring
@@ -294,7 +292,7 @@ theorem exists_weinbergerLowerRootCertificate (ε : ℝ) (hε : 0 < ε) (hε100
       refine mul_le_mul_of_nonneg_left (by linarith) ?_
       have : (0 : ℝ) ≤ b - a - t := by linarith
       positivity
-    nlinarith [hA, htpos, hkey]
+    nlinarith only [hε, ht, hgappos, hgoal, hA, hA, htpos, hkey]
   obtain ⟨r₁, hr₁mem, hr₁⟩ :=
     intermediate_value_Icc (by linarith : b - t ≤ b)
       ((continuous_charAt ε).continuousOn) (Set.mem_Icc.2 ⟨hvbt, hvb⟩)
@@ -369,15 +367,15 @@ theorem printed_weinberger_low_shift_inequality_reversed
     positivity
   have halt : a < 25 := by
     rw [show a = ritzLow ε from rfl, ritzLow]
-    nlinarith [ritzLowCoefficient_lt_printed]
+    nlinarith only [hε, hε100, hc0, ritzLowCoefficient_lt_printed]
   have hblt : b < 100 := by
     rw [show b = ritzHigh ε from rfl, ritzHigh]
-    nlinarith [ritzHighCoefficient_lt_printed]
+    nlinarith only [hε, hε100, ritzHighCoefficient_lt_printed]
   have hab : a < b := by
     rw [show a = ritzLow ε from rfl, show b = ritzHigh ε from rfl]
     have hgap := ritzHigh_sub_ritzLow ε
     have hsqrt : 0 < Real.sqrt 3 := Real.sqrt_pos.2 (by norm_num)
-    nlinarith
+    nlinarith only [hε, hgap, hsqrt]
   have hq : 0 < q := by
     dsimp [q]
     positivity
@@ -412,14 +410,14 @@ theorem printed_weinberger_low_shift_inequality_reversed
   have hsquare : ε ^ 2 < 10000 := by
     have hsum : 0 < 100 + ε := by linarith
     have hprod := mul_pos (sub_pos.mpr hε100) hsum
-    nlinarith
+    nlinarith only [hprod]
   have hcloseSmall : d < 4 / 3 := by
-    nlinarith
+    nlinarith only [hclose, hsquare]
   have heA : e < A := by
     dsimp [e, A, d] at hcloseSmall ⊢
     linarith
   have heqd : q * (e + d) = d * e * (A + d) := by
-    nlinarith [hroot']
+    nlinarith only [hroot', hroot']
   have hpositiveRemainder : 0 < d ^ 2 * (A - e) := by positivity
   have hfactorIdentity :
       (d * A - q) * (e + d) = d ^ 2 * (A - e) := by
@@ -461,7 +459,7 @@ theorem weinberger_tangent_le_lowerExactBound (ε : ℝ) (hε : 0 < ε) (hε100
   have hc0 : 0 < ritzLowCoefficient := ritzLowCoefficient_pos
   have hc1 : ritzLowCoefficient < (4227 : ℝ) / 20000 := ritzLowCoefficient_lt_printed
   have hapos : 0 < ritzLow ε := by rw [ritzLow]; positivity
-  have halt : ritzLow ε < 25 := by rw [ritzLow]; nlinarith
+  have halt : ritzLow ε < 25 := by rw [ritzLow]; nlinarith only [hε, hε100, hc0, hc1]
   have hclose : ritzLow ε - C.lower₀ ≤ ε ^ 2 / 7500 :=
     ritzLow_sub_weinbergerLowerRoots_le ε hε hε100
   have hroot_le : C.lower₀ ≤ ritzLow ε := C.lower₀_le_ritz
@@ -477,7 +475,7 @@ theorem weinberger_tangent_le_lowerExactBound (ε : ℝ) (hε : 0 < ε) (hε100
       = (ε * (Real.sqrt 15 / 15)) / (500 - ritzLow ε) := by
     unfold weinbergerLowerTangentExactBound
     rw [show ritzLow ε = ε * ritzLowCoefficient from rfl] at hden ⊢
-    rw [div_eq_div_iff (by nlinarith) (by linarith)]
+    rw [div_eq_div_iff (by nlinarith only [hden]) (by linarith)]
     ring
   have hWpos : 0 ≤ weinbergerLowerTangentExactBound ε := by
     rw [hW]
@@ -496,7 +494,7 @@ theorem weinberger_tangent_le_lowerExactBound (ε : ℝ) (hε : 0 < ε) (hε100
         ≤ (ε ^ 2 / 7500) * (500 - ritzLow ε) ^ 2 :=
           mul_le_mul_of_nonneg_right hclose (sq_nonneg _)
       _ ≤ ε ^ 2 / 15 * (500 - ritzLow ε) := by
-          nlinarith [mul_nonneg (mul_nonneg (sq_nonneg ε) hden.le) hapos.le]
+          nlinarith only [hapos, hden, mul_nonneg (mul_nonneg (sq_nonneg ε) hden.le) hapos.le]
   nlinarith [hchain, hWpos, sq_nonneg (tanPhi - weinbergerLowerTangentExactBound ε)]
 
 /-- **The certified middle root is within `ε²/7500` of the upper Ritz value.** -/
@@ -527,7 +525,7 @@ theorem weinberger_tangent_le_upperExactBound (ε : ℝ) (hε : 0 < ε) (hε100
   have hapos : 0 < ritzHigh ε := by rw [ritzHigh]; positivity
   have halt : ritzHigh ε < 100 := by
     rw [ritzHigh]
-    nlinarith [ritzHighCoefficient_lt_printed]
+    nlinarith only [hε, hε100, hc1pos, ritzHighCoefficient_lt_printed]
   have hclose : ritzHigh ε - C.lower₁ ≤ ε ^ 2 / 7500 :=
     ritzHigh_sub_weinbergerLowerRoots_le ε hε hε100
   have hroot_le : C.lower₁ ≤ ritzHigh ε := C.lower₁_le_ritz
@@ -540,7 +538,7 @@ theorem weinberger_tangent_le_upperExactBound (ε : ℝ) (hε : 0 < ε) (hε100
       = (ε * (Real.sqrt 15 / 15)) / (500 - ritzHigh ε) := by
     unfold weinbergerUpperTangentExactBound tangentThetaExactBound
     rw [show ritzHigh ε = ε * ritzHighCoefficient from rfl] at hden ⊢
-    rw [div_eq_div_iff (by nlinarith) (by linarith)]
+    rw [div_eq_div_iff (by nlinarith only [hden]) (by linarith)]
     ring
   have hWpos : 0 ≤ weinbergerUpperTangentExactBound ε := by
     rw [hW]
@@ -558,7 +556,7 @@ theorem weinberger_tangent_le_upperExactBound (ε : ℝ) (hε : 0 < ε) (hε100
         ≤ (ε ^ 2 / 7500) * (500 - ritzHigh ε) ^ 2 :=
           mul_le_mul_of_nonneg_right hclose (sq_nonneg _)
       _ ≤ ε ^ 2 / 15 * (500 - ritzHigh ε) := by
-          nlinarith [mul_nonneg (mul_nonneg (sq_nonneg ε) hden.le) hapos.le]
+          nlinarith only [hapos, hden, mul_nonneg (mul_nonneg (sq_nonneg ε) hden.le) hapos.le]
   nlinarith [hchain, hWpos, sq_nonneg (tanPhi - weinbergerUpperTangentExactBound ε)]
 
 /-- **Equation (9.8), first line, as printed**, from a Weinberger sine estimate at
diff --git a/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamClassicalReal.lean b/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamClassicalReal.lean
index f6e3d172a9..8adf977525 100644
--- a/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamClassicalReal.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamClassicalReal.lean
@@ -5,14 +5,20 @@ Authors: Jon Crall, OpenAI GPT-5.6 Sol
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.Specialized.FreeBeam.BeamFormSpaceReal
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamModeUniqueness
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamCharacteristicConverse
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamOrthogonality
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamRootLocalization
 public import Mathlib.Analysis.Real.Pi.Bounds
-public import Mathlib.Tactic
+import Mathlib.Tactic.Abel -- shake: keep
+import Mathlib.Tactic.FieldSimp -- shake: keep
+import Mathlib.Tactic.FunProp -- shake: keep
+import Mathlib.Tactic.Linarith -- shake: keep
+import Mathlib.Tactic.LinearCombination -- shake: keep
+import Mathlib.Tactic.NormNum -- shake: keep
+import Mathlib.Tactic.Positivity -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-! # Beam Classical Real -/
 
diff --git a/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamFormSpaceScalar.lean b/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamFormSpaceScalar.lean
index 708af9aa0a..1e989371d8 100644
--- a/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamFormSpaceScalar.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamFormSpaceScalar.lean
@@ -5,13 +5,17 @@ Authors: Jon Crall, Claude Fable 5
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.ShiftedBeamRealization
 public import LeanPool.DavisKahan.ForTauCeti.MeasureTheory.IntervalSecondPrimitiveCompact
 public import LeanPool.DavisKahan.ForTauCeti.MeasureTheory.IntervalSecondPrimitiveDeriv
 public import Mathlib.Analysis.Calculus.Deriv.Polynomial
 public import Mathlib.Analysis.InnerProductSpace.ProdL2
-public import Mathlib.Tactic
+import Mathlib.Tactic.Abel -- shake: keep
+import Mathlib.Tactic.FunProp -- shake: keep
+import Mathlib.Tactic.Linarith -- shake: keep
+import Mathlib.Tactic.NormNum -- shake: keep
+import Mathlib.Tactic.Positivity -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-! # Beam Form Space Scalar -/
 
diff --git a/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamSpectrum.lean b/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamSpectrum.lean
index 3ed15e4c4b..5d63146470 100644
--- a/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamSpectrum.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamSpectrum.lean
@@ -5,12 +5,17 @@ Authors: Jon Crall, Claude Fable 5
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.Specialized.FreeBeam.BeamFormSpace
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamModeUniqueness
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.FreeBeamRootLocalization
 public import Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
-public import Mathlib.Tactic
+import Mathlib.Tactic.Abel -- shake: keep
+import Mathlib.Tactic.FunProp -- shake: keep
+import Mathlib.Tactic.Linarith -- shake: keep
+import Mathlib.Tactic.LinearCombination -- shake: keep
+import Mathlib.Tactic.NormNum -- shake: keep
+import Mathlib.Tactic.Positivity -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-!
 # Kernel and eigenfunctions of the free-beam operator
diff --git a/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamSpectrumReal.lean b/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamSpectrumReal.lean
index 59fad3bc3d..f97d1671bc 100644
--- a/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamSpectrumReal.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamSpectrumReal.lean
@@ -5,11 +5,12 @@ Authors: Jon Crall, OpenAI GPT-5.6 Sol
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.Specialized.FreeBeam.BeamClassicalReal
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.CompactSelfAdjointClassification
 public import Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
-public import Mathlib.Tactic
+import Mathlib.Tactic.Abel -- shake: keep
+import Mathlib.Tactic.Linarith -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-!
 # Spectrum of the real free-beam realization
diff --git a/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamTrialReal.lean b/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamTrialReal.lean
index e4beeea5db..99f60198a5 100644
--- a/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamTrialReal.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Specialized/FreeBeam/BeamTrialReal.lean
@@ -5,13 +5,14 @@ Authors: Jon Crall, OpenAI GPT-5.6 Sol
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.Specialized.FreeBeam.BeamSpectrumReal
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.ExactData
 public import LeanPool.DavisKahan.DavisKahan.Sources.DavisKahan1970.Section9.TrialSubspace
 public import LeanPool.DavisKahan.DavisKahan.SinTheta.BoundedPerturbation
 public import LeanPool.DavisKahan.ForTauCeti.MeasureTheory.RadonNikodymL2
-public import Mathlib.Tactic
+import Mathlib.Tactic.FunProp -- shake: keep
+import Mathlib.Tactic.NormNum -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-! # Beam Trial Real -/
 
diff --git a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/BoundedGraphCompactness.lean b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/BoundedGraphCompactness.lean
index 67274dd304..90bdfa0152 100644
--- a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/BoundedGraphCompactness.lean
+++ b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/BoundedGraphCompactness.lean
@@ -5,9 +5,10 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.CompactGraphEmbedding
-public import Mathlib.Tactic
+import Mathlib.Tactic.Abel -- shake: keep
+import Mathlib.Tactic.Positivity -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-!
 # Graph compactness under bounded perturbations
diff --git a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/BoundedInverseRealization.lean b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/BoundedInverseRealization.lean
index f9b8356feb..6f3e5260a8 100644
--- a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/BoundedInverseRealization.lean
+++ b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/BoundedInverseRealization.lean
@@ -5,7 +5,6 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 /-
 The dense-range lemma below is adapted from Adam Bornemann's private lemma
 `denseRange_of_selfAdjoint_injective` in
@@ -17,7 +16,7 @@ The original and adapted files are Apache-2.0 licensed.
 
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.PositiveSurjectiveCriterion
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.CoerciveUnit
-public import Mathlib.Tactic
+import Mathlib.Tactic.Linarith -- shake: keep
 
 /-!
 # Unbounded inverse of a bounded positive resolvent
diff --git a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/CoerciveFormResolvent.lean b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/CoerciveFormResolvent.lean
index abcede3fda..79d402cae5 100644
--- a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/CoerciveFormResolvent.lean
+++ b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/CoerciveFormResolvent.lean
@@ -5,10 +5,8 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.BoundedInverseRealization
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.CoerciveUnit
-public import Mathlib.Tactic
 
 /-!
 # Bounded resolvent produced by a coercive form operator
diff --git a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/CompactGraphEmbedding.lean b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/CompactGraphEmbedding.lean
index 56f11ebed9..1591f64c0c 100644
--- a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/CompactGraphEmbedding.lean
+++ b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/CompactGraphEmbedding.lean
@@ -5,9 +5,9 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.BoundedInverseRealization
-public import Mathlib.Tactic
+import Mathlib.Tactic.Linarith -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-!
 # Compact resolvents and compact graph embeddings
diff --git a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/FormCompactness.lean b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/FormCompactness.lean
index 22280f1ece..7b3b9e68e2 100644
--- a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/FormCompactness.lean
+++ b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/FormCompactness.lean
@@ -5,10 +5,8 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.CoerciveFormResolvent
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.CompactGraphEmbedding
-public import Mathlib.Tactic
 
 /-!
 # Compact form embeddings give compact resolvents
diff --git a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/GraphClosedness.lean b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/GraphClosedness.lean
index a4e1f822cb..95a81b07a9 100644
--- a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/GraphClosedness.lean
+++ b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/GraphClosedness.lean
@@ -5,9 +5,7 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.TraceKernelModel
-public import Mathlib.Tactic
 
 /-!
 # Closedness of the transported fourth-order graph
diff --git a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/MaximalDomainTransport.lean b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/MaximalDomainTransport.lean
index d41d768312..42b8c23d98 100644
--- a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/MaximalDomainTransport.lean
+++ b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/MaximalDomainTransport.lean
@@ -5,9 +5,7 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.TraceKernelModel
-public import Mathlib.Tactic
 
 /-!
 # Transport of the maximal fourth-order graph space into the ambient Hilbert space
diff --git a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/PositiveSurjectiveCriterion.lean b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/PositiveSurjectiveCriterion.lean
index 363bd13760..f53d6c08a1 100644
--- a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/PositiveSurjectiveCriterion.lean
+++ b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/PositiveSurjectiveCriterion.lean
@@ -5,7 +5,6 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 /-
 The proof architecture of the self-adjointness criterion below is adapted from
 Adam Bornemann's proof of `Spectra.TomitaTakesaki.modularOp_isSelfAdjoint` in
@@ -19,7 +18,9 @@ public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.LinearPM
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.LinearPMap.Constructions
 public import LeanPool.DavisKahan.DavisKahan.BoundedOperator.Problem
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.AbstractSpectrum
-public import Mathlib.Tactic
+import Mathlib.Tactic.Abel -- shake: keep
+import Mathlib.Tactic.Linarith -- shake: keep
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-!
 # A positive-surjective self-adjointness criterion
diff --git a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/ShiftedBeamRealization.lean b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/ShiftedBeamRealization.lean
index 51cbb6e4c8..ef84c7224a 100644
--- a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/ShiftedBeamRealization.lean
+++ b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/ShiftedBeamRealization.lean
@@ -5,12 +5,11 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.CoerciveFormResolvent
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.FormCompactness
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.FormMethod.BoundedGraphCompactness
 public import LeanPool.DavisKahan.DavisKahan.SinTheta.BoundedPerturbation
-public import Mathlib.Tactic
+import Mathlib.Tactic.Ring -- shake: keep
 
 /-! # Shifted Beam Realization -/
 
diff --git a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/TraceKernelModel.lean b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/TraceKernelModel.lean
index 99e8a2ad72..a152c09f28 100644
--- a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/TraceKernelModel.lean
+++ b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/FormMethod/TraceKernelModel.lean
@@ -5,12 +5,10 @@ Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
 
-
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.LinearPMap.Closed
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.LinearPMap.Constructions
 public import LeanPool.DavisKahan.DavisKahan.BoundedOperator.Problem
 public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.AbstractSpectrum
-public import Mathlib.Tactic
 
 /-!
 # A graph-Hilbert model for fourth-order endpoint traces
diff --git a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/PartialMap/Complexification.lean b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/PartialMap/Complexification.lean
index 5e8af5809f..45ae014163 100644
--- a/LeanPool/DavisKahan/DavisKahan/SpectralTheory/PartialMap/Complexification.lean
+++ b/LeanPool/DavisKahan/DavisKahan/SpectralTheory/PartialMap/Complexification.lean
@@ -74,7 +74,7 @@ omit [InnerProductSpace ℝ E] [CompleteSpace E] in
 /-- Each coordinate norm is bounded by the L2 norm. -/
 theorem norm_im_le (z : Eℂ) : ‖im z‖ ≤ ‖z‖ := by
   rw [← sq_le_sq₀ (norm_nonneg _) (norm_nonneg _), RealComplexification.norm_sq]
-  nlinarith [sq_nonneg ‖re z‖]
+  nlinarith only [sq_nonneg ‖re z‖]
 
 /-- Coordinatewise complexification of a real closed-operator domain. -/
 def domain (A : E →ₗ.[ℝ] E) :
@@ -470,7 +470,7 @@ theorem semiboundedBelow_complexify
   change c * (‖re (z : Eℂ)‖ ^ 2 + ‖im (z : Eℂ)‖ ^ 2) ≤
     ⟪A (domainRe A z), re (z : Eℂ)⟫_ℝ +
       ⟪A (domainIm A z), im (z : Eℂ)⟫_ℝ
-  nlinarith [hr, hi]
+  nlinarith only [hr, hi, hr, hi]
 
 omit [CompleteSpace E] in
 /-- An upper quadratic-form bound is preserved exactly by complexification. -/
@@ -488,7 +488,7 @@ theorem semiboundedAbove_complexify
     ⟪A (domainRe A z), re (z : Eℂ)⟫_ℝ +
       ⟪A (domainIm A z), im (z : Eℂ)⟫_ℝ ≤
       c * (‖re (z : Eℂ)‖ ^ 2 + ‖im (z : Eℂ)‖ ^ 2)
-  nlinarith [hr, hi]
+  nlinarith only [hr, hi, hr, hi]
 
 omit [CompleteSpace E] in
 /-- Symmetry is preserved by coordinatewise complexification. -/
diff --git a/LeanPool/DavisKahan/DavisKahan/Sylvester/ShiftedInverse.lean b/LeanPool/DavisKahan/DavisKahan/Sylvester/ShiftedInverse.lean
index bfec558816..171a6a4952 100644
--- a/LeanPool/DavisKahan/DavisKahan/Sylvester/ShiftedInverse.lean
+++ b/LeanPool/DavisKahan/DavisKahan/Sylvester/ShiftedInverse.lean
@@ -99,9 +99,9 @@ theorem norm_shift_apply_le_of_form_bounds
     rw [hre, abs_le]
     constructor
     · rw [hc, hr] at *
-      nlinarith [sq_nonneg ‖(w : F)‖]
+      nlinarith only [h1, sq_nonneg ‖(w : F)‖]
     · rw [hc, hr] at *
-      nlinarith [sq_nonneg ‖(w : F)‖]
+      nlinarith only [h2, sq_nonneg ‖(w : F)‖]
   -- polarization: unnormalized sesquilinear bound
   have hpolar : ∀ v w : B.domain,
       RCLike.re ⟪S v, (w : F)⟫_𝕜 ≤ (r / 2) * (‖(v : F)‖ ^ 2 + ‖(w : F)‖ ^ 2) := by
@@ -142,7 +142,7 @@ theorem norm_shift_apply_le_of_form_bounds
       rw [Submodule.coe_sub]
     rw [hcoeadd] at hb1
     rw [hcoesub] at hb2
-    nlinarith [hexp]
+    nlinarith only [hβα, hr, hexp, hb1, hb2, hpar, hexp]
   -- scaling: the sharp sesquilinear bound
   have hscaled : ∀ v w : B.domain,
       RCLike.re ⟪S v, (w : F)⟫_𝕜 ≤ r * ‖(v : F)‖ * ‖(w : F)‖ := by
@@ -221,7 +221,7 @@ theorem norm_shift_apply_le_of_form_bounds
   rcases eq_or_lt_of_le (norm_nonneg (S u)) with h0 | h0
   · rw [← h0]
     exact mul_nonneg hr0 (norm_nonneg _)
-  · nlinarith
+  · nlinarith only [hkey, h0]
 
 /-! ## Constant-one interval/exterior closed Sylvester estimates -/
 
@@ -308,7 +308,7 @@ theorem norm_sylvester_le_of_intervalExterior
       hallz
   have hmul := mul_le_mul_of_nonneg_left hXnorm hrd.le
   rw [← mul_assoc, mul_inv_cancel₀ hrd.ne', one_mul] at hmul
-  nlinarith [norm_nonneg X]
+  nlinarith only [hmul, norm_nonneg X]
 
 omit [CompleteSpace E] [CompleteSpace F] in
 /-- Raw partial-map form of the constant-one estimate in the swapped
@@ -377,7 +377,7 @@ theorem norm_sylvester_le_of_exteriorInterval
       hbound
   have hmul := mul_le_mul_of_nonneg_left hXnorm hrd.le
   rw [← mul_assoc, mul_inv_cancel₀ hrd.ne', one_mul] at hmul
-  nlinarith [norm_nonneg X]
+  nlinarith only [hmul, norm_nonneg X]
 
 /-! ## The unbounded `sin Θ` theorem, operator norm -/
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/Convex/Majorization.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/Convex/Majorization.lean
index a68f2dca5f..090ae9e877 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/Convex/Majorization.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/Convex/Majorization.lean
@@ -6,14 +6,14 @@ Authors: Jon Crall, GPT-5.6 Thinking, Claude Fable 5, Claude Opus 5
 module
 
 public import Mathlib.Analysis.Convex.Basic
-public import Mathlib.Algebra.BigOperators.Fin
-public import Mathlib.Algebra.Order.Field.Basic
+import Mathlib.Algebra.BigOperators.Fin
+import Mathlib.Algebra.Order.Field.Basic
 public import Mathlib.Basic.Real.Basic
-public import Mathlib.Tactic.FieldSimp
+public meta import Mathlib.Tactic.FieldSimp
 public import Mathlib.Data.Fin.Tuple.Sort
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.LinearCombination
-public import Mathlib.Algebra.Order.BigOperators.Group.Finset
+public meta import Mathlib.Tactic.Linarith
+public meta import Mathlib.Tactic.LinearCombination
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
 
 /-!
 # Weak majorization and the Hardy–Littlewood–Pólya transfer lemma
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/ExponentialAbs.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/ExponentialAbs.lean
index 0343e98920..8d619a3fad 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/ExponentialAbs.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/ExponentialAbs.lean
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Crall, GPT 5.6 High
 -/
 module
+public import Mathlib.Analysis.Fourier.FourierTransform
 
-public import Mathlib.Analysis.Fourier.Inversion
+import Mathlib.Analysis.Fourier.Inversion
 
 /-!
 # The exponential Fourier transform of the two-sided absolute exponential
@@ -115,7 +116,7 @@ theorem integral_cexp_neg_mul_abs_mul_cexp
       ring
     _ = ((2 * y) / (y ^ 2 + x ^ 2) : ℝ) := by
       have hden : y ^ 2 + x ^ 2 ≠ 0 := by
-        nlinarith [sq_nonneg x]
+        nlinarith only [hy, sq_nonneg x]
       apply Complex.ext
       · rw [Complex.sub_re, Complex.div_re, Complex.div_re, Complex.ofReal_re]
         simp only [aNeg, aPos, Complex.normSq_apply, Complex.one_re, Complex.one_im,
@@ -162,7 +163,7 @@ theorem fourier_cexp_neg_two_pi_mul_abs
       norm_cast
       have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
       have hden : y ^ 2 + x ^ 2 ≠ 0 := by
-        nlinarith [sq_nonneg x]
+        nlinarith only [hy, sq_nonneg x]
       field_simp [hpi, hden]
       norm_num
       ring
@@ -205,7 +206,7 @@ theorem cauchy_fourier_isBigO_rpow_neg_two
     subst x
     norm_num at hxabs
   have hsum_pos : 0 < y ^ 2 + x ^ 2 := by
-    nlinarith [sq_pos_of_ne_zero hx0, sq_nonneg y]
+    nlinarith only [hx0, sq_pos_of_ne_zero hx0, sq_nonneg y]
   have hquot_nonneg : 0 ≤ y / (Real.pi * (y ^ 2 + x ^ 2)) := by positivity
   rw [Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg hquot_nonneg,
     Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (abs_nonneg x) _)]
@@ -217,7 +218,7 @@ theorem cauchy_fourier_isBigO_rpow_neg_two
       field_simp [Real.pi_ne_zero]
     _ ≤ (y / Real.pi) / x ^ 2 := by
       exact div_le_div_of_nonneg_left (by positivity) (sq_pos_of_ne_zero hx0)
-        (by nlinarith [sq_nonneg y])
+        (by nlinarith only [sq_nonneg y])
     _ = (y / Real.pi) * (x ^ 2)⁻¹ := div_eq_mul_inv _ _
 
 /-- Two-sided integrability of a symmetric exponential. -/
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/HaagerupZsido/Defs.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/HaagerupZsido/Defs.lean
index 202e968989..5071f361c1 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/HaagerupZsido/Defs.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/HaagerupZsido/Defs.lean
@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Crall, GPT 5.6 High
 -/
 module
+public import Mathlib.MeasureTheory.Integral.Bochner.Basic
+public import Mathlib.MeasureTheory.Measure.Haar.OfBasis
 
-public import Mathlib.MeasureTheory.Integral.ExpDecay
+import Mathlib.MeasureTheory.Integral.ExpDecay
 
 /-!
 # The Haagerup--Zsidó kernel: definitions and elementary API
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/HaagerupZsido/Fourier.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/HaagerupZsido/Fourier.lean
index f7217ef600..617954f195 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/HaagerupZsido/Fourier.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/HaagerupZsido/Fourier.lean
@@ -5,6 +5,11 @@ Authors: Jon Crall, GPT 5.6 High
 -/
 module
 
+import Mathlib.MeasureTheory.Group.Integral
+import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
+import Mathlib.MeasureTheory.Integral.Prod
+import Mathlib.MeasureTheory.Measure.Lebesgue.Integral
+
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.Fourier.ExponentialAbs
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.Fourier.HaagerupZsido.Defs
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.SpecialFunctions.Integral.RationalQuadratic
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/HaagerupZsido/Integrability.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/HaagerupZsido/Integrability.lean
index aa7ebca8e7..5483b02a78 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/HaagerupZsido/Integrability.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/HaagerupZsido/Integrability.lean
@@ -5,6 +5,9 @@ Authors: Jon Crall, GPT 5.6 High
 -/
 module
 
+import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
+import Mathlib.MeasureTheory.Integral.Prod
+
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.Fourier.HaagerupZsido.Defs
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.SpecialFunctions.Integral.SineLaplace
 
@@ -47,7 +50,7 @@ private theorem weight_mul_exp_ratio {y : ℝ} (hy : 0 < y) :
     weight y * ((1 + Real.exp (-Real.pi * y)) /
       (1 - Real.exp (-Real.pi * y))) = 1 := by
   have hq1 : Real.exp (-(Real.pi * y)) < 1 :=
-    Real.exp_lt_one_iff.mpr (by nlinarith [Real.pi_pos])
+    Real.exp_lt_one_iff.mpr (by nlinarith only [hy, Real.pi_pos])
   have hne : 1 - Real.exp (-(Real.pi * y)) ≠ 0 := by linarith
   have hpos : (0 : ℝ) < 1 + Real.exp (-(Real.pi * y)) := by positivity
   rw [weight_eq_exp_quotient, show -Real.pi * y = -(Real.pi * y) by ring]
@@ -75,7 +78,7 @@ theorem integrable_kernel_prod :
     filter_upwards [ae_restrict_mem measurableSet_Ioi] with y hy
     have hy0 : (0 : ℝ) < y := hy
     have hq1 : Real.exp (-Real.pi * y) < 1 :=
-      Real.exp_lt_one_iff.mpr (by nlinarith [Real.pi_pos])
+      Real.exp_lt_one_iff.mpr (by nlinarith only [hy0, Real.pi_pos])
     have hne : 1 - Real.exp (-Real.pi * y) ≠ 0 := by linarith
     have hy2 : (1 : ℝ) + y ^ 2 ≠ 0 := by positivity
     calc
@@ -110,7 +113,7 @@ private theorem integral_abs_sin_mul_weightLaplaceTransform :
         intro y hy
         have hy0 : (0 : ℝ) < y := hy
         have hq1 : Real.exp (-Real.pi * y) < 1 :=
-          Real.exp_lt_one_iff.mpr (by nlinarith [Real.pi_pos])
+          Real.exp_lt_one_iff.mpr (by nlinarith only [hy0, Real.pi_pos])
         have hne : 1 - Real.exp (-Real.pi * y) ≠ 0 := by linarith
         have hy2 : (1 : ℝ) + y ^ 2 ≠ 0 := by positivity
         dsimp only
@@ -177,7 +180,7 @@ private theorem integrable_realKernel : Integrable realKernel := by
   rw [Real.norm_eq_abs, abs_realKernel]
   have h1 := weightLaplaceTransform_nonneg t
   have h2 := abs_nonneg (Real.sin t)
-  nlinarith
+  nlinarith only [h1, h2]
 
 /-- The reciprocal kernel is integrable. -/
 theorem integrable_reciprocalKernel : Integrable reciprocalKernel := by
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/Poisson/CauchyLattice.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/Poisson/CauchyLattice.lean
index 524d6d42d6..bee5ff6390 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/Poisson/CauchyLattice.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/Fourier/Poisson/CauchyLattice.lean
@@ -5,8 +5,8 @@ Authors: Jon Crall, GPT 5.6 High
 -/
 module
 
-public import Mathlib.Analysis.Fourier.PoissonSummation
-public import Mathlib.Analysis.PSeries
+import Mathlib.Analysis.Fourier.PoissonSummation
+import Mathlib.Analysis.PSeries
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.Fourier.ExponentialAbs
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.Fourier.HaagerupZsido.Defs
 
@@ -209,7 +209,7 @@ private theorem tsum_int_inv_sq_add_sq
         intro n
         norm_cast
         have hden : y ^ 2 + (n : ℝ) ^ 2 ≠ 0 := by
-          nlinarith [sq_nonneg (n : ℝ)]
+          nlinarith only [hy, sq_nonneg (n : ℝ)]
         field_simp [Real.pi_ne_zero, hden]
       _ = ((y / Real.pi : ℝ) : ℂ) *
           ∑' n : ℤ, (((y ^ 2 + (n : ℝ) ^ 2)⁻¹ : ℝ) : ℂ) := tsum_mul_left
@@ -242,7 +242,7 @@ private theorem summable_nat_inv_sq_add_sq (y : ℝ) :
     · intro n
       have hbase : 0 < (((n + 1 : ℕ) : ℝ) ^ 2) := by positivity
       have hden : 0 < y ^ 2 + ((n + 1 : ℕ) : ℝ) ^ 2 := by positivity
-      exact (inv_le_inv₀ hden hbase).2 (by nlinarith [sq_nonneg y])
+      exact (inv_le_inv₀ hden hbase).2 (by nlinarith only [sq_nonneg y])
     · exact hmajor
   apply (summable_nat_add_iff 1).mp
   exact htail
@@ -276,7 +276,7 @@ private theorem tsum_nat_inv_sq_add_sq
   simp only [fNat, Nat.cast_zero, Nat.cast_add, Nat.cast_one] at hNatSplit
   have hzero : (y ^ 2 + (0 : ℝ) ^ 2)⁻¹ = y⁻¹ ^ 2 := by simp [inv_pow]
   rw [hzero] at hIntSplit hNatSplit
-  nlinarith
+  nlinarith only [hLattice, hIntSplit, hNatSplit]
 
 /-- The positive odd part of the Cauchy lattice. -/
 private theorem tsum_odd_inv_sq_add_sq
@@ -299,9 +299,9 @@ private theorem tsum_odd_inv_sq_add_sq
     intro n
     dsimp only [f]
     have hdenLeft : y ^ 2 + ((2 * n : ℕ) : ℝ) ^ 2 ≠ 0 := by
-      nlinarith [sq_nonneg (((2 * n : ℕ) : ℝ))]
+      nlinarith only [hy, sq_nonneg (((2 * n : ℕ) : ℝ))]
     have hdenRight : (y / 2) ^ 2 + (n : ℝ) ^ 2 ≠ 0 := by
-      nlinarith [sq_nonneg (n : ℝ)]
+      nlinarith only [hy, sq_nonneg (n : ℝ)]
     field_simp [hdenLeft, hdenRight]
     norm_num
     ring
@@ -316,7 +316,7 @@ private theorem tsum_odd_inv_sq_add_sq
   rw [hAllValue, hHalfValue] at hOddEq
   let r : ℝ := Real.exp (-(Real.pi * y))
   have hrpos : 0 < r := Real.exp_pos _
-  have hrlt : r < 1 := Real.exp_lt_one_iff.mpr (by nlinarith [Real.pi_pos])
+  have hrlt : r < 1 := Real.exp_lt_one_iff.mpr (by nlinarith only [hy, Real.pi_pos])
   have hFullExp : Real.exp (-(2 * Real.pi * y)) = r ^ 2 := by
     rw [← Real.exp_nat_mul]
     congr 1
@@ -345,7 +345,7 @@ private theorem tsum_odd_inv_sq_add_sq
         hInvHalf]
       have hOneSub : 1 - r ≠ 0 := by linarith
       have hOneAdd : 1 + r ≠ 0 := by positivity
-      have hSq : 1 - r ^ 2 ≠ 0 := by nlinarith
+      have hSq : 1 - r ^ 2 ≠ 0 := by nlinarith only [hrpos, hrlt]
       field_simp [hy.ne', hOneSub, hOneAdd, hSq]
       ring
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/AlignedBasis.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/AlignedBasis.lean
index eab34ac869..2931932500 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/AlignedBasis.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/AlignedBasis.lean
@@ -19,8 +19,9 @@ orthonormal family, used to build the `d × d` overlap operator whose singular
 values are the principal-angle cosines.
 -/
 module
+public import Mathlib.Analysis.InnerProductSpace.SingularValues
 
-public import Mathlib.LinearAlgebra.Basis.Defs
+import Mathlib.LinearAlgebra.Basis.Defs
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.Singular.Subspace
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.Gram.Matrix
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BasisSpan.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BasisSpan.lean
index c20cd2c885..6afa2a9d82 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BasisSpan.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BasisSpan.lean
@@ -20,7 +20,7 @@ only the fragments the Courant–Fischer proofs needed.
 module
 
 public import Mathlib.Analysis.InnerProductSpace.PiL2
-public import Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
+import Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
 
 /-! # Spans of orthonormal subfamilies
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BorelCalculus/Multiplicative.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BorelCalculus/Multiplicative.lean
index eb5ea7e823..24265db27c 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BorelCalculus/Multiplicative.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BorelCalculus/Multiplicative.lean
@@ -500,10 +500,10 @@ theorem norm_borelCalculus_apply_le (hf : IsBddMeasurable f) {M : ℝ} (hM : 0 
     intro x
     rw [Complex.mul_re, Complex.conj_re, Complex.conj_im]
     have h := hfb x
-    have hnn : ‖f x‖ ^ 2 ≤ M ^ 2 := by nlinarith [norm_nonneg (f x)]
+    have hnn : ‖f x‖ ^ 2 ≤ M ^ 2 := by nlinarith only [hM, h, norm_nonneg (f x)]
     have : ‖f x‖ ^ 2 = (f x).re ^ 2 + (f x).im ^ 2 := by
       rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]; ring
-    nlinarith
+    nlinarith only [hnn, this]
   have hbound : ∫ x, ((starRingEnd ℂ) (f x) * f x).re ∂(diagMeasure ha ξ)
       ≤ M ^ 2 * ‖ξ‖ ^ 2 := by
     calc ∫ x, ((starRingEnd ℂ) (f x) * f x).re ∂(diagMeasure ha ξ)
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BorelCalculus/Operator.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BorelCalculus/Operator.lean
index 1a04b838ac..28dde94f94 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BorelCalculus/Operator.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BorelCalculus/Operator.lean
@@ -273,7 +273,7 @@ theorem norm_pair_le_crude (hfm : Measurable f) {M : ℝ} (hM : 0 ≤ M)
     linarith
   have hgoal : M * ‖ξ + ψ‖ ^ 2 + M * ‖ξ + Complex.I • ψ‖ ^ 2
       + M * ‖ξ - ψ‖ ^ 2 + M * ‖ξ - Complex.I • ψ‖ ^ 2
-      = 4 * (M * (‖ψ‖ ^ 2 + ‖ξ‖ ^ 2)) := by nlinarith [hpar1, hpar2]
+      = 4 * (M * (‖ψ‖ ^ 2 + ‖ξ‖ ^ 2)) := by nlinarith only [hM, hpar1, hpar2, hpar1, hpar2]
   calc 1 / 4 * _ ≤ 1 / 4 * (4 * (M * (‖ψ‖ ^ 2 + ‖ξ‖ ^ 2))) := by
         rw [← hgoal]; gcongr
     _ = M * (‖ψ‖ ^ 2 + ‖ξ‖ ^ 2) := by ring
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/CoerciveUnit.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/CoerciveUnit.lean
index a434043fca..5b0bf0a1d2 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/CoerciveUnit.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/CoerciveUnit.lean
@@ -71,7 +71,8 @@ theorem norm_smul_le_norm_apply_of_coercive {N : E →L[𝕜] E} {c : ℝ}
       calc RCLike.re ⟪N z, z⟫_𝕜 ≤ ‖⟪N z, z⟫_𝕜‖ := RCLike.re_le_norm _
         _ ≤ ‖N z‖ * ‖z‖ := norm_inner_le_norm _ _
     have hzpos : (0 : ℝ) < ‖z‖ := norm_pos_iff.mpr hz
-    have h3 : c * ‖z‖ * ‖z‖ ≤ ‖N z‖ * ‖z‖ := by nlinarith
+    have h3 : c * ‖z‖ * ‖z‖ ≤ ‖N z‖ * ‖z‖ := by
+      simpa only [pow_two, mul_assoc] using h1.trans h2
     exact le_of_mul_le_mul_right h3 hzpos
 
 /-- Operator Lax–Milgram: a uniformly coercive bounded operator on a Hilbert
@@ -79,43 +80,36 @@ space is a unit of the algebra of bounded operators. -/
 theorem isUnit_of_coercive {N : E →L[𝕜] E} {c : ℝ} (hc : 0 < c)
     (hcoer : ∀ z, c * ‖z‖ ^ 2 ≤ RCLike.re ⟪N z, z⟫_𝕜) : IsUnit N := by
   have hlow := norm_smul_le_norm_apply_of_coercive hcoer
+  have hanti : AntilipschitzWith (Real.toNNReal c)⁻¹ N := by
+    refine ContinuousLinearMap.antilipschitz_of_bound N ?_
+    intro x
+    have hcoe : (((Real.toNNReal c)⁻¹ : NNReal) : ℝ) = c⁻¹ := by
+      rw [NNReal.coe_inv, Real.coe_toNNReal c hc.le]
+    rw [hcoe, le_inv_mul_iff₀ hc]
+    exact hlow x
   rw [ContinuousLinearMap.isUnit_iff_bijective]
-  constructor
-  · intro a b hab
-    have h1 : N (a - b) = 0 := by rw [map_sub, hab, sub_self]
-    have h2 := hlow (a - b)
-    rw [h1, norm_zero] at h2
-    have h3 : ‖a - b‖ ≤ 0 := by nlinarith [norm_nonneg (a - b)]
-    rw [← sub_eq_zero]
-    exact norm_le_zero_iff.mp h3
-  · have hanti : AntilipschitzWith (Real.toNNReal c)⁻¹ N := by
-      refine ContinuousLinearMap.antilipschitz_of_bound N ?_
-      intro x
-      have hcoe : (((Real.toNNReal c)⁻¹ : NNReal) : ℝ) = c⁻¹ := by
-        rw [NNReal.coe_inv, Real.coe_toNNReal c hc.le]
-      rw [hcoe, le_inv_mul_iff₀ hc]
-      exact hlow x
-    have hclosed :
-        IsClosed ((LinearMap.range (N : E →ₗ[𝕜] E) : Submodule 𝕜 E) : Set E) := by
-      rw [LinearMap.coe_range]
-      exact hanti.isClosed_range N.uniformContinuous
-    have : CompleteSpace (LinearMap.range (N : E →ₗ[𝕜] E)) :=
-      hclosed.completeSpace_coe
-    have : (LinearMap.range (N : E →ₗ[𝕜] E)).HasOrthogonalProjection :=
-      Submodule.HasOrthogonalProjection.ofCompleteSpace _
-    have hrange : LinearMap.range (N : E →ₗ[𝕜] E) = ⊤ := by
-      rw [← Submodule.orthogonal_eq_bot_iff, Submodule.eq_bot_iff]
-      intro z hz
-      have h0 : ⟪N z, z⟫_𝕜 = 0 :=
-        (Submodule.mem_orthogonal _ z).mp hz (N z)
-          (LinearMap.mem_range.mpr ⟨z, rfl⟩)
-      have h1 := hcoer z
-      rw [h0, map_zero] at h1
-      have h2 : ‖z‖ ^ 2 ≤ 0 := by nlinarith
-      have h3 : ‖z‖ = 0 :=
-        (pow_eq_zero_iff two_ne_zero).mp (le_antisymm h2 (sq_nonneg _))
-      exact norm_eq_zero.mp h3
-    exact LinearMap.range_eq_top.mp hrange
+  refine ⟨hanti.injective, ?_⟩
+  have hclosed :
+      IsClosed ((LinearMap.range (N : E →ₗ[𝕜] E) : Submodule 𝕜 E) : Set E) := by
+    rw [LinearMap.coe_range]
+    exact hanti.isClosed_range N.uniformContinuous
+  have : CompleteSpace (LinearMap.range (N : E →ₗ[𝕜] E)) :=
+    hclosed.completeSpace_coe
+  have : (LinearMap.range (N : E →ₗ[𝕜] E)).HasOrthogonalProjection :=
+    Submodule.HasOrthogonalProjection.ofCompleteSpace _
+  have hrange : LinearMap.range (N : E →ₗ[𝕜] E) = ⊤ := by
+    rw [← Submodule.orthogonal_eq_bot_iff, Submodule.eq_bot_iff]
+    intro z hz
+    have h0 : ⟪N z, z⟫_𝕜 = 0 :=
+      (Submodule.mem_orthogonal _ z).mp hz (N z)
+        (LinearMap.mem_range.mpr ⟨z, rfl⟩)
+    have h1 := hcoer z
+    rw [h0, map_zero] at h1
+    have h2 : ‖z‖ ^ 2 ≤ 0 := nonpos_of_mul_nonpos_right h1 hc
+    have h3 : ‖z‖ = 0 :=
+      (pow_eq_zero_iff two_ne_zero).mp (le_antisymm h2 (sq_nonneg _))
+    exact norm_eq_zero.mp h3
+  exact LinearMap.range_eq_top.mp hrange
 
 /-- `1 + W⋆ W` is invertible for every bounded Hilbert-space operator `W`:
 its quadratic form dominates `‖z‖ ^ 2`, so the operator Lax–Milgram lemma
@@ -126,8 +120,18 @@ theorem isUnit_one_add_star_mul_self (W : E →L[𝕜] E) :
   have h : (1 + star W * W) z = z + star W (W z) := rfl
   rw [h]
   simp only [inner_add_left, map_add, inner_self_eq_norm_sq,
-    ContinuousLinearMap.star_eq_adjoint, ContinuousLinearMap.adjoint_inner_left]
-  nlinarith [sq_nonneg ‖W z‖]
+    ContinuousLinearMap.star_eq_adjoint, ContinuousLinearMap.adjoint_inner_left, one_mul]
+  exact le_add_of_nonneg_right (sq_nonneg ‖W z‖)
+
+omit [CompleteSpace E] in
+/-- Cauchy--Schwarz bound on the quadratic form of a bounded operator. -/
+private theorem re_inner_apply_self_le_norm_mul_sq (B : E →L[𝕜] E) (y : E) :
+    RCLike.re ⟪B y, y⟫_𝕜 ≤ ‖B‖ * ‖y‖ ^ 2 := by
+  calc RCLike.re ⟪B y, y⟫_𝕜 ≤ ‖⟪B y, y⟫_𝕜‖ := RCLike.re_le_norm _
+    _ ≤ ‖B y‖ * ‖y‖ := norm_inner_le_norm _ _
+    _ ≤ (‖B‖ * ‖y‖) * ‖y‖ :=
+        mul_le_mul_of_nonneg_right (B.le_opNorm y) (norm_nonneg _)
+    _ = ‖B‖ * ‖y‖ ^ 2 := by ring
 
 omit [CompleteSpace E] in
 /-- Cauchy–Schwarz for the semi-inner product induced by a positive symmetric
@@ -159,18 +163,15 @@ theorem norm_apply_sq_le_of_positive {B : E →L[𝕜] E}
       rw [h1] at h0
       simpa [map_sub, map_add, RCLike.re_ofReal_mul, inner_self_eq_norm_sq]
         using h0
-    have h3 : RCLike.re ⟪B (B y), B y⟫_𝕜 ≤ ‖B‖ * ‖B y‖ ^ 2 := by
-      calc RCLike.re ⟪B (B y), B y⟫_𝕜 ≤ ‖⟪B (B y), B y⟫_𝕜‖ := RCLike.re_le_norm _
-        _ ≤ ‖B (B y)‖ * ‖B y‖ := norm_inner_le_norm _ _
-        _ ≤ (‖B‖ * ‖B y‖) * ‖B y‖ :=
-            mul_le_mul_of_nonneg_right (B.le_opNorm (B y)) (norm_nonneg _)
-        _ = ‖B‖ * ‖B y‖ ^ 2 := by ring
+    have h3 : RCLike.re ⟪B (B y), B y⟫_𝕜 ≤ ‖B‖ * ‖B y‖ ^ 2 :=
+      re_inner_apply_self_le_norm_mul_sq B (B y)
     have key : t * (t * RCLike.re ⟪B (B y), B y⟫_𝕜) ≤ t * ‖B y‖ ^ 2 := by
       refine mul_le_mul_of_nonneg_left ?_ ht.le
       calc t * RCLike.re ⟪B (B y), B y⟫_𝕜 ≤ t * (‖B‖ * ‖B y‖ ^ 2) :=
             mul_le_mul_of_nonneg_left h3 ht.le
         _ = ‖B y‖ ^ 2 := by rw [← mul_assoc, hts, one_mul]
-    have h7 : t * ‖B y‖ ^ 2 ≤ RCLike.re ⟪B y, y⟫_𝕜 := by linarith
+    have h7 : t * ‖B y‖ ^ 2 ≤ RCLike.re ⟪B y, y⟫_𝕜 := by
+      linarith only [h2, key]
     calc ‖B y‖ ^ 2 = ‖B‖ * (t * ‖B y‖ ^ 2) := by
           rw [← mul_assoc, mul_comm ‖B‖ t, hts, one_mul]
       _ ≤ ‖B‖ * RCLike.re ⟪B y, y⟫_𝕜 :=
@@ -189,7 +190,8 @@ private lemma div_one_add_le_of_sq_le {c d K : ℝ} (hc : 0 ≤ c)
   have hd : 0 ≤ d := le_trans (sq_nonneg c) hcd
   have hD : (0 : ℝ) < 1 + 2 * c + d := by linarith
   rw [div_le_iff₀ (by linarith : (0 : ℝ) < 1 + c)]
-  have h9 : c * (1 + 2 * c + d) ≤ (c + d) * (1 + c) := by nlinarith [hcd]
+  have h9 : c * (1 + 2 * c + d) ≤ (c + d) * (1 + c) := by
+    linear_combination hcd
   have h10 : c * (1 + 2 * c + d) ≤ (K * (1 + c)) * (1 + 2 * c + d) := by
     calc c * (1 + 2 * c + d) ≤ (c + d) * (1 + c) := h9
       _ ≤ (K * (1 + 2 * c + d)) * (1 + c) :=
@@ -204,7 +206,8 @@ Pure real analysis; `b = ‖B‖` at the use site. -/
 private lemma tendsto_sub_sq_div_add_sub_sq {b : ℝ} (hb : 0 < b) :
     Filter.Tendsto (fun ε : ℝ => (b - ε) ^ 2 / (b + (b - ε) ^ 2))
       (nhdsWithin 0 (Set.Ioo 0 b)) (nhds (b / (1 + b))) := by
-  have hden : b + (b - 0) ^ 2 ≠ 0 := by nlinarith
+  have hden : b + (b - 0) ^ 2 ≠ 0 :=
+    ne_of_gt (add_pos_of_pos_of_nonneg hb (sq_nonneg _))
   have h1 : Filter.Tendsto (fun ε : ℝ => (b - ε) ^ 2 / (b + (b - ε) ^ 2))
       (nhds 0) (nhds ((b - 0) ^ 2 / (b + (b - 0) ^ 2))) := by
     refine Filter.Tendsto.div ?_ ?_ hden
@@ -212,7 +215,9 @@ private lemma tendsto_sub_sq_div_add_sub_sq {b : ℝ} (hb : 0 < b) :
     · exact ((continuous_const.add
         ((continuous_const.sub continuous_id).pow 2)).tendsto 0)
   have h2 : (b - 0) ^ 2 / (b + (b - 0) ^ 2) = b / (1 + b) := by
-    rw [sub_zero, div_eq_div_iff (by nlinarith) (by linarith)]
+    rw [sub_zero, div_eq_div_iff
+      (ne_of_gt (add_pos_of_pos_of_nonneg hb (sq_nonneg _)))
+      (ne_of_gt (add_pos_of_pos_of_nonneg zero_lt_one hb.le))]
     ring
   rw [← h2]
   exact h1.mono_left nhdsWithin_le_nhds
@@ -234,16 +239,6 @@ private theorem div_one_add_le_of_forall_sub_sq_le {b K : ℝ} (hb : 0 < b)
   exact le_of_tendsto hcont
     (by filter_upwards [self_mem_nhdsWithin] with ε hε using h ε hε)
 
-omit [CompleteSpace E] in
-/-- Cauchy--Schwarz bound on the quadratic form of a bounded operator. -/
-private theorem re_inner_apply_self_le_norm_mul_sq (B : E →L[𝕜] E) (y : E) :
-    RCLike.re ⟪B y, y⟫_𝕜 ≤ ‖B‖ * ‖y‖ ^ 2 := by
-  calc RCLike.re ⟪B y, y⟫_𝕜 ≤ ‖⟪B y, y⟫_𝕜‖ := RCLike.re_le_norm _
-    _ ≤ ‖B y‖ * ‖y‖ := norm_inner_le_norm _ _
-    _ ≤ (‖B‖ * ‖y‖) * ‖y‖ :=
-        mul_le_mul_of_nonneg_right (B.le_opNorm y) (norm_nonneg _)
-    _ = ‖B‖ * ‖y‖ ^ 2 := by ring
-
 omit [CompleteSpace E] in
 /-- Expansion of `‖(1 + B) y‖²`.  The two cross terms are conjugate, so they add to twice the real
 part — no self-adjointness of `B` is needed, only conjugate symmetry of the inner product. -/
@@ -316,7 +311,7 @@ theorem norm_one_sub_inverse_one_add {B : E →L[𝕜] E} (hB : IsSelfAdjoint B)
       have hc := norm_apply_sq_le_of_positive hB.isSymmetric hBpos y
       rw [hval y, hNsq y, abs_of_nonneg (by positivity)]
       rw [div_mul_eq_mul_div, le_div_iff₀ (by linarith : (0 : ℝ) < 1 + ‖B‖)]
-      nlinarith [hb, hc]
+      linear_combination hb + hc
     refine norm_le_of_abs_re_inner_map_self_le hCsa.isSymmetric
       (div_nonneg hs.le (by linarith)) ?_
     intro z
@@ -334,42 +329,40 @@ theorem norm_one_sub_inverse_one_add {B : E →L[𝕜] E} (hB : IsSelfAdjoint B)
             _ ≤ ‖B u‖ * ‖u‖ := norm_inner_le_norm _ _
             _ ≤ ‖B u‖ * 1 := mul_le_mul_of_nonneg_left hu (norm_nonneg _)
             _ = ‖B u‖ := mul_one _
-        nlinarith [norm_nonneg (B u)]
-      have hCS : RCLike.re ⟪(1 - R) (N u), N u⟫_𝕜 ≤ ‖1 - R‖ * ‖N u‖ ^ 2 := by
-        calc RCLike.re ⟪(1 - R) (N u), N u⟫_𝕜
-            ≤ ‖⟪(1 - R) (N u), N u⟫_𝕜‖ := RCLike.re_le_norm _
-          _ ≤ ‖(1 - R) (N u)‖ * ‖N u‖ := norm_inner_le_norm _ _
-          _ ≤ (‖1 - R‖ * ‖N u‖) * ‖N u‖ :=
-              mul_le_mul_of_nonneg_right ((1 - R).le_opNorm _) (norm_nonneg _)
-          _ = ‖1 - R‖ * ‖N u‖ ^ 2 := by ring
+        exact pow_le_pow_left₀ hb0 h1 2
+      have hCS : RCLike.re ⟪(1 - R) (N u), N u⟫_𝕜 ≤ ‖1 - R‖ * ‖N u‖ ^ 2 :=
+        re_inner_apply_self_le_norm_mul_sq (1 - R) (N u)
       rw [hval u, hNsq u] at hCS
-      have husq : ‖u‖ ^ 2 ≤ 1 := by nlinarith [norm_nonneg u]
+      have husq : ‖u‖ ^ 2 ≤ 1 := by
+        simpa only [one_pow] using pow_le_pow_left₀ (norm_nonneg u) hu 2
       have hK0 : (0 : ℝ) ≤ ‖1 - R‖ := norm_nonneg _
       have h8 : RCLike.re ⟪B u, u⟫_𝕜 + ‖B u‖ ^ 2
           ≤ ‖1 - R‖ * (1 + 2 * RCLike.re ⟪B u, u⟫_𝕜 + ‖B u‖ ^ 2) := by
-        nlinarith [hCS]
+        linear_combination hCS + ‖1 - R‖ * husq
       exact div_one_add_le_of_sq_le hb0 hc2 h8
     have hstep2 : ∀ ε ∈ Set.Ioo (0 : ℝ) ‖B‖,
         (‖B‖ - ε) ^ 2 / (‖B‖ + (‖B‖ - ε) ^ 2) ≤ ‖1 - R‖ := by
       intro ε hε
       obtain ⟨u, hu1, hu2⟩ :=
-        B.exists_lt_apply_of_lt_opNorm (r := ‖B‖ - ε) (by linarith [hε.1])
+        B.exists_lt_apply_of_lt_opNorm (r := ‖B‖ - ε) (sub_lt_self _ hε.1)
       have hb0 := hBpos u
       have hcs := norm_apply_sq_le_of_positive hB.isSymmetric hBpos u
       have hbge : (‖B‖ - ε) ^ 2 / ‖B‖ ≤ RCLike.re ⟪B u, u⟫_𝕜 := by
         rw [div_le_iff₀ hs]
         have hsq : (‖B‖ - ε) * (‖B‖ - ε) ≤ ‖B u‖ * ‖B u‖ :=
-          mul_self_le_mul_self (by linarith [hε.2]) hu2.le
-        nlinarith [hcs, hsq]
+          mul_self_le_mul_self (sub_pos.mpr hε.2).le hu2.le
+        have hsq' : (‖B‖ - ε) ^ 2 ≤ ‖B u‖ ^ 2 := by
+          simpa only [pow_two] using hsq
+        simpa only [mul_comm] using hsq'.trans hcs
       have hmono := hstep u hu1.le
       have hmono2 : (‖B‖ - ε) ^ 2 / (‖B‖ + (‖B‖ - ε) ^ 2)
           ≤ RCLike.re ⟪B u, u⟫_𝕜 / (1 + RCLike.re ⟪B u, u⟫_𝕜) := by
         have hr2 : (‖B‖ - ε) ^ 2 ≤ RCLike.re ⟪B u, u⟫_𝕜 * ‖B‖ := by
-          rw [div_le_iff₀ hs] at hbge
-          linarith
-        rw [div_le_div_iff₀ (by nlinarith [sq_nonneg (‖B‖ - ε)]) (by linarith)]
-        nlinarith [hr2, sq_nonneg (‖B‖ - ε)]
-      linarith
+          rwa [div_le_iff₀ hs] at hbge
+        rw [div_le_div_iff₀ (add_pos_of_pos_of_nonneg hs (sq_nonneg _))
+          (add_pos_of_pos_of_nonneg zero_lt_one hb0)]
+        linear_combination hr2
+      exact hmono2.trans hmono
     exact div_one_add_le_of_forall_sub_sq_le hs hstep2
   exact le_antisymm hupper hlower
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Complexification/Basic.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Complexification/Basic.lean
index 287b9db19b..4061b0bb91 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Complexification/Basic.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Complexification/Basic.lean
@@ -24,9 +24,9 @@ Authors: Jon Crall, GPT-5.6 Thinking
 module
 
 public import Mathlib.Algebra.Module.MinimalAxioms
-public import Mathlib.Analysis.InnerProductSpace.ProdL2
+import Mathlib.Analysis.InnerProductSpace.ProdL2
 public import Mathlib.Analysis.InnerProductSpace.Adjoint
-public import Mathlib.Analysis.Normed.Operator.Banach
+import Mathlib.Analysis.Normed.Operator.Banach
 
 /-!
 # Complexification of real Hilbert spaces
@@ -443,7 +443,7 @@ theorem norm_complexify [NormedAddCommGroup E] [InnerProductSpace ℝ E]
           (T.le_opNorm _)
       change ‖T (re z)‖ ^ 2 + ‖T (im z)‖ ^ 2 ≤
         ‖T‖ ^ 2 * (‖re z‖ ^ 2 + ‖im z‖ ^ 2)
-      nlinarith
+      nlinarith only [hre, him]
   · refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_
     simpa using (complexify T).le_opNorm (ofReal x)
 
@@ -498,7 +498,7 @@ deleted the remaining copies and made this one public, which is the state descri
 theorem norm_re_le [NormedAddCommGroup E] (z : RealComplexification E) :
     ‖re z‖ ≤ ‖z‖ := by
   have h := norm_sq z
-  nlinarith [norm_nonneg (re z), norm_nonneg (im z), norm_nonneg z]
+  nlinarith only [h, norm_nonneg (re z), norm_nonneg (im z), norm_nonneg z]
 
 /-- **Restrict a complex operator to the real copy and take its real
 coordinate.**  No invariance assumption is needed to define this: the map is
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Complexification/FunctionalCalculus.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Complexification/FunctionalCalculus.lean
index 5f9a9a3e49..ad0f7a89a6 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Complexification/FunctionalCalculus.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Complexification/FunctionalCalculus.lean
@@ -4,14 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Crall, OpenAI GPT-5.6 Thinking
 -/
 module
+public import Mathlib.Analysis.InnerProductSpace.Positive
+public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
+public import Mathlib.Analysis.CStarAlgebra.Classes
 
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.Complexification.Basic
-public import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
-public import Mathlib.Analysis.InnerProductSpace.StarOrder
-public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
-public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
-public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
-public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
+import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
+import Mathlib.Analysis.InnerProductSpace.StarOrder
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
 
 /-!
 # Real descent for bounded functional calculus
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/CourantFischer.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/CourantFischer.lean
index 1024901ffb..0a4e05261d 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/CourantFischer.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/CourantFischer.lean
@@ -23,9 +23,9 @@ To be re-authored per upstream AI-contribution policy at PR time.
 -/
 module
 
-public import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.Analysis.InnerProductSpace.PiL2
 public import Mathlib.Analysis.InnerProductSpace.Spectrum
-public import Mathlib.Analysis.InnerProductSpace.Adjoint
+import Mathlib.Analysis.InnerProductSpace.Adjoint
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.BasisSpan
 
 /-! # Courant–Fischer min-max and Weyl's eigenvalue perturbation inequality
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/DoubleAngle/UnboundedPole.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/DoubleAngle/UnboundedPole.lean
index b537520d11..479615037f 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/DoubleAngle/UnboundedPole.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/DoubleAngle/UnboundedPole.lean
@@ -210,7 +210,7 @@ theorem crossBlockBound_lt_one {δ nB : ℝ} (hδ : 0 < δ) (hnB : 0 ≤ nB) :
   have hD2 : √(δ ^ 2 + 4 * nB ^ 2) ^ 2 = δ ^ 2 + 4 * nB ^ 2 :=
     Real.sq_sqrt (by positivity)
   rw [crossBlockBound_eq, div_lt_one hD]
-  nlinarith [hD, hD2, hnB, hδ]
+  nlinarith only [hδ, hnB, hD, hD2, hD, hD2, hnB, hδ]
 
 /-- The scalar step from the cross-block bound to the diagonal-block bound:
 `c² + s² = n²` and `s ≤ (2β/D) n` give `(δ/D) n ≤ c`, where `D² = δ² + 4β²`. -/
@@ -271,7 +271,7 @@ private theorem gap_mul_le_of_cross {δ nB s nx nC : ℝ} (hnB : 0 ≤ nB)
       _ = 4 * nB ^ 2 * nx ^ 2 := by field_simp
   have hsq : (δ * s) ^ 2 ≤ (2 * nB * nC) ^ 2 := by
     rw [hD2] at hmul
-    nlinarith [hmul, hpy]
+    nlinarith only [hpy, hmul, hmul, hpy]
   calc δ * s = √((δ * s) ^ 2) := (Real.sqrt_sq (by positivity)).symm
     _ ≤ √((2 * nB * nC) ^ 2) := Real.sqrt_le_sqrt hsq
     _ = 2 * nB * nC := Real.sqrt_sq (by positivity)
@@ -490,7 +490,7 @@ theorem sylvester_pairing_le (Ω : BoundedCutoff A U τ) {x : H}
     have h := norm_sq_diagonalPart_add_norm_sq_offDiagonalPart_of_mem_orthogonal
       (U := U) hZnorm hyU
     rw [hy1, one_pow, ← hCdef, ← hSdef] at h
-    nlinarith [sq_nonneg ‖r‖, hSynorm]
+    nlinarith only [hSynorm, h, sq_nonneg ‖r‖, hSynorm]
   have hCxle : ‖C x‖ ≤ √(1 - q ^ 2) := by
     rw [← Real.sqrt_sq (norm_nonneg (C x)), hCxnorm]
   have hCyle : ‖C y‖ ≤ √(1 - q ^ 2) := by
@@ -562,7 +562,7 @@ private theorem le_crossBlockBound_of_mul_le {δ m t : ℝ}
     (hmain : δ * m ≤ 2 * t * √(1 - m ^ 2)) :
     m ≤ crossBlockBound δ t := by
   -- close the algebra
-  have h1m2 : 0 ≤ 1 - m ^ 2 := by nlinarith [hm1, hm0]
+  have h1m2 : 0 ≤ 1 - m ^ 2 := by nlinarith only [hm0, hm1, hm1, hm0]
   have hlhs0 : 0 ≤ δ * m := by positivity
   have hrhs : (2 * t * √(1 - m ^ 2)) ^ 2 = 4 * t ^ 2 * (1 - m ^ 2) := by
     rw [mul_pow, Real.sq_sqrt h1m2]
@@ -578,7 +578,7 @@ private theorem le_crossBlockBound_of_mul_le {δ m t : ℝ}
     ring
   have hmD : (m * D) ^ 2 ≤ (2 * t) ^ 2 := by
     rw [hmDeq]
-    nlinarith [hsq]
+    nlinarith only [hsq, hsq]
   have hfin : m * D ≤ 2 * t :=
     calc m * D = √((m * D) ^ 2) := (Real.sqrt_sq (by positivity)).symm
       _ ≤ √((2 * t) ^ 2) := Real.sqrt_le_sqrt hmD
@@ -666,11 +666,11 @@ theorem opNorm_offDiagonalPart_comp_le (Ω : BoundedCutoff A U τ) (hτ : 0 ≤
         Real.norm_eq_abs, abs_of_pos hx₀pos]
     have hinv : ‖x₀‖ * ‖x₀‖⁻¹ = 1 := mul_inv_cancel₀ hx₀pos.ne'
     have hinvge : (1 : ℝ) ≤ ‖x₀‖⁻¹ := by
-      nlinarith [hinv, hx₀le, hx₀pos, inv_pos.mpr hx₀pos]
+      nlinarith only [hx₀pos, hx₀le, hinv, hinv, hx₀le, hx₀pos, inv_pos.mpr hx₀pos]
     have hqlow : m - ε < q := by
       have h1 : ‖S x₀‖ ≤ q := by
         rw [hqval]
-        nlinarith [hinvge, hSx₀pos.le]
+        nlinarith only [hεm, hv2, hinvge, hinvge, hSx₀pos.le]
       linarith
     have hq0 : 0 < q := lt_of_le_of_lt (by linarith) hqlow
     have hqm : q ≤ m := by
@@ -692,7 +692,7 @@ theorem opNorm_offDiagonalPart_comp_le (Ω : BoundedCutoff A U τ) (hτ : 0 ≤
     have hLle : L ≤ √(2 * ε) := by
       rw [← Real.sqrt_sq hL0]
       exact Real.sqrt_le_sqrt (by linarith [hleak])
-    have h1m2 : 0 ≤ 1 - m ^ 2 := by nlinarith [hm1, hm0]
+    have h1m2 : 0 ≤ 1 - m ^ 2 := by nlinarith only [hm0, hm1, hm1, hm0]
     have hqsqrt : √(1 - q ^ 2) ≤ √(1 - m ^ 2) + √(2 * ε) := by
       refine le_trans (Real.sqrt_le_sqrt (by linarith : 1 - q ^ 2 ≤
         (1 - m ^ 2) + 2 * ε)) ?_
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/DoubleAngle/Vector.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/DoubleAngle/Vector.lean
index 28dbd25fad..a1d5e04905 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/DoubleAngle/Vector.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/DoubleAngle/Vector.lean
@@ -31,7 +31,7 @@ with no smallness assumption on the perturbation.
 module
 
 public import Mathlib.Analysis.InnerProductSpace.Projection.Basic
-public import Mathlib.Analysis.InnerProductSpace.Symmetric
+import Mathlib.Analysis.InnerProductSpace.Symmetric
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
 
 /-! # The Davis sin 2θ theorem (per-eigenvector, product form)
@@ -294,7 +294,7 @@ theorem sin_two_theta_le_of_mem (hT : T.IsSymmetric) (hH : H.IsSymmetric)
       ≤ 4 * (‖y‖ ^ 2 * ‖z‖ ^ 2) * ε := by linarith
   have h4 : (0 : ℝ) < 4 * (‖y‖ ^ 2 * ‖z‖ ^ 2) := by
     have := mul_pos hcs hcs
-    nlinarith [this]
+    nlinarith only [this, this]
   exact le_of_mul_le_mul_left hfinal h4
 
 /-- **Davis's sin 2θ theorem, per-eigenvector product form.**  Under the
@@ -341,13 +341,13 @@ theorem sin_two_arccos_le (hT : T.IsSymmetric) (hH : H.IsSymmetric)
     have h := norm_add_sq (𝕜 := 𝕜) y z
     simp only [hxsum, hx, hyz, map_zero, mul_zero, add_zero, one_pow] at h
     linarith
-  have hc1 : ‖y‖ ≤ 1 := by nlinarith [norm_nonneg y, sq_nonneg ‖z‖, sq_nonneg (‖y‖ - 1)]
+  have hc1 : ‖y‖ ≤ 1 := by nlinarith only [hpyth, norm_nonneg y, sq_nonneg ‖z‖, sq_nonneg (‖y‖ - 1)]
   rw [Real.sin_two_mul, Real.cos_arccos (by linarith [norm_nonneg y]) hc1, Real.sin_arccos]
   have hsqrt : Real.sqrt (1 - ‖y‖ ^ 2) = ‖z‖ := by
     rw [show (1 : ℝ) - ‖y‖ ^ 2 = ‖z‖ ^ 2 by linarith]
     exact Real.sqrt_sq (norm_nonneg z)
   rw [hsqrt]
-  nlinarith [hmain]
+  nlinarith only [hmain, hmain]
 
 /-- **Davis's tan 2θ theorem, orthogonal-decomposition form.**  Same setup as
 `sin_two_theta_le_of_mem`, but with the *vanishing-pinch* hypotheses: `H` has
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/EigenvalueChange.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/EigenvalueChange.lean
index 385f077b35..808ced0b36 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/EigenvalueChange.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/EigenvalueChange.lean
@@ -26,8 +26,8 @@ decomposition in `.mathlib-quality/decomposition.md`.
 -/
 module
 
-public import Mathlib.Analysis.Convex.Birkhoff
-public import Mathlib.GroupTheory.Perm.Support
+import Mathlib.Analysis.Convex.Birkhoff
+import Mathlib.GroupTheory.Perm.Support
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.SchurHorn
 
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Gram/Matrix.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Gram/Matrix.lean
index 2546baa09f..3346d885a2 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Gram/Matrix.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Gram/Matrix.lean
@@ -23,12 +23,12 @@ the span, ambient, and `gram` statements are thin corollaries.
 module
 
 public import Mathlib.Analysis.InnerProductSpace.GramMatrix
-public import Mathlib.Analysis.InnerProductSpace.PiL2
-public import Mathlib.LinearAlgebra.Isomorphisms
+import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.LinearAlgebra.Isomorphisms
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.Basic
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.Normed.Operator.LinearIsometry
-public import Mathlib.Analysis.Normed.Module.FiniteDimension
-public import Mathlib.Topology.MetricSpace.Sequences
+import Mathlib.Analysis.Normed.Module.FiniteDimension
+import Mathlib.Topology.MetricSpace.Sequences
 
 
 /-! # Gram matrix rigidity
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/IntertwiningUnitary.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/IntertwiningUnitary.lean
index 710c387ce4..66dbdec430 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/IntertwiningUnitary.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/IntertwiningUnitary.lean
@@ -17,7 +17,7 @@ Milestone 2 of the operator polar decomposition project — COMPLETE
 module
 
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.Polar.Decomposition
-public import Mathlib.Analysis.InnerProductSpace.Spectrum
+import Mathlib.Analysis.InnerProductSpace.Spectrum
 
 
 /-! # The canonical intertwining (matching) unitary (Milestone 2)
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/KyFan.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/KyFan.lean
index f7b330b370..92fe9e4c07 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/KyFan.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/KyFan.lean
@@ -218,13 +218,13 @@ private theorem sum_mul_le_sum_top {n k : ℕ} (hk : k ≤ n) {lam c : Fin n →
       intro j hj
       have hjk : (j : ℕ) < k := (Finset.mem_filter.mp hj).2
       have hle : t ≤ lam j := hlam (Fin.le_def.mpr hjk.le)
-      nlinarith [mul_nonneg (sub_nonneg.mpr hle) (sub_nonneg.mpr (h1 j))]
+      nlinarith only [h1, hle, mul_nonneg (sub_nonneg.mpr hle) (sub_nonneg.mpr (h1 j))]
     have htail : ∀ j ∈ Finset.univ.filter (fun j : Fin n => ¬ (j : ℕ) < k),
         lam j * c j ≤ t * c j := by
       intro j hj
       have hjk : ¬ (j : ℕ) < k := (Finset.mem_filter.mp hj).2
       have hle : lam j ≤ t := hlam (Fin.le_def.mpr (Nat.le_of_not_lt hjk))
-      nlinarith [mul_nonneg (sub_nonneg.mpr hle) (h0 j)]
+      nlinarith only [h0, hle, mul_nonneg (sub_nonneg.mpr hle) (h0 j)]
     have hsplit := (Finset.sum_filter_add_sum_filter_not Finset.univ
       (fun j : Fin n => (j : ℕ) < k) (fun j => lam j * c j)).symm
     have hhead_eq : ∑ j ∈ Finset.univ.filter (fun j : Fin n => (j : ℕ) < k),
@@ -363,7 +363,7 @@ private theorem re_sum_inner_map_le_sum_singularValues_square {A : E →ₗ[𝕜
     rw [hterm i, ← hquad, ← hquad]
     have h1 : RCLike.re ⟪R (W.symm (u i)), R (v i)⟫_𝕜 ≤ ‖R (W.symm (u i))‖ * ‖R (v i)‖ :=
       (RCLike.re_le_norm _).trans (norm_inner_le_norm _ _)
-    nlinarith [sq_nonneg (‖R (W.symm (u i))‖ - ‖R (v i)‖)]
+    nlinarith only [h1, sq_nonneg (‖R (W.symm (u i))‖ - ‖R (v i)‖)]
   have hu' : Orthonormal 𝕜 (fun i => W.symm (u i)) := by
     rw [orthonormal_iff_ite] at hu ⊢
     intro i j
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/RealLowerBound.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/RealLowerBound.lean
index 2c48a57f88..a15a26c610 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/RealLowerBound.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/RealLowerBound.lean
@@ -60,7 +60,7 @@ theorem injective_shiftMap_of_lower_bound (hc : 0 < c)
   have h := hbd x
   rw [show A x - z • (x : E) = shiftMap A z x from rfl, hx, norm_zero] at h
   have hx0 : ‖(x : E)‖ = 0 :=
-    le_antisymm (by nlinarith [norm_nonneg ((x : E))]) (norm_nonneg _)
+    le_antisymm (by nlinarith only [hc, h, norm_nonneg ((x : E))]) (norm_nonneg _)
   exact Subtype.ext (by simpa using hx0)
 
 /-- **Dense range, at a real point.**  A vector orthogonal to the range of
@@ -210,7 +210,7 @@ theorem norm_sub_smul_ge_of_coercive_comp
   rcases eq_or_lt_of_le (norm_nonneg ((x : E))) with h0 | h0
   · rw [← h0, mul_zero]
     exact norm_nonneg _
-  · nlinarith
+  · nlinarith only [hcs, hb, h0]
 
 /-- **A real point is a resolvent point when the shifted operator is coercive
 against a bounded isometry.**
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/SelfAdjointResolvent.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/SelfAdjointResolvent.lean
index 4d088059d1..5bfc810a4d 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/SelfAdjointResolvent.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/SelfAdjointResolvent.lean
@@ -157,7 +157,7 @@ theorem injective_shiftMap {A : E →ₗ.[ℂ] E} (hsym : A.IsFormalAdjoint A)
   have h := norm_sub_smul_ge_abs_im hsym z x
   rw [show A x - z • (x : E) = shiftMap A z x from rfl, hx, norm_zero] at h
   have hxz : ‖(x : E)‖ = 0 := by
-    nlinarith [abs_pos.mpr hz, norm_nonneg ((x : E))]
+    nlinarith only [hz, h, abs_pos.mpr hz, norm_nonneg ((x : E))]
   exact Subtype.ext (by simpa using hxz)
 
 /-- The shifted map is surjective.  This is the harder half -- it needs closed range, which comes
@@ -356,7 +356,7 @@ theorem exists_norm_le_two_sided_shifted_inverse_of_spectrum_gap
       have hsle : s ≤ ‖μ‖⁻¹ := hinvnorm ▸ hge
       have hcancel : ‖μ‖⁻¹ * ‖μ‖ = 1 := inv_mul_cancel₀ (ne_of_gt hpos)
       rw [show s⁻¹ = 1 / s by ring, le_div_iff₀ hs]
-      nlinarith [hsle, hpos, hcancel]
+      nlinarith only [hge, hinvnorm, hpos, hcancel, hsle, hpos, hcancel]
   -- for a self-adjoint element the norm *is* the spectral radius
   have hsa : _root_.IsSelfAdjoint (resolvent A (c : ℂ)) := isSelfAdjoint_resolvent_ofReal hA hc
   have hrad : spectralRadius ℂ (resolvent A (c : ℂ)) ≤ ENNReal.ofReal s⁻¹ := by
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/SpectralGrid.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/SpectralGrid.lean
index 2e14a82d6a..11c08d0ef6 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/SpectralGrid.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/SpectralGrid.lean
@@ -66,10 +66,10 @@ theorem pairwise_disjoint_gridCell (hε : 0 < ε) :
   rintro x hxk hxl
   rcases lt_or_gt_of_ne hkl with h | h
   · have hkl' : ((k : ℝ) + 1) ≤ (l : ℝ) := by exact_mod_cast Int.add_one_le_iff.mpr h
-    have : ((k : ℝ) + 1) * ε ≤ (l : ℝ) * ε := by nlinarith [hε.le]
+    have : ((k : ℝ) + 1) * ε ≤ (l : ℝ) * ε := by nlinarith only [hε, hkl', hε.le]
     exact absurd (lt_of_lt_of_le hxk.2 this) (not_lt.mpr hxl.1)
   · have hlk' : ((l : ℝ) + 1) ≤ (k : ℝ) := by exact_mod_cast Int.add_one_le_iff.mpr h
-    have : ((l : ℝ) + 1) * ε ≤ (k : ℝ) * ε := by nlinarith [hε.le]
+    have : ((l : ℝ) + 1) * ε ≤ (k : ℝ) * ε := by nlinarith only [hε, hlk', hε.le]
     exact absurd (lt_of_lt_of_le hxl.2 this) (not_lt.mpr hxk.1)
 
 /-- The cells cover the line. -/
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/SpectralSupport.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/SpectralSupport.lean
index 85a6276132..be5b7a8dcf 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/SpectralSupport.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LinearPMap/SpectralSupport.lean
@@ -87,7 +87,7 @@ theorem specProjection_eq_zero_of_norm_resolvent_mul_lt_one
   have hx0 : ‖x‖ = 0 := by
     by_contra hne
     have hpos : 0 < ‖x‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hne)
-    nlinarith [norm_nonneg (resolvent A (c : ℂ))]
+    nlinarith only [hsmall, hnx, hpos, norm_nonneg (resolvent A (c : ℂ))]
   simpa [hxdef] using norm_eq_zero.mp hx0
 
 /-- **The diagonal measures are supported on the spectrum.**  A Borel set of
@@ -122,8 +122,8 @@ theorem diag_eq_zero_of_subset_resolventSet
     · have h := hs.2
       rw [abs_le]
       constructor
-      · nlinarith [neg_abs_le lam, h.1]
-      · nlinarith [le_abs_self lam, h.2]
+      · nlinarith only [h, neg_abs_le lam, h.1]
+      · nlinarith only [h, le_abs_self lam, h.2]
     · have h := hs.2
       rw [abs_le]
       exact ⟨by linarith [h.1], by linarith [h.2]⟩
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LyapunovPositivity.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LyapunovPositivity.lean
index e9b37806b7..297ad4adc9 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LyapunovPositivity.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/LyapunovPositivity.lean
@@ -307,7 +307,7 @@ theorem nonneg_of_lyapunov_nonneg {X G : H →L[ℂ] H}
         have h2 : RCLike.re ⟪P v, v⟫_ℂ ≤ ‖P v‖ * ‖v‖ := by
           calc RCLike.re ⟪P v, v⟫_ℂ ≤ ‖⟪P v, v⟫_ℂ‖ := RCLike.re_le_norm _
             _ ≤ ‖P v‖ * ‖v‖ := norm_inner_le_norm _ _
-        nlinarith [norm_nonneg (P v), norm_nonneg v]
+        nlinarith only [h1, h2, norm_nonneg (P v), norm_nonneg v]
       have hb := hPbound v
       have hA : RCLike.re ⟪A v, v⟫_ℂ
           = ‖v‖ ^ 2 - ‖P v‖ ^ 2 - RCLike.re ⟪X (P v), P v⟫_ℂ := by
@@ -315,16 +315,16 @@ theorem nonneg_of_lyapunov_nonneg {X G : H →L[ℂ] H}
         simp only [sub_apply, inner_sub_left, map_sub]
         rw [show ((1 : H →L[ℂ] H)) v = v from rfl, hXPv, hPv, hself, hvv]
       have hnormsq : ‖P v‖ ^ 2 ≤ ‖v‖ ^ 2 := by
-        nlinarith [hnorm, norm_nonneg (P v), norm_nonneg v]
+        nlinarith only [hnorm, hnorm, norm_nonneg (P v), norm_nonneg v]
       rw [hA]
-      nlinarith [hb, hnormsq, hβ, hβ1]
+      nlinarith only [hβ1, hb, hnormsq, hb, hnormsq, hβ, hβ1]
     have hAunit : IsUnit A :=
       TauCeti.ContinuousLinearMap.isUnit_of_coercive (by positivity) hAcoer
     have hAnonneg : (0 : H →L[ℂ] H) ≤ A := by
       rw [_root_.ContinuousLinearMap.nonneg_iff_isPositive]
       refine ⟨_root_.ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mp hAsa, fun v => ?_⟩
       rw [_root_.ContinuousLinearMap.reApplyInnerSelf_apply]
-      nlinarith [hAcoer v, norm_nonneg v, hβ]
+      nlinarith only [hβ, hAcoer, hAcoer v, norm_nonneg v, hβ]
     -- the compression of `G`
     set K : H →L[ℂ] H := P * G * P with hKdef
     have hKform : ∀ v : H, ⟪K v, v⟫_ℂ = ⟪G (P v), P v⟫_ℂ := by
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/NearIsometry.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/NearIsometry.lean
index 1ab8dc4b4b..854caf76a6 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/NearIsometry.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/NearIsometry.lean
@@ -197,7 +197,7 @@ private theorem norm_diagonal_apply_le (b : OrthonormalBasis (Fin d) ℝ E) (c :
     rw [repr_diagonal, mul_pow]
     refine mul_le_mul_of_nonneg_right ?_ (sq_nonneg _)
     have := hc k
-    nlinarith [abs_nonneg (c k), abs_le.mp (hc k), sq_abs (c k)]
+    nlinarith only [hδ0, this, abs_nonneg (c k), abs_le.mp (hc k), sq_abs (c k)]
   nlinarith [hbnd, norm_nonneg (diagonal b c x), mul_nonneg hδ0 (norm_nonneg x),
     sq_nonneg (‖diagonal b c x‖ - δ * ‖x‖)]
 
@@ -460,7 +460,7 @@ theorem exists_linearIsometryEquiv_norm_sub_le (M : E →ₗ[ℝ] E) {δ : ℝ}
       exact nonneg_of_mul_nonneg_left
         (le_trans (abs_nonneg (⟪M v, M v⟫_ℝ - ⟪v, v⟫_ℝ)) (hM v)) hvpos
     have := norm_nonneg x
-    nlinarith
+    nlinarith only [hδ0, this]
 
 end LinearMap
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/OperatorRealAlgebra.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/OperatorRealAlgebra.lean
index f9aeec8553..1159481235 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/OperatorRealAlgebra.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/OperatorRealAlgebra.lean
@@ -4,11 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Crall, Claude Opus 5
 -/
 module
+public import Mathlib.Analysis.InnerProductSpace.Defs
 
-public import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
-public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
-public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
-public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
+import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
 
 /-!
 # The real algebra structure on `E →L[𝕜] E`
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/OrthogonalGluing.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/OrthogonalGluing.lean
index b69da5b0f0..aef98038a6 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/OrthogonalGluing.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/OrthogonalGluing.lean
@@ -104,9 +104,7 @@ theorem norm_orthogonalGlueMap (f : A ≃ₗᵢ[𝕜] A') (g : Aᗮ ≃ₗᵢ[
       rw [Submodule.norm_coe, g.norm_map, ← Submodule.norm_coe,
         Submodule.coe_orthogonalProjectionOnto_apply]
     rw [h1, h2]
-  have h1 : (0 : ℝ) ≤ ‖orthogonalGlueMap f g x‖ := norm_nonneg _
-  have h2 : (0 : ℝ) ≤ ‖x‖ := norm_nonneg _
-  nlinarith
+  exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp hsq
 
 /-- The glue as a linear isometry. -/
 noncomputable def orthogonalGlueIsometry (f : A ≃ₗᵢ[𝕜] A') (g : Aᗮ ≃ₗᵢ[𝕜] A'ᗮ) :
@@ -314,9 +312,7 @@ theorem norm_supGlueAmbient_of_mem_sup (hAB : A ≤ Bᗮ) (hAB' : A' ≤ B'ᗮ)
     rw [Submodule.norm_coe, g.norm_map, ← Submodule.norm_coe]
   have hsq : ‖(f ⟨a, ha⟩ : H') + (g ⟨b, hb⟩ : H')‖ ^ 2 = ‖a + b‖ ^ 2 := by
     rw [@norm_add_sq 𝕜, @norm_add_sq 𝕜, hperp', hperp, hfa, hgb]
-  have h1 : (0 : ℝ) ≤ ‖(f ⟨a, ha⟩ : H') + (g ⟨b, hb⟩ : H')‖ := norm_nonneg _
-  have h2 : (0 : ℝ) ≤ ‖a + b‖ := norm_nonneg _
-  nlinarith
+  exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp hsq
 
 omit [A'.HasOrthogonalProjection] [B'.HasOrthogonalProjection] in
 /-- The ambient map sends `A ⊔ B` into `A' ⊔ B'`. -/
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/PartialIsometry.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/PartialIsometry.lean
index 5779e67344..855e295da6 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/PartialIsometry.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/PartialIsometry.lean
@@ -17,11 +17,11 @@ Sub-dev II of the operator polar decomposition project — COMPLETE
 module
 
 public import Mathlib.Analysis.InnerProductSpace.Adjoint
-public import Mathlib.Analysis.InnerProductSpace.Projection.Basic
-public import Mathlib.Analysis.InnerProductSpace.Projection.Submodule
-public import Mathlib.Analysis.InnerProductSpace.LinearMap
-public import Mathlib.Analysis.InnerProductSpace.Subspace
-public import Mathlib.Algebra.Star.StarProjection
+import Mathlib.Analysis.InnerProductSpace.Projection.Basic
+import Mathlib.Analysis.InnerProductSpace.Projection.Submodule
+import Mathlib.Analysis.InnerProductSpace.LinearMap
+import Mathlib.Analysis.InnerProductSpace.Subspace
+import Mathlib.Algebra.Star.StarProjection
 
 
 /-! # Partial isometries (Sub-dev II)
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Polar/Decomposition.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Polar/Decomposition.lean
index 8c5c7f6e9b..a788f75952 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Polar/Decomposition.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Polar/Decomposition.lean
@@ -19,9 +19,9 @@ module
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.PositiveSqrt
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.SelfAdjointFunctionalCalculus
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.PartialIsometry
-public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
-public import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
-public import Mathlib.Analysis.InnerProductSpace.StarOrder
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
+import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
+import Mathlib.Analysis.InnerProductSpace.StarOrder
 
 
 /-! # Operator polar decomposition `A = U |A|` (Sub-dev III)
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Polar/SelfAdjointCompletion.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Polar/SelfAdjointCompletion.lean
index b56d70620e..2ee250cfee 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Polar/SelfAdjointCompletion.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Polar/SelfAdjointCompletion.lean
@@ -197,15 +197,10 @@ theorem l2Column_gram_le_id_of_norm_le_one (a : E →L[ℂ] F) (b : E →L[ℂ]
       inner_self_eq_norm_sq (𝕜 := ℂ) x, inner_self_eq_norm_sq (𝕜 := ℂ) (a x),
       inner_self_eq_norm_sq (𝕜 := ℂ) (b x)]
   have hcol : ‖a x‖ ^ 2 + ‖b x‖ ^ 2 ≤ ‖x‖ ^ 2 := by
-    rw [← norm_l2Column_apply_sq]
     have hle : ‖l2Column a b x‖ ≤ ‖x‖ := by
-      calc ‖l2Column a b x‖ ≤ ‖l2Column a b‖ * ‖x‖ :=
-          ContinuousLinearMap.le_opNorm _ _
-        _ ≤ 1 * ‖x‖ := by
-            have := norm_nonneg x
-            nlinarith
-        _ = ‖x‖ := one_mul _
-    nlinarith [norm_nonneg (l2Column a b x), norm_nonneg x]
+      simpa only [one_mul] using (l2Column a b).le_of_opNorm_le h x
+    simpa only [norm_l2Column_apply_sq] using
+      pow_le_pow_left₀ (norm_nonneg _) hle 2
   change 0 ≤ RCLike.re ⟪(ContinuousLinearMap.id ℂ E -
     (ContinuousLinearMap.adjoint a ∘L a +
       ContinuousLinearMap.adjoint b ∘L b)) x, x⟫_ℂ
@@ -304,10 +299,10 @@ theorem norm_l2Block_le_one_of_diag (a : E →L[𝕜] G) (d : F →L[𝕜] H)
     ‖l2Block a (0 : F →L[𝕜] G) (0 : E →L[𝕜] H) d‖ ≤ 1 := by
   refine ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun z => ?_
   rw [one_mul]
-  have ha' : ‖a z.fst‖ ≤ ‖z.fst‖ :=
-    (a.le_opNorm z.fst).trans (by nlinarith [norm_nonneg z.fst])
-  have hd' : ‖d z.snd‖ ≤ ‖z.snd‖ :=
-    (d.le_opNorm z.snd).trans (by nlinarith [norm_nonneg z.snd])
+  have ha' : ‖a z.fst‖ ≤ ‖z.fst‖ := by
+    simpa only [one_mul] using a.le_of_opNorm_le ha z.fst
+  have hd' : ‖d z.snd‖ ≤ ‖z.snd‖ := by
+    simpa only [one_mul] using d.le_of_opNorm_le hd z.snd
   have h₁ : ‖l2Block a (0 : F →L[𝕜] G) (0 : E →L[𝕜] H) d z‖ ^ 2
       = ‖a z.fst‖ ^ 2 + ‖d z.snd‖ ^ 2 := by
     rw [WithLp.prod_norm_sq_eq_of_L2]
@@ -317,8 +312,9 @@ theorem norm_l2Block_le_one_of_diag (a : E →L[𝕜] G) (d : F →L[𝕜] H)
     mul_self_le_mul_self (norm_nonneg _) ha'
   have k₂ : ‖d z.snd‖ * ‖d z.snd‖ ≤ ‖z.snd‖ * ‖z.snd‖ :=
     mul_self_le_mul_self (norm_nonneg _) hd'
-  refine nonneg_le_nonneg_of_sq_le_sq (norm_nonneg _) ?_
-  nlinarith [h₁, h₂, k₁, k₂]
+  apply (sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).mp
+  rw [h₁, h₂]
+  simpa only [pow_two] using add_le_add k₁ k₂
 
 end Block
 
@@ -479,7 +475,9 @@ theorem exists_selfAdjoint_contraction_extension_of_column_gram_le
     rw [hJadj, hJinvol] at h
     have hid : ‖ContinuousLinearMap.id ℂ (WithLp 2 (E × E))‖ ≤ 1 :=
       ContinuousLinearMap.norm_id_le
-    nlinarith [norm_nonneg J]
+    apply (sq_le_one_iff₀ (norm_nonneg J)).mp
+    rw [pow_two, ← h]
+    exact hid
   -- Step 9: the block-diagonal damping.
   set L : WithLp 2 (E × E) →L[ℂ] WithLp 2 (E × F) :=
     l2Block (ContinuousLinearMap.id ℂ E) (0 : E →L[ℂ] E) (0 : E →L[ℂ] F) Γ with hLdef
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/PositiveSqrt.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/PositiveSqrt.lean
index 3981395511..bbf686d340 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/PositiveSqrt.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/PositiveSqrt.lean
@@ -17,9 +17,9 @@ Sub-dev I of the operator polar decomposition project — COMPLETE
 -/
 module
 
-public import Mathlib.Analysis.InnerProductSpace.Positive
-public import Mathlib.Analysis.InnerProductSpace.Spectrum
-public import Mathlib.Analysis.InnerProductSpace.Adjoint
+import Mathlib.Analysis.InnerProductSpace.Positive
+import Mathlib.Analysis.InnerProductSpace.Spectrum
+import Mathlib.Analysis.InnerProductSpace.Adjoint
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.SelfAdjointFunctionalCalculus
 
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/PrincipalAngles.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/PrincipalAngles.lean
index d437a3b9cf..bde005adef 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/PrincipalAngles.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/PrincipalAngles.lean
@@ -393,7 +393,7 @@ theorem norm_orthogonal_starProjection_comp_starProjection
         nlinarith [h]
       have hyz2 : ‖y‖ ^ 2 ≤ ‖z‖ ^ 2 := by
         have h := mul_self_le_mul_self (norm_nonneg y) hyz
-        nlinarith [h]
+        nlinarith only [h, h]
       linarith [mul_le_mul_of_nonneg_left hyz2 h1σ, p1]
     calc ‖((Submodule.span 𝕜 (Set.range w))ᗮ.starProjection ∘L
           (Submodule.span 𝕜 (Set.range u)).starProjection) z‖
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Projection/Gap.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Projection/Gap.lean
index 717e30112c..4956e14745 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Projection/Gap.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Projection/Gap.lean
@@ -357,7 +357,7 @@ theorem directedProjectionGap_le_of_inf_orthogonal_eq_bot (U V : Submodule 𝕜
   set t := U.directedProjectionGap V with ht
   have ht0 : 0 ≤ t := norm_nonneg _
   have ht1 : t ≤ 1 := U.directedProjectionGap_le_one V
-  have hk0 : (0 : ℝ) ≤ 1 - t ^ 2 := by nlinarith
+  have hk0 : (0 : ℝ) ≤ 1 - t ^ 2 := by nlinarith only [ht0, ht1]
   set c := Real.sqrt (1 - t ^ 2) with hc
   have hc0 : 0 ≤ c := Real.sqrt_nonneg _
   have hcsq : c ^ 2 = 1 - t ^ 2 := Real.sq_sqrt hk0
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Projection/Geometry.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Projection/Geometry.lean
index b11ebcec3f..ca0910a717 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Projection/Geometry.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Projection/Geometry.lean
@@ -5,7 +5,7 @@ Authors: Jon Crall, Claude Fable 5, Claude Opus 4.8
 -/
 module
 
-public import Mathlib.Analysis.InnerProductSpace.Projection.Basic
+import Mathlib.Analysis.InnerProductSpace.Projection.Basic
 public import Mathlib.Analysis.InnerProductSpace.PiL2
 
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/QuadraticFormBounds.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/QuadraticFormBounds.lean
index 9cca9ea920..8fa254ff7a 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/QuadraticFormBounds.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/QuadraticFormBounds.lean
@@ -5,7 +5,7 @@ Authors: Jon Crall, GPT 5.6 High
 -/
 module
 
-public import Mathlib.Analysis.InnerProductSpace.Adjoint
+import Mathlib.Analysis.InnerProductSpace.Adjoint
 public import Mathlib.Analysis.InnerProductSpace.Positive
 
 /-!
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/RealContinuousFunctionalCalculus.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/RealContinuousFunctionalCalculus.lean
index 9b8dfda4b1..0279916500 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/RealContinuousFunctionalCalculus.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/RealContinuousFunctionalCalculus.lean
@@ -6,7 +6,7 @@ Authors: Jon Crall, Claude Opus 5
 module
 
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.Complexification.Spectrum
-public import Mathlib.Analysis.InnerProductSpace.StarOrder
+import Mathlib.Analysis.InnerProductSpace.StarOrder
 
 /-!
 # Continuous functional calculus over `ℝ` for a real Hilbert space
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/RectangularSingularValues.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/RectangularSingularValues.lean
index 0f2f704f4f..9a91662786 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/RectangularSingularValues.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/RectangularSingularValues.lean
@@ -6,10 +6,10 @@ Authors: Jon Crall, GPT-5.6 High, Claude Fable 5
 module
 
 public import Mathlib.Analysis.InnerProductSpace.SingularValues
-public import Mathlib.Analysis.InnerProductSpace.Positive
+import Mathlib.Analysis.InnerProductSpace.Positive
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.CourantFischer
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.Spectrum
-public import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.Analysis.InnerProductSpace.PiL2
 
 
 /-!
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/ReducingSubspace.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/ReducingSubspace.lean
index 3eeff4d535..0da727a20b 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/ReducingSubspace.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/ReducingSubspace.lean
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Crall, GPT 5.6 High
 -/
 module
+public import Mathlib.Analysis.InnerProductSpace.Projection.Basic
 
-public import Mathlib.Analysis.InnerProductSpace.Projection.Submodule
+import Mathlib.Analysis.InnerProductSpace.Projection.Submodule
 
 /-!
 # Reducing subspaces for bounded operators
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Rosenblum.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Rosenblum.lean
index 52ba2c0683..1159622855 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Rosenblum.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Rosenblum.lean
@@ -117,7 +117,7 @@ theorem tendsto_damp {w : ℂ} (hw : w ≠ 1) :
       have hNn : (N : ℝ) ≤ (n : ℝ) := Nat.cast_le.mpr hn
       have : 1 / ‖w - 1‖ < (n : ℝ) := lt_of_lt_of_le hN hNn
       calc (1 : ℝ) = (1 / ‖w - 1‖) * ‖w - 1‖ := by field_simp
-        _ ≤ (n : ℝ) * ‖w - 1‖ := by nlinarith
+        _ ≤ (n : ℝ) * ‖w - 1‖ := by nlinarith only [hpos, hN, hNn]
     exact min_eq_left hle
   exact tendsto_const_nhds.congr' (hev.mono fun n hn => hn.symm)
 
@@ -138,7 +138,7 @@ theorem norm_cayleySymbolFun_le (f : C(ℝ, ℝ)) (hf : ∀ x, f x ∈ Set.Icc (
   have h2 : |damp n w| ≤ 1 := by
     rw [abs_of_nonneg (damp_nonneg n w)]
     exact damp_le_one n w
-  nlinarith [abs_nonneg (f (cayleyCoordFun w)), abs_nonneg (damp n w)]
+  nlinarith only [h1, h2, abs_nonneg (f (cayleyCoordFun w)), abs_nonneg (damp n w)]
 
 /-- **The damped symbol is continuous everywhere, including at `w = 1`.**  This is the point of the
 construction: `cayleyCoordFun` alone is only `ContinuousOn {w ≠ 1}`, and the damping squeezes the
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SchurHorn.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SchurHorn.lean
index 90de9e563e..96cd575477 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SchurHorn.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SchurHorn.lean
@@ -25,9 +25,10 @@ declared upstream).  Independently re-derived here on this project's existing
 `LinearMap.IsSymmetric.re_inner_apply_self_eq_sum_eigenvalues_mul_sq`.
 -/
 module
+public import Mathlib.Analysis.InnerProductSpace.Spectrum
 
-public import Mathlib.Analysis.Convex.Jensen
-public import Mathlib.Analysis.Convex.Mul
+import Mathlib.Analysis.Convex.Jensen
+import Mathlib.Analysis.Convex.Mul
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.CourantFischer
 
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SelfAdjointFunctionalCalculus.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SelfAdjointFunctionalCalculus.lean
index a2f23ac4a1..1b526af309 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SelfAdjointFunctionalCalculus.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SelfAdjointFunctionalCalculus.lean
@@ -6,7 +6,7 @@ Authors: Jon Crall, GPT-5.6 Thinking
 module
 
 public import Mathlib.Analysis.InnerProductSpace.Positive
-public import Mathlib.Analysis.InnerProductSpace.Spectrum
+import Mathlib.Analysis.InnerProductSpace.Spectrum
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.CourantFischer
 
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SeparatedIntertwiner.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SeparatedIntertwiner.lean
index 43ccc20822..87edc64988 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SeparatedIntertwiner.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SeparatedIntertwiner.lean
@@ -5,6 +5,8 @@ Authors: Jon Crall
 -/
 module
 
+import Mathlib.Analysis.InnerProductSpace.StarOrder
+
 public import Mathlib.Analysis.InnerProductSpace.Adjoint
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.RCLike.ScalarTransportFunctionalCalculus
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.LinearPMap.Resolvent
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SinTheta/OperatorNorm.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SinTheta/OperatorNorm.lean
index 9c50de14f1..fb69a5e446 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SinTheta/OperatorNorm.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SinTheta/OperatorNorm.lean
@@ -27,7 +27,7 @@ public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.Sylveste
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.DoubleAngle.Vector
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.CourantFischer
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.PrincipalAngles
-public import Mathlib.Analysis.InnerProductSpace.Adjoint
+import Mathlib.Analysis.InnerProductSpace.Adjoint
 
 /-! # The operator-norm Davis–Kahan sin-Θ theorem
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Spectral/Cutoff.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Spectral/Cutoff.lean
index c137d837b8..d59b456255 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Spectral/Cutoff.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Spectral/Cutoff.lean
@@ -143,7 +143,7 @@ theorem tailCutoff_tail_bound
     have hid : 1 - (1 - u ^ 2 / x) = u ^ 2 / x := by ring
     rw [hid]
     have hmul : u ^ 4 ≤ u ^ 2 * x := by
-      nlinarith [sq_nonneg (u ^ 2)]
+      nlinarith only [hx, sq_nonneg (u ^ 2)]
     calc
       x * (u ^ 2 / x) ^ 2 = u ^ 4 / x := by
         field_simp [hxpos.ne']
@@ -267,8 +267,8 @@ theorem norm_apply_le_of_spectralCutoff_apply_eq_zero {A : E →L[ℂ] E} (hA :
     intro t ht
     have ht0 : 0 ≤ t := spectrum_nonneg_of_nonneg hA ht
     rcases le_or_gt t s with h | h
-    · rw [max_eq_right (by linarith)]; nlinarith
-    · rw [max_eq_left (by linarith)]; nlinarith
+    · rw [max_eq_right (by linarith)]; nlinarith only [hs, ht0, h]
+    · rw [max_eq_left (by linarith)]; nlinarith only []
   have hnn : (0 : E →L[ℂ] E) ≤
       (s ^ 2 : ℝ) • (1 : E →L[ℂ] E) + (A + (s : ℝ) • 1) * A.spectralCutoff s - A * A := by
     rw [cutoff_split A hA s]
@@ -280,10 +280,10 @@ theorem norm_apply_le_of_spectralCutoff_apply_eq_zero {A : E →L[ℂ] E} (hA :
   simp only [sub_apply, add_apply, happ, add_zero, smul_apply, one_apply_eq_self,
     inner_sub_left, map_sub, re_inner_mul_self hsa y,
     re_inner_real_smul_self (s ^ 2) y] at hform
-  have hsq : ‖A y‖ ^ 2 ≤ (s * ‖y‖) ^ 2 := by nlinarith
+  have hsq : ‖A y‖ ^ 2 ≤ (s * ‖y‖) ^ 2 := by nlinarith only [hform]
   have h1 : (0 : ℝ) ≤ ‖A y‖ := norm_nonneg _
   have h2 : (0 : ℝ) ≤ s * ‖y‖ := mul_nonneg hs (norm_nonneg _)
-  nlinarith
+  nlinarith only [hform, h2]
 
 /-- **`A` is bounded below by `s` on the orthogonal complement of the kernel of its
 `s`-cutoff.** -/
@@ -319,7 +319,7 @@ theorem le_norm_apply_of_mem_orthogonal_ker_spectralCutoff {A : E →L[ℂ] E} (
   · simp
   · have hpos : 0 < ‖y‖ := norm_pos_iff.mpr hy0
     have hkey : s * ‖y‖ ^ 2 ≤ ‖A y‖ * ‖y‖ := by linarith
-    nlinarith
+    nlinarith only [hform, hcs, hpos]
 
 section SmoothCutoff
 
@@ -492,7 +492,7 @@ theorem mul_norm_cfc_tailCutoff_le_norm_apply
     have hx0 := hCspec_nonneg x hx
     have hcut := TauCeti.tailCutoff_lower_bound (x := x) hu0
     change 0 ≤ (x - u ^ 2) * (TauCeti.tailCutoff u x) ^ 2
-    nlinarith
+    nlinarith only [hcut]
   have hlowerIdentity :
       cfc (fun x => (x - u ^ 2) * (p x) ^ 2) C =
         Pc * C * Pc - u ^ 2 • (Pc * Pc) :=
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Spectral/GapProjection.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Spectral/GapProjection.lean
index 9c4f07ee88..b17d4f2a56 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Spectral/GapProjection.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Spectral/GapProjection.lean
@@ -5,6 +5,8 @@ Authors: Jon Crall, Claude Opus 5
 -/
 module
 
+import Mathlib.Analysis.InnerProductSpace.StarOrder
+
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.SeparatedIntertwiner
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.SpectralOrder
 
@@ -114,7 +116,7 @@ private theorem norm_lower_of_re_inner_le (T : E →L[𝕜] E) {c : ℝ} {x : E}
     simp [hx0]
   · have hcs : RCLike.re ⟪T x, x⟫_𝕜 ≤ ‖T x‖ * ‖x‖ :=
       le_trans (RCLike.re_le_norm _) (norm_inner_le_norm _ _)
-    have hmul : c * ‖x‖ * ‖x‖ ≤ ‖T x‖ * ‖x‖ := by nlinarith
+    have hmul : c * ‖x‖ * ‖x‖ ≤ ‖T x‖ * ‖x‖ := by nlinarith only [h, hcs]
     exact le_of_mul_le_mul_right hmul hx
 
 omit [CompleteSpace E] in
@@ -193,7 +195,7 @@ theorem spectrum_subset_union_of_formGap (hA : IsSelfAdjoint A)
     rw [hTinner]
     have := hlow x hx
     have hcle : c ≤ lam - α := min_le_left _ _
-    nlinarith [sq_nonneg ‖x‖]
+    nlinarith only [this, hcle, sq_nonneg ‖x‖]
   have hboundUperp : ∀ x ∈ Uᗮ, c * ‖x‖ ≤ ‖T x‖ := by
     intro x hx
     have hneg : c * ‖x‖ ^ 2 ≤ RCLike.re ⟪(-T) x, x⟫_𝕜 := by
@@ -202,7 +204,7 @@ theorem spectrum_subset_union_of_formGap (hA : IsSelfAdjoint A)
       rw [hTx, hTinner]
       have := hhigh x hx
       have hcle : c ≤ α + δ - lam := min_le_right _ _
-      nlinarith [sq_nonneg ‖x‖]
+      nlinarith only [this, hcle, sq_nonneg ‖x‖]
     simpa using norm_lower_of_re_inner_le (-T) hneg
   -- add the two estimates in quadrature
   have hbound : ∀ x : E, c ^ 2 * ‖x‖ ^ 2 ≤ ‖T x‖ ^ 2 := by
@@ -226,11 +228,11 @@ theorem spectrum_subset_union_of_formGap (hA : IsSelfAdjoint A)
     rw [hnormT, hnormx]
     have h1' : c ^ 2 * ‖u‖ ^ 2 ≤ ‖T u‖ ^ 2 := by
       have := mul_self_le_mul_self (by positivity : (0 : ℝ) ≤ c * ‖u‖) h1
-      nlinarith
+      nlinarith only [this]
     have h2' : c ^ 2 * ‖w‖ ^ 2 ≤ ‖T w‖ ^ 2 := by
       have := mul_self_le_mul_self (by positivity : (0 : ℝ) ≤ c * ‖w‖) h2
-      nlinarith
-    nlinarith
+      nlinarith only [this]
+    nlinarith only [h1', h2']
   -- `T * T` is invertible, hence so is `T`
   have hTsym := ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mp hTsa
   have hTTunit : IsUnit (T * T) := by
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Spectral/Subspace.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Spectral/Subspace.lean
index 0f52f7cdf9..fa553710d7 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Spectral/Subspace.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Spectral/Subspace.lean
@@ -4,11 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Crall, GPT 5.6 High
 -/
 module
+public import Mathlib.Analysis.InnerProductSpace.Adjoint
+public import Mathlib.LinearAlgebra.Eigenspace.Basic
 
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.CourantFischer
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.Projection.Gap
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.SpectralOrder
-public import Mathlib.Analysis.Normed.Operator.Banach
+import Mathlib.Analysis.Normed.Operator.Banach
 
 /-!
 # Finite-dimensional spectral subspaces
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SpectralOrder.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SpectralOrder.lean
index d995ff251a..c131654596 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SpectralOrder.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SpectralOrder.lean
@@ -9,7 +9,7 @@ public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.Quadrati
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.ReducingSubspace
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.BoundedOperator.Projector
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.RCLike.ScalarTransportFunctionalCalculus
-public import Mathlib.Analysis.InnerProductSpace.StarOrder
+import Mathlib.Analysis.InnerProductSpace.StarOrder
 
 /-!
 # Spectral order and quadratic forms over `RCLike`
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SphericalPythagoras.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SphericalPythagoras.lean
index 387ce0d439..21df2e8927 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SphericalPythagoras.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/SphericalPythagoras.lean
@@ -124,7 +124,7 @@ private lemma logCosNumer_deriv_nonneg {t : ℝ} (h0 : 0 < t) (h : t < π / 2) :
     Real.sin_nonneg_of_nonneg_of_le_pi h0.le (by linarith [Real.pi_pos])
   have hsl : Real.sin t ≤ t := Real.sin_le h0.le
   have hc1 : Real.cos t ≤ 1 := Real.cos_le_one t
-  have hkey : Real.sin t * Real.cos t ≤ t := by nlinarith
+  have hkey : Real.sin t * Real.cos t ≤ t := by nlinarith only [h0, hc, hsl, hc1]
   have hsplit : t / Real.cos t ^ 2 - Real.sin t / Real.cos t =
       (t - Real.sin t * Real.cos t) / Real.cos t ^ 2 := by
     field_simp
@@ -199,8 +199,8 @@ theorem cos_sqrt_sq_add_sq_le_cos_mul_cos {a b : ℝ} (ha0 : 0 ≤ a)
   set r := Real.sqrt (a ^ 2 + b ^ 2) with hr
   have hrnn : 0 ≤ r := Real.sqrt_nonneg _
   have hrsq : r ^ 2 = a ^ 2 + b ^ 2 := Real.sq_sqrt (by positivity)
-  have har : a ≤ r := by nlinarith
-  have hbr : b ≤ r := by nlinarith
+  have har : a ≤ r := by nlinarith only [hrnn, hrsq]
+  have hbr : b ≤ r := by nlinarith only [hrnn, hrsq]
   have hcosa : 0 ≤ Real.cos a :=
     Real.cos_nonneg_of_mem_Icc ⟨by linarith [Real.pi_pos], ha⟩
   have hcosb : 0 ≤ Real.cos b :=
@@ -279,7 +279,7 @@ theorem sq_le_sq_add_sq_of_cos_eq_cos_mul_cos {ω a b : ℝ} (hω0 : 0 ≤ ω)
     exact arccos_cos_mul_cos_le_sqrt ha0 ha hb0 hb
   have hsq : Real.sqrt (a ^ 2 + b ^ 2) ^ 2 = a ^ 2 + b ^ 2 :=
     Real.sq_sqrt (by positivity)
-  nlinarith [Real.sqrt_nonneg (a ^ 2 + b ^ 2)]
+  nlinarith only [hω0, hle, hsq, Real.sqrt_nonneg (a ^ 2 + b ^ 2)]
 
 /-! ### The exact identity in an inner product space -/
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Bound.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Bound.lean
index db6465d97c..4ae3187772 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Bound.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Bound.lean
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Crall, Claude Fable 5
 -/
 module
+public import Mathlib.Analysis.InnerProductSpace.Symmetric
 
-public import Mathlib.Analysis.InnerProductSpace.Rayleigh
+import Mathlib.Analysis.InnerProductSpace.Rayleigh
 
 /-! # An operator-norm bound for the Sylvester equation
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Internal/ReciprocalMultiplier.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Internal/ReciprocalMultiplier.lean
index cb7e913e34..b4ca8ac84b 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Internal/ReciprocalMultiplier.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Internal/ReciprocalMultiplier.lean
@@ -5,6 +5,8 @@ Authors: Jon Crall, GPT 5.6 High
 -/
 module
 
+import Mathlib.Analysis.Real.Pi.Bounds
+
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.Sylvester.Internal.ReciprocalMultiplier.DoubledPhase
 
 /-!
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Internal/ReciprocalMultiplier/Fourier.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Internal/ReciprocalMultiplier/Fourier.lean
index 41e45dc0af..57024071c0 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Internal/ReciprocalMultiplier/Fourier.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Internal/ReciprocalMultiplier/Fourier.lean
@@ -4,13 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Crall, GPT 5.6 High
 -/
 module
+public import Mathlib.Analysis.CStarAlgebra.Classes
+public import Mathlib.MeasureTheory.Measure.Haar.OfBasis
+public import Mathlib.MeasureTheory.Integral.Average
 
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.Sylvester.Internal.ReciprocalMultiplier.OrbitAction
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.Fourier.HaagerupZsido.Kernel
-public import Mathlib.Analysis.Convex.Integral
-public import Mathlib.Analysis.Real.Pi.Bounds
-public import Mathlib.MeasureTheory.SpecificCodomains.Pi
-public import Mathlib.LinearAlgebra.Lagrange
+import Mathlib.Analysis.SpecialFunctions.Complex.Circle
+import Mathlib.Analysis.Convex.Integral
+import Mathlib.Analysis.Real.Pi.Bounds
+import Mathlib.MeasureTheory.SpecificCodomains.Pi
+import Mathlib.LinearAlgebra.Lagrange
 
 /-!
 # Finite Fourier interpolation of the reciprocal
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Internal/ReciprocalMultiplier/OrbitAction.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Internal/ReciprocalMultiplier/OrbitAction.lean
index 801684d8e9..4ab22c4910 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Internal/ReciprocalMultiplier/OrbitAction.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/Sylvester/Internal/ReciprocalMultiplier/OrbitAction.lean
@@ -6,7 +6,7 @@ Authors: Jon Crall, GPT 5.6 High
 module
 
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.UnitarilyInvariantSeminorm
-public import Mathlib.Analysis.SpecialFunctions.Complex.Arg
+import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 public import Mathlib.Analysis.Complex.Circle
 
 /-!
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/TwoDimensionalSingularValues.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/TwoDimensionalSingularValues.lean
index e3bbde7631..2291630bd6 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/TwoDimensionalSingularValues.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/TwoDimensionalSingularValues.lean
@@ -7,7 +7,7 @@ module
 
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.KyFan
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.UnitarilyInvariantSeminorm
-public import Mathlib.Analysis.Matrix.Hermitian
+import Mathlib.Analysis.Matrix.Hermitian
 
 
 /-!
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Basic.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Basic.lean
index 98e7ac65f8..de169a1efa 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Basic.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Basic.lean
@@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Crall, Claude Fable 5
 -/
 module
+public import Mathlib.Analysis.InnerProductSpace.SingularValues
 
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.KyFan
-public import Mathlib.Algebra.Order.Algebra
-public import Mathlib.Analysis.Normed.Group.Basic
-public import Mathlib.Data.EReal.Operations
-public import Mathlib.Analysis.Convex.Caratheodory
+import Mathlib.Algebra.Order.Algebra
+import Mathlib.Analysis.Normed.Group.Basic
+import Mathlib.Data.EReal.Operations
+import Mathlib.Analysis.Convex.Caratheodory
 
 /-!
 # Unitarily invariant seminorms on rectangular linear maps
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Gauge.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Gauge.lean
index c3a8e35e6d..26f0c5f296 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Gauge.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Gauge.lean
@@ -8,7 +8,7 @@ module
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.DiagonalOperator
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.UnitarilyInvariantSeminorm.Basic
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.Convex.Majorization
-public import Mathlib.Analysis.InnerProductSpace.Projection.Reflection
+import Mathlib.Analysis.InnerProductSpace.Projection.Reflection
 
 /-!
 # Symmetric gauges of square specializations
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Majorization.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Majorization.lean
index 3c74df4fd7..d2d4a777f0 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Majorization.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Majorization.lean
@@ -7,7 +7,7 @@ module
 
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.Gram.Matrix
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.Convex.Majorization
-public import Mathlib.Analysis.InnerProductSpace.Projection.Reflection
+import Mathlib.Analysis.InnerProductSpace.Projection.Reflection
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.DiagonalOperator
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.UnitarilyInvariantSeminorm.Basic
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/Normed/Operator/SylvesterBoundedInverse.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/Normed/Operator/SylvesterBoundedInverse.lean
index 3bc3812438..a6990d3d6d 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/Normed/Operator/SylvesterBoundedInverse.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/Normed/Operator/SylvesterBoundedInverse.lean
@@ -128,7 +128,7 @@ theorem opNorm_le_of_leftInverse_fixedPoint
   have hmul : (ρ + δ) * N X ≤ N C + N X * ρ := by
     have h := mul_le_mul_of_nonneg_left hbound hρδ.le
     rwa [mul_add, ← mul_assoc, ← mul_assoc, mul_inv_cancel₀ hρδ.ne', one_mul, one_mul] at h
-  nlinarith [hmul]
+  nlinarith only [hmul, hmul]
 
 /-- **Davis--Kahan 1970 Theorem 5.1, for any compatible operator norm.**
 
@@ -174,7 +174,7 @@ theorem opNorm_le_of_sylvester_of_leftInverse
   have hmul : (ρ + δ) * N X ≤ N C + N X * ρ := by
     have h := mul_le_mul_of_nonneg_left hbound hρδ.le
     rwa [mul_add, ← mul_assoc, ← mul_assoc, mul_inv_cancel₀ hρδ.ne', one_mul, one_mul] at h
-  nlinarith [hmul]
+  nlinarith only [hmul, hmul]
 
 /-- **Davis--Kahan 1970 Theorem 5.1** at the operator norm: with a bounded left
 inverse satisfying `‖A⁻¹‖ ≤ (ρ + δ)⁻¹` and `‖B‖ ≤ ρ`, any solution of
@@ -271,7 +271,7 @@ theorem opNorm_le_of_sylvester_of_rightInverse
             ((ρ + δ) * (ρ + δ)⁻¹) * N C := by ring
       _ = ρ * N X + N C := by rw [mul_inv_cancel₀ hρδ.ne']; ring
   rw [hnormalize] at hmul
-  nlinarith [hmul]
+  nlinarith only [hmul, hmul]
 
 /-- The right-inverse form of Theorem 5.1 at the ordinary operator norm. -/
 theorem norm_le_of_sylvester_of_rightInverse
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/FiniteValueSeparation.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/FiniteValueSeparation.lean
index b6c3db53df..2e96621862 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/FiniteValueSeparation.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/FiniteValueSeparation.lean
@@ -101,13 +101,13 @@ theorem exists_uniform_positive_separation
   refine ⟨η, hη0, ?_, ?_, ?_⟩
   · have hmin : min (ε / 16) (min δv δp) ≤ ε / 16 := min_le_left _ _
     dsimp only [η]
-    nlinarith
+    nlinarith only [hε, hmin]
   · intro i
     have hmin1 : min (ε / 16) (min δv δp) ≤ min δv δp := min_le_right _ _
     have hmin2 : min δv δp ≤ δv := min_le_left _ _
     have hlt : δv < a i := hδv i (Finset.mem_univ i)
     dsimp only [η]
-    nlinarith
+    nlinarith only [hδv0, hmin1, hmin2, hlt]
   · intro i j hij
     have hp : (i, j) ∈ pairs := by
       apply Finset.mem_filter.mpr
@@ -117,7 +117,7 @@ theorem exists_uniform_positive_separation
     have hmin1 : min (ε / 16) (min δv δp) ≤ min δv δp := min_le_right _ _
     have hmin2 : min δv δp ≤ δp := min_le_right _ _
     dsimp only [η]
-    nlinarith
+    nlinarith only [hδp0, hgap, hmin1, hmin2]
 
 end
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/RCLike/ScalarTransport.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/RCLike/ScalarTransport.lean
index 2d06008fbb..024ad10a92 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/RCLike/ScalarTransport.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/RCLike/ScalarTransport.lean
@@ -15,12 +15,12 @@ Transport of Hilbert-space structure along an isomorphism of `RCLike` fields.
 -/
 module
 
-public import Mathlib.Analysis.Complex.Basic
-public import Mathlib.Analysis.InnerProductSpace.Adjoint
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Analysis.InnerProductSpace.Adjoint
 public import Mathlib.Analysis.InnerProductSpace.LinearPMap
-public import Mathlib.Analysis.InnerProductSpace.Projection.Basic
-public import Mathlib.Analysis.RCLike.Basic
-public import Mathlib.LinearAlgebra.Dimension.Basic
+import Mathlib.Analysis.InnerProductSpace.Projection.Basic
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.LinearAlgebra.Dimension.Basic
 
 /-! # Transport of a Hilbert space along an isomorphism of `RCLike` fields
 
@@ -154,7 +154,7 @@ theorem im_I_map (e : RCLikeIso 𝕜 𝕂) :
 @[simp] theorem norm_map (e : RCLikeIso 𝕜 𝕂) (x : 𝕜) : ‖e x‖ = ‖x‖ := by
   have h1 : ‖e x‖ ^ 2 = ‖x‖ ^ 2 := by
     rw [RCLike.norm_sq_eq_def, RCLike.norm_sq_eq_def, e.re_map, e.im_map]
-  nlinarith [norm_nonneg (e x), norm_nonneg x, h1]
+  exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp h1
 
 /-- The isomorphism commutes with conjugation. -/
 @[simp] theorem map_conj (e : RCLikeIso 𝕜 𝕂) (x : 𝕜) :
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/RCLike/ScalarTransportFunctionalCalculus.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/RCLike/ScalarTransportFunctionalCalculus.lean
index 8d7b44e926..00a507f527 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/RCLike/ScalarTransportFunctionalCalculus.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/RCLike/ScalarTransportFunctionalCalculus.lean
@@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Crall, Claude Opus 5
 -/
 module
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
+import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
+import Mathlib.Analysis.InnerProductSpace.StarOrder
 
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.CStarAlgebra.ContinuousFunctionalCalculusTransport
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.InnerProductSpace.OperatorRealAlgebra
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/Integral/RationalQuadratic.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/Integral/RationalQuadratic.lean
index 3c2b396032..751c88c50d 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/Integral/RationalQuadratic.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/Integral/RationalQuadratic.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Crall, GPT 5.6 High
 -/
 module
+import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
+import Mathlib.MeasureTheory.Integral.DominatedConvergence
 
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.Fourier.HaagerupZsido.Defs
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.Fourier.Poisson.CauchyLattice
@@ -50,7 +52,7 @@ private theorem integrable_inv_sq_add_sq {c : ℝ} (hc : c ≠ 0) :
   apply hscaled.congr
   filter_upwards [] with x
   have hden : c ^ 2 + x ^ 2 ≠ 0 := by
-    nlinarith [sq_pos_of_ne_zero hc, sq_nonneg x]
+    nlinarith only [hc, sq_pos_of_ne_zero hc, sq_nonneg x]
   have hbase : 1 + (c⁻¹ * x) ^ 2 ≠ 0 := by positivity
   field_simp [hc, hden, hbase]
 
@@ -67,14 +69,14 @@ private theorem integral_Ioi_inv_sq_add_sq {c : ℝ} (hc : 0 < c) :
     apply setIntegral_congr_fun measurableSet_Ioi
     intro x _
     have hden : c ^ 2 + x ^ 2 ≠ 0 := by
-      nlinarith [sq_pos_of_pos hc, sq_nonneg x]
+      nlinarith only [hc, sq_pos_of_pos hc, sq_nonneg x]
     have hbase : 1 + (c⁻¹ * x) ^ 2 ≠ 0 := by positivity
     field_simp [hc.ne', hden, hbase]
   rw [hleft] at hchange
   simp only [mul_zero, integral_Ioi_inv_one_add_sq, Real.arctan_zero,
     sub_zero, inv_inv, smul_eq_mul] at hchange
   field_simp [hc.ne'] at hchange ⊢
-  nlinarith
+  nlinarith only [hchange]
 
 /-- The repeated-pole Cauchy integral needed when the two positive parameters
 coincide. -/
@@ -87,7 +89,7 @@ private theorem integral_Ioi_sq_div_sq_add_sq_sq {c : ℝ} (hc : 0 < c) :
       (c ^ 2 + x ^ 2) ^ 2
   have hderiv (x : ℝ) := by
     have hden : c ^ 2 + x ^ 2 ≠ 0 := by
-      nlinarith [sq_pos_of_pos hc, sq_nonneg x]
+      nlinarith only [hc, sq_pos_of_pos hc, sq_nonneg x]
     exact (hasDerivAt_id x).div ((hasDerivAt_pow 2 x).const_add (c ^ 2)) hden
   have hCauchy : Integrable (fun x : ℝ => (c ^ 2 + x ^ 2)⁻¹) :=
     integrable_inv_sq_add_sq hc.ne'
@@ -100,13 +102,13 @@ private theorem integral_Ioi_sq_div_sq_add_sq_sq {c : ℝ} (hc : 0 < c) :
       have hden : Continuous (fun x : ℝ => (c ^ 2 + x ^ 2) ^ 2) := by
         fun_prop
       exact (hnum.div hden fun x => pow_ne_zero _ (by
-        nlinarith [sq_pos_of_pos hc, sq_nonneg x])).aestronglyMeasurable
+        nlinarith only [hc, sq_pos_of_pos hc, sq_nonneg x])).aestronglyMeasurable
     · filter_upwards [] with x
       have hden : 0 < c ^ 2 + x ^ 2 := by
-        nlinarith [sq_pos_of_pos hc, sq_nonneg x]
+        nlinarith only [hc, sq_pos_of_pos hc, sq_nonneg x]
       have habs : |c ^ 2 - x ^ 2| ≤ c ^ 2 + x ^ 2 := by
         rw [abs_sub_le_iff]
-        constructor <;> nlinarith [sq_nonneg c, sq_nonneg x]
+        constructor <;> nlinarith only [sq_nonneg c, sq_nonneg x]
       dsimp only [g']
       have hnum : 1 * (c ^ 2 + x ^ 2) - x * ((2 : ℝ) * x ^ (2 - 1)) =
           c ^ 2 - x ^ 2 := by norm_num; ring
@@ -147,7 +149,7 @@ private theorem integral_Ioi_sq_div_sq_add_sq_sq {c : ℝ} (hc : 0 < c) :
           c ^ 2 - x ^ 2 := by norm_num; ring
       rw [hnum]
       have hden : c ^ 2 + x ^ 2 ≠ 0 := by
-        nlinarith [sq_pos_of_pos hc, sq_nonneg x]
+        nlinarith only [hc, sq_pos_of_pos hc, sq_nonneg x]
       field_simp [hden]
       ring
     _ = (1 / 2 : ℝ) * (∫ x : ℝ in Set.Ioi 0, (c ^ 2 + x ^ 2)⁻¹) -
@@ -174,7 +176,7 @@ private theorem integral_Ioi_sq_div_two_quadratics
         intro y hy
         have hy0 : y ≠ 0 := hy.ne'
         have hcden : c ^ 2 + y ^ 2 ≠ 0 := by
-          nlinarith [sq_pos_of_pos hc, sq_nonneg y]
+          nlinarith only [hc, sq_pos_of_pos hc, sq_nonneg y]
         field_simp [hy0, hcden]
         ring
       _ = Real.pi / (2 * c) := integral_Ioi_inv_sq_add_sq hc
@@ -195,7 +197,7 @@ private theorem integral_Ioi_sq_div_two_quadratics
         intro hsq
         rcases (sq_eq_sq_iff_eq_or_eq_neg.mp hsq) with h | h
         · exact hac h.symm
-        · nlinarith
+        · nlinarith only [hc, haPos, h]
       have hCInt : Integrable (fun y : ℝ => (c ^ 2 + y ^ 2)⁻¹) :=
         integrable_inv_sq_add_sq hc.ne'
       have hAInt : Integrable (fun y : ℝ => (a ^ 2 + y ^ 2)⁻¹) :=
@@ -209,9 +211,9 @@ private theorem integral_Ioi_sq_div_two_quadratics
           apply setIntegral_congr_fun measurableSet_Ioi
           intro y _
           have hcden : c ^ 2 + y ^ 2 ≠ 0 := by
-            nlinarith [sq_pos_of_pos hc, sq_nonneg y]
+            nlinarith only [hc, sq_pos_of_pos hc, sq_nonneg y]
           have haden : a ^ 2 + y ^ 2 ≠ 0 := by
-            nlinarith [sq_pos_of_pos haPos, sq_nonneg y]
+            nlinarith only [haPos, sq_pos_of_pos haPos, sq_nonneg y]
           field_simp [hdiff, hcden, haden]
           ring
         _ = (c ^ 2 / (c ^ 2 - a ^ 2)) *
@@ -253,7 +255,7 @@ private theorem integrable_sq_div_two_quadratics
       calc
         y ^ 2 / ((y ^ 2 + c ^ 2) * (y ^ 2 + a ^ 2)) ≤
             (y ^ 2 + a ^ 2) / ((y ^ 2 + c ^ 2) * (y ^ 2 + a ^ 2)) :=
-          div_le_div_of_nonneg_right (by nlinarith [sq_nonneg a]) (by positivity)
+          div_le_div_of_nonneg_right (by nlinarith only [sq_nonneg a]) (by positivity)
         _ = (c ^ 2 + y ^ 2)⁻¹ := by
           field_simp [hC.ne', hA.ne']
           ring
@@ -343,7 +345,7 @@ theorem integral_weight_mul_reciprocal_difference
     have hcommon : 0 < y ^ 2 + (c n) ^ 2 := by positivity
     have hA : 0 < y ^ 2 + a ^ 2 := by positivity
     have hAB : y ^ 2 + a ^ 2 ≤ y ^ 2 + (a + 2) ^ 2 := by
-      nlinarith
+      nlinarith only [ha]
     have hden :
         (y ^ 2 + (c n) ^ 2) * (y ^ 2 + a ^ 2) ≤
           (y ^ 2 + (c n) ^ 2) * (y ^ 2 + (a + 2) ^ 2) :=
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/Integral/SineLaplace.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/Integral/SineLaplace.lean
index cbb6ff985f..fb5eeb28a0 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/Integral/SineLaplace.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/Integral/SineLaplace.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Crall, GPT 5.6 High
 -/
 module
+import Mathlib.MeasureTheory.Integral.ExpDecay
+import Mathlib.MeasureTheory.Measure.Lebesgue.Integral
 
 public import LeanPool.DavisKahan.ForTauCeti.Analysis.Fourier.ExponentialAbs
 
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/Sqrt.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/Sqrt.lean
index 4a9a498b1a..22a91dbe0d 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/Sqrt.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/Sqrt.lean
@@ -64,8 +64,8 @@ theorem abs_sqrt_sub_one_le_abs_sub_one {μ : ℝ} (hμ : 0 ≤ μ) :
   have key : |Real.sqrt μ - 1| * (Real.sqrt μ + 1) = |μ - 1| := by
     rw [← abs_of_nonneg (by linarith : (0 : ℝ) ≤ Real.sqrt μ + 1), ← abs_mul]
     congr 1
-    nlinarith [hsq]
-  nlinarith [key, mul_nonneg (abs_nonneg (Real.sqrt μ - 1)) hs]
+    nlinarith only [hsq, hsq]
+  nlinarith only [hs, key, key, mul_nonneg (abs_nonneg (Real.sqrt μ - 1)) hs]
 
 /-- If `|μ - 1| ≤ δ ≤ 1 / 2`, then `|1 - (√μ)⁻¹| ≤ δ`.
 
@@ -84,11 +84,11 @@ theorem abs_one_sub_inv_sqrt_le {μ δ : ℝ} (hδ : δ ≤ 1 / 2) (hμ : |μ -
   have hssq : s ^ 2 = μ := Real.sq_sqrt (le_of_lt hμpos)
   -- `s ≥ 1/2` (since `s² = μ ≥ 1/2`)
   have hssqlb : (1 : ℝ) / 2 ≤ s ^ 2 := by rw [hssq]; linarith
-  have hsge : (1 : ℝ) / 2 ≤ s := by nlinarith [hs0, hssqlb]
+  have hsge : (1 : ℝ) / 2 ≤ s := by nlinarith only [hδ, hμlb, hμpos, hs0, hssq, hs0, hssqlb]
   have hδ0 : 0 ≤ δ := le_trans (abs_nonneg _) hμ
   rw [abs_le] at hμ ⊢
   obtain ⟨hμ1, hμ2⟩ := hμ
-  have hssq' : s * s = μ := by nlinarith [hssq]
+  have hssq' : s * s = μ := by nlinarith only [hssq, hssq]
   -- Lower bound `1 ≤ (1 + δ) * s`: its square is `(1 + δ)² μ ≥ (1 + δ)² (1 - δ) ≥ 1`.
   have hlow : 1 ≤ (1 + δ) * s := by
     have hpos : 0 < (1 + δ) * s := by positivity
@@ -97,8 +97,8 @@ theorem abs_one_sub_inv_sqrt_le {μ δ : ℝ} (hδ : δ ≤ 1 / 2) (hμ : |μ -
   -- Upper bound `(1 - δ) * s ≤ 1`: equivalently `(1 - δ)² μ ≤ 1` when `1 - δ ≥ 0`.
   have hhigh : (1 - δ) * s ≤ 1 := by
     rcases le_or_gt (1 - δ) 0 with h | h
-    · nlinarith [hs0, h]
-    · nlinarith [hssq', hμ1, hμ2, hδ0, hsge, h, mul_nonneg hδ0 hδ0]
+    · nlinarith only [hδ, h, hs0, h]
+    · nlinarith only [hμlb, hs0, hssq, hμ2, hlow, hssq', hμ1, hμ2, hδ0, hsge, h, mul_nonneg hδ0 hδ0]
   -- Translate the two multiplicative bounds into bounds on `s⁻¹`.
   have hinv_le : s⁻¹ ≤ 1 + δ := by
     rw [inv_eq_one_div, div_le_iff₀ hs0]; linarith [hlow]
diff --git a/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/TanArcsin.lean b/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/TanArcsin.lean
index 293dc1a37c..5fd8a3a01e 100644
--- a/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/TanArcsin.lean
+++ b/LeanPool/DavisKahan/ForTauCeti/Analysis/SpecialFunctions/TanArcsin.lean
@@ -40,8 +40,8 @@ theorem tanArcsin_le_tanArcsin {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hb :
     Real.tan (Real.arcsin a) ≤ Real.tan (Real.arcsin b) := by
   rw [Real.tan_arcsin, Real.tan_arcsin]
   have hb0 : 0 ≤ b := ha.trans hab
-  have hbsq : b ^ 2 < 1 := by nlinarith
-  have hasq : a ^ 2 ≤ b ^ 2 := by nlinarith
+  have hbsq : b ^ 2 < 1 := by nlinarith only [ha, hab, hb]
+  have hasq : a ^ 2 ≤ b ^ 2 := by nlinarith only [ha, hab]
   have hbpos : 0 < Real.sqrt (1 - b ^ 2) := Real.sqrt_pos.mpr (by linarith)
   have hapos : 0 < Real.sqrt (1 - a ^ 2) := by
     have : a ^ 2 < 1 := lt_of_le_of_lt hasq hbsq
@@ -67,14 +67,14 @@ theorem sin_arctan_lt_one (C : ℝ) : Real.sin (Real.arctan C) < 1 := by
   rw [div_lt_one hpos]
   rcases le_or_gt C 0 with hC | hC
   · exact lt_of_le_of_lt hC hpos
-  · exact (Real.lt_sqrt hC.le).mpr (by nlinarith)
+  · exact (Real.lt_sqrt hC.le).mpr (by nlinarith only [])
 
 /-- The sine-to-tangent transfer is continuous at every point of `[0, 1)`. -/
 theorem continuousAt_tanArcsin {t : ℝ} (h0 : 0 ≤ t) (h1 : t < 1) :
     ContinuousAt (fun s => Real.tan (Real.arcsin s)) t := by
   have hcos : Real.cos (Real.arcsin t) ≠ 0 := by
     rw [Real.cos_arcsin]
-    have : (0 : ℝ) < 1 - t ^ 2 := by nlinarith
+    have : (0 : ℝ) < 1 - t ^ 2 := by nlinarith only [h0, h1]
     exact (Real.sqrt_pos.mpr this).ne'
   exact (Real.continuousAt_tan.mpr hcos).comp Real.continuous_arcsin.continuousAt
 
diff --git a/LeanPool/DavisKahan/Palomar/DKSectionTwo/SolutionPrelude.lean b/LeanPool/DavisKahan/Palomar/DKSectionTwo/SolutionPrelude.lean
index 70c8c12bc2..e119c5d368 100644
--- a/LeanPool/DavisKahan/Palomar/DKSectionTwo/SolutionPrelude.lean
+++ b/LeanPool/DavisKahan/Palomar/DKSectionTwo/SolutionPrelude.lean
@@ -6,9 +6,9 @@ Authors: Jon Crall
 module
 
 public import Mathlib.Analysis.InnerProductSpace.LinearPMap
-public import Mathlib.Order.CompletePartialOrder
-public import Mathlib.RingTheory.PicardGroup
-public import Mathlib.Tactic
+-- Preserve the instance dictionaries in the elaborated comparator vocabulary.
+public import Mathlib.Order.CompletePartialOrder -- shake: keep
+public import Mathlib.RingTheory.PicardGroup -- shake: keep
 
 /-!
 # Davis--Kahan 1970: the four Section 2 theorems