perf(DavisKahan): narrow proof imports and simplify operator estimates

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

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

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

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

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

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) :

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‖]

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

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 ?_

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)

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
 

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

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