refactor: Lint

HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean

@@ -95,7 +95,7 @@ lemma isBounded_right_zero {m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ :
   obtain ⟨c, hc⟩ := h
   use c
   intro Φ x
-  have hc1 :=  hc Φ 0 x
+  have hc1 := hc Φ 0 x
   rw [right_zero] at hc1
   exact hc1
 

HepLean/StandardModel/HiggsBoson/Basic.lean

@@ -59,6 +59,8 @@ lemma smooth_toFin2ℂ : Smooth 𝓘(ℝ, HiggsVec) 𝓘(ℝ, Fin 2 → ℂ) toF
 def orthonormBasis : OrthonormalBasis (Fin 2) ℂ HiggsVec :=
   EuclideanSpace.basisFun (Fin 2) ℂ
 
+/-- Generating a Higgs vector from a real number, such that the norm-squared of that Higgs vector
+  is the given real number. -/
 def ofReal (a : ℝ) : HiggsVec :=
   ![Real.sqrt a, 0]
 
@@ -164,6 +166,8 @@ lemma isConst_of_higgsVec (φ : HiggsVec) : φ.toField.IsConst := fun _ => congr
 lemma isConst_iff_of_higgsVec (Φ : HiggsField) : Φ.IsConst ↔ ∃ (φ : HiggsVec), Φ = φ.toField :=
   Iff.intro (fun h ↦ ⟨Φ 0, by ext x y; rw [← h x 0]; rfl⟩) (fun ⟨φ, hφ⟩ x y ↦ by subst hφ; rfl)
 
+/-- Generating a constant Higgs field from a real number, such that the norm-squared of that Higgs
+  vector is the given real number. -/
 def ofReal (a : ℝ) : HiggsField := (HiggsVec.ofReal a).toField
 
 end HiggsField

HepLean/StandardModel/HiggsBoson/GaugeAction.lean

@@ -135,7 +135,7 @@ def rotateGuageGroup {φ : HiggsVec} (hφ : φ ≠ 0) : GaugeGroup :=
     ⟨1, ⟨(rotateMatrix φ), rotateMatrix_specialUnitary hφ⟩, 1⟩
 
 lemma rotateGuageGroup_apply {φ : HiggsVec} (hφ : φ ≠ 0) :
-    rep (rotateGuageGroup hφ) φ = ![0, ofReal ‖φ‖] := by
+    rep (rotateGuageGroup hφ) φ = ![0, Complex.ofReal ‖φ‖] := by
   rw [rep_apply]
   simp only [rotateGuageGroup, rotateMatrix, one_pow, one_smul,
     Nat.succ_eq_add_one, Nat.reduceAdd, ofReal_eq_coe]
@@ -155,7 +155,7 @@ lemma rotateGuageGroup_apply {φ : HiggsVec} (hφ : φ ≠ 0) :
       Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm]
 
 theorem rotate_fst_zero_snd_real (φ : HiggsVec) :
-    ∃ (g : GaugeGroup), rep g φ = ![0, ofReal ‖φ‖] := by
+    ∃ (g : GaugeGroup), rep g φ = ![0, Complex.ofReal ‖φ‖] := by
   by_cases h : φ = 0
   · use ⟨1, 1, 1⟩
     simp [h]

HepLean/StandardModel/HiggsBoson/Potential.lean

@@ -76,7 +76,8 @@ lemma discrim_nonneg (μ2 : ℝ) {𝓵 : ℝ} (h : 𝓵 ≠ 0) (φ : HiggsField)
     exact sq_nonneg (2 * 𝓵 * ‖φ‖_H ^ 2 x + - μ2)
   · exact h
 
-lemma discrim_eq_sqrt_discrim_mul_self (μ2 : ℝ) {𝓵 : ℝ} (h : 𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) :
+lemma discrim_eq_sqrt_discrim_mul_self (μ2 : ℝ) {𝓵 : ℝ} (h : 𝓵 ≠ 0) (φ : HiggsField)
+    (x : SpaceTime) :
     discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x) = Real.sqrt (discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x)) *
       Real.sqrt (discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x)) := by
   refine Eq.symm (Real.mul_self_sqrt ?h)
@@ -134,7 +135,7 @@ lemma discrim_ge_zero_of_neg_𝓵 (μ2 : ℝ) {𝓵 : ℝ} (h : 𝓵 < 0) (c :
     ← (div_le_iff₀' (by linarith : 0 < - 4 * 𝓵)), le_neg]
   ring_nf
 
-example (a b c : ℝ ) (hc : c < 0) :  a ≤ b / c ↔ b ≤ c * a := by
+example (a b c : ℝ) (hc : c < 0) : a ≤ b / c ↔ b ≤ c * a := by
   exact le_div_iff_of_neg' hc
 lemma pot_le_zero_of_neg_𝓵 (μ2 : ℝ) {𝓵 : ℝ} (h : 𝓵 < 0) (φ : HiggsField) (x : SpaceTime) :
     (0 < μ2 ∧ potential μ2 𝓵 φ x ≤ 0) ∨ μ2 ≤ 0 := by
@@ -142,7 +143,7 @@ lemma pot_le_zero_of_neg_𝓵 (μ2 : ℝ) {𝓵 : ℝ} (h : 𝓵 < 0) (φ : Higg
   · simp [hμ2]
   simp [potential, hμ2]
   apply And.intro (lt_of_not_ge hμ2)
-  have h1 : 0 ≤  μ2 * ‖φ x‖ ^ 2 := by
+  have h1 : 0 ≤ μ2 * ‖φ x‖ ^ 2 := by
     refine Left.mul_nonneg ?ha ?hb
     · exact le_of_not_ge hμ2
     · exact sq_nonneg ‖φ x‖
@@ -198,7 +199,8 @@ lemma exist_sol_iff_of_neg_𝓵 (μ2 : ℝ) {𝓵 : ℝ} (h𝓵 : 𝓵 < 0) (c :
         rw [← le_div_iff_of_neg']
         · exact h.2
         · linarith
-    have hdd : discrim 𝓵 (-μ2) (-c) = Real.sqrt (discrim 𝓵 (-μ2) (-c)) * Real.sqrt (discrim 𝓵 (-μ2) (-c)) := by
+    have hdd : discrim 𝓵 (-μ2) (-c) = Real.sqrt (discrim 𝓵 (-μ2) (-c))
+        * Real.sqrt (discrim 𝓵 (-μ2) (-c)) := by
       exact (Real.mul_self_sqrt hd).symm
     refine (quadratic_eq_zero_iff (ne_of_gt h𝓵).symm hdd _).mpr ?_
     simp only [neg_neg, or_true, a]
@@ -258,8 +260,6 @@ lemma isBounded_𝓵_nonneg {μ2 𝓵 : ℝ} (h : IsBounded μ2 𝓵) :
       rw [hφ] at hc2
       linarith
 
-
-
 section lowerBound
 /-!
 
@@ -310,7 +310,6 @@ variable (h𝓵 : 0 < 𝓵)
 
 -/
 
-
 include h𝓵
 lemma normSq_of_eq_bound (φ : HiggsField) (x : SpaceTime)
     (hV : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵)) :