feat: Linting and small lemma

PhysLean/CondensedMatter/TightBindingChain/Basic.lean

@@ -538,7 +538,7 @@ lemma energyEigenstate_orthogonal :
     simp only [Nat.cast_one] at h2 h1
     calc _ = Complex.exp (Complex.I * k2 * 1 * T.N * T.a - Complex.I * k1 * 1 * T.N * T.a) := by
              ring_nf
-         _ = 1 := by rw [Complex.exp_sub, h2, h1, div_one]
+        _ = 1 := by rw [Complex.exp_sub, h2, h1, div_one]
   have hω_ne_one : ω ≠ 1 := by
     intro hω_eq_one
     apply hne

PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean

@@ -432,6 +432,17 @@ lemma potentialIsBounded_iff_exists_forall_reduced (P : PotentialParameters) :
         · nlinarith
         · grind
 
+lemma massTermReduced_pos_of_quarticTermReduced_zero_potentialIsBounded (P : PotentialParameters)
+    (hP : PotentialIsBounded P) (k : EuclideanSpace ℝ (Fin 3))
+    (hk : ‖k‖ ^ 2 ≤ 1) (hq : quarticTermReduced P k = 0) : 0 ≤ massTermReduced P k := by
+  rw [potentialIsBounded_iff_exists_forall_reduced] at hP
+  obtain ⟨c, hc₀, hc⟩ := hP
+  specialize hc k hk
+  rw [hq] at hc
+  simp only [le_refl, mul_zero, zero_mul, sq_nonpos_iff, true_and] at hc
+  generalize massTermReduced P k = j2 at *
+  grind
+
 @[sorryful]
 lemma potentialIsBounded_iff_forall_reduced (P : PotentialParameters) :
     PotentialIsBounded P ↔ ∀ k : EuclideanSpace ℝ (Fin 3), ‖k‖ ^ 2 ≤ 1 →

PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean

@@ -227,8 +227,7 @@ noncomputable def evalTColorToComplex {n : ℕ}
     permT (S := complexLorentzTensor) (σ := (id : Fin n → Fin n))
       (by
         -- transport ((colorToComplex ∘ c) ∘ i.succAbove) and (colorToComplex ∘ (c ∘ i.succAbove))
-        simp [Function.comp_apply]
-      )
+        simp [Function.comp_apply])
       ((TensorSpecies.Tensor.evalT (S := complexLorentzTensor) (c := (colorToComplex ∘ c))
           i (evalIdxToComplex (c := c) i b)) t)