Reduce MetricCodes spectral and harmonic proof elaboration cost

LeanPool/MetricCodes/Binary.lean

@@ -2110,7 +2110,7 @@ theorem coupledDegreeCoordinates_pairing {n w p q L : ℕ}
               n (p + q + i.val)))) _
           (e.repr A) (e.repr B)
       rw [PiLp.inner_apply]
-      simp only [RCLike.inner_apply, Real.ringHom_apply, mul_comm]
+      simp only [Real.inner_apply]
     _ = @inner ℝ
         (MetricCodes.Boolean.harmonicEuclideanLayer n
           (p + q + i.val)) _ A B :=
@@ -6357,7 +6357,7 @@ theorem clebschNormSq_succ_mul
     exact (mul_eq_zero.mp hcancel).resolve_left hpositive.ne'
   dsimp [A, B, T, M₀, Mprev] at hidentity
   push_cast at hidentity
-  nlinarith only [hidentity]
+  linear_combination hidentity
 
 theorem clebschNormSq_div_succ
     {w N p q t : ℕ}
@@ -6828,8 +6828,7 @@ theorem johnsonMiddleSignedScalar_eq_sqrt_hattedDiagonal
   have heq :
       (johnsonDiagonalChannelSign n w p q j * D) * S =
         Real.sqrt (D ^ 2 / z) := by
-    nlinarith [hsquare, hsqrt,
-      Real.sqrt_nonneg (D ^ 2 / z)]
+    exact (sq_eq_sq₀ hleft (Real.sqrt_nonneg _)).mp (hsquare.trans hsqrt.symm)
   rw [clebschClosedCenteredExpectation_eq_johnsonDiagonal
     h hstrict source]
   have hhatted :
@@ -8216,12 +8215,10 @@ theorem johnsonLowerOffDiagonalScalar_eq_sqrt_source
       johnsonLowerOffDiagonalScalar n w p q target.val ^ 2 =
         johnsonSourceChannelCoefficient
           n w p q L source target := by
-    nlinarith [sq_nonneg
-      (johnsonLowerOffDiagonalScalar n w p q target.val ^ 2 -
-        johnsonSourceChannelCoefficient n w p q L source target)]
+    exact (sq_eq_sq₀ (sq_nonneg _) hright).mp
+      ((pow_mul _ 2 2).symm.trans hfourth)
   have hroot := Real.sq_sqrt hright
-  nlinarith [Real.sqrt_nonneg
-    (johnsonSourceChannelCoefficient n w p q L source target)]
+  exact (sq_eq_sq₀ hleft.le (Real.sqrt_nonneg _)).mp (hsquare.trans hroot.symm)
 
 theorem johnsonUpperOffDiagonalScalar_eq_sqrt_source
     {n w p q L : ℕ}

LeanPool/MetricCodes/Conclusion.lean

@@ -4456,10 +4456,9 @@ theorem gtRelativeCasimir_comp_eq_smul_add_of_orthogonal_full_block_rows
   apply gtRelativeCasimir_comp_eq_smul_add_of_full_axis_transverse_rows
     lam hn hdom B A K d
   · intro mu
-    rw [haxisOrth mu, smul_zero, zero_add, haxis mu]
+    simpa only [haxisOrth mu, smul_zero, zero_add] using haxis mu
   · intro mu
-    rw [htransverseOrth mu, LinearMap.zero_comp, add_zero,
-      htransverse mu]
+    simpa only [htransverseOrth mu, LinearMap.zero_comp, add_zero] using htransverse mu
 
 end AllRankGTPhysicalRetainedAdditiveColumn
 

LeanPool/MetricCodes/HarmonicAnalysis.lean

@@ -6817,7 +6817,7 @@ theorem rawLiftChannel_inner {n k L : ℕ}
       rw [PiLp.inner_apply]
       apply Finset.sum_congr rfl
       intro a ha
-      simp only [RCLike.inner_apply, Real.ringHom_apply, mul_comm]
+      simp only [Real.inner_apply]
 
 /-- The zero coordinate index in the nonempty certificate fibre. -/
 def firstFibreIndex (n k : ℕ) (hn : 3 ≤ n) :

LeanPool/MetricCodes/Hierarchy.lean

@@ -2700,7 +2700,9 @@ theorem sliceCost_continuousOn {s : ℝ} (hs : s < 1) :
   have harg : (1 - t) / (1 - s) ≠ 0 := by
     exact (div_pos (by linarith [ht.2]) (by linarith)).ne'
   unfold MetricCodes.Spherical.SidelnikovLocalization.sliceCost Real.logb
-  fun_prop
+  exact continuousWithinAt_const.mul
+    ((((continuousWithinAt_const.sub continuousWithinAt_id).div_const (1 - s)).log harg).div_const
+      _)
 
 theorem levelRate_zero_le_squared_entropy_of_spectral {t : ℝ}
     (ht : 0 < t) (hspectral : t < 2 * spectralAtom (t ^ 2)) :

LeanPool/MetricCodes/HighestWeights.lean

@@ -571,7 +571,7 @@ theorem projectedCoordinateRaise_canonicalGelfandTsetlinFibre_eq_of_pathExchange
   simpa only [EuclideanSpace.basisFun_apply, mul_one] using
     (projectedCoordinateRaise_reverseInterlacingHarmonicBranch_eq_of_pathExchange low mu row
       hlow hhigh hdom 1
-      (by simpa using hexchange) q)
+      (by simpa only [one_smul] using hexchange) q)
 
 theorem canonicalAdjacentProjectedRaiseCoefficient_sq
     {r n : ℕ} (low : Fin (r + 2) → ℕ)
@@ -2869,12 +2869,6 @@ theorem spectralPathOperator_succ_rtt_of
     spectralPathOperator_succ lam hdom a t k v,
     spectralPathOperator_succ lam hdom a t k u,
     spectralPathOperator_succ lam hdom a s k v]
-  change
-    (u - v) •
-        ((x • C - A.comp S).comp (y • F - B.comp T) -
-          (y • F - B.comp T).comp (x • C - A.comp S)) =
-      (x • E - A.comp T).comp (y • D - B.comp S) -
-        (y • F - B.comp T).comp (x • C - A.comp S)
   exact hstep
 
 end ArbitraryRowSameAxisDiamondSpectralRTTStep

LeanPool/MetricCodes/MatrixPerron.lean

@@ -179,7 +179,8 @@ theorem exists_nonnegative_topEigenvector (A : Matrix I I ℝ)
   have hyray : rayleigh A y = topEigenvalue A :=
     le_antisymm habove hbelow
   have hself : IsSelfAdjoint (continuousOperator A) :=
-    (operator_isSymmetric A hsymm).isSelfAdjoint
+    LinearMap.IsSymmetric.isSelfAdjoint (A := continuousOperator A)
+      (operator_isSymmetric A hsymm)
   have hmax :
       IsMaxOn (continuousOperator A).reApplyInnerSelf
         (sphere (0 : Space I) ‖y‖) y := by

LeanPool/MetricCodes/Rates.lean

@@ -2923,8 +2923,8 @@ theorem edgeLimit_sq_div_zero
   have hs := (Real.sqrt_pos.mpr hu).ne'
   have hf := hfactor'.ne'
   unfold edgeLimit hattedEdgeLimit
+  rw [div_pow, hsquare]
   field_simp [hz, hm, hs, hf]
-  nlinarith [hsquare]
 
 theorem tendsto_johnsonHattedDiagonal
     {d a b g u : ℝ}

LeanPool/MetricCodes/Rigidity.lean

@@ -2063,19 +2063,11 @@ theorem rootJointHarmonicBracketActionMixed_add_lowerStructure_eq_zero
       (((rootJointHarmonicActionLowerRootStructureCross n lam (k + 1) f S).val :
         youngMultihomogeneousSubmodule n (rootWedgeWeight lam S)) :
         PolynomialSpace r n) = 0
-  change
-    rootJointHarmonicPolynomialInclusion n lam (k + 1)
-        (rootJointHarmonicBracketActionMixed n lam k f) S.val =
-      rootPolynomialBracketActionMixed r n k g S.val at hmixedS
+  simp only [LinearMap.comp_apply] at hmixedS
   rw [rootJointHarmonicPolynomialInclusion_apply_admissible] at hmixedS
   rw [hmixedS]
-  change
-    rootBracketCoboundary r n k (rootActionBoundary r n k g) S.val +
-        rootActionBoundary r n (k + 1)
-          (rootBracketCoboundary r n (k + 1) g) S.val +
-      (((rootJointHarmonicActionLowerRootStructureCross n lam (k + 1) f S).val :
-        youngMultihomogeneousSubmodule n (rootWedgeWeight lam S)) :
-        PolynomialSpace r n) = 0
+  simp only [rootPolynomialBracketActionMixed, LinearMap.add_apply,
+    LinearMap.comp_apply, Pi.add_apply]
   rw [add_comm
     (rootBracketCoboundary r n k (rootActionBoundary r n k g) S.val)
     (rootActionBoundary r n (k + 1)
@@ -2819,19 +2811,11 @@ theorem rootJointHarmonicActionBracketMixed_add_upperStructure_eq_zero
       (((rootJointHarmonicActionUpperRootStructureCross n lam (k + 1) f S).val :
         youngMultihomogeneousSubmodule n (rootWedgeWeight lam S)) :
         PolynomialSpace r n) = 0
-  change
-    rootJointHarmonicPolynomialInclusion n lam (k + 1)
-        (rootJointHarmonicActionBracketMixed n lam k f) S.val =
-      rootPolynomialActionBracketMixed r n k g S.val at hmixedS
+  simp only [LinearMap.comp_apply] at hmixedS
   rw [rootJointHarmonicPolynomialInclusion_apply_admissible] at hmixedS
   rw [hmixedS]
-  change
-    rootActionCoboundary r n k (rootBracketBoundary r n k g) S.val +
-        rootBracketBoundary r n (k + 1)
-          (rootActionCoboundary r n (k + 1) g) S.val +
-      (((rootJointHarmonicActionUpperRootStructureCross n lam (k + 1) f S).val :
-        youngMultihomogeneousSubmodule n (rootWedgeWeight lam S)) :
-        PolynomialSpace r n) = 0
+  simp only [rootPolynomialActionBracketMixed, LinearMap.add_apply,
+    LinearMap.comp_apply, Pi.add_apply]
   rw [hfull]
   rw [fullRootExteriorUpperRootStructureIncidence_zeroExtension_apply lam f S]
   exact neg_add_cancel _