Merge pull request #92 from HEPLean/Update-versions

refactor: Basic lint
2024-07-18 17:00:13 -04:00 · 2024-07-18 17:00:13 -04:00 · ea45922df8
commit ea45922df8
parent 1233987bd7 52e591fa7a
27 changed files with 53 additions and 57 deletions
--- a/HepLean/AnomalyCancellation/Basic.lean
+++ b/HepLean/AnomalyCancellation/Basic.lean
@ -183,12 +183,11 @@ lemma QuadSols.ext {χ : ACCSystemQuad} {S T : χ.QuadSols} (h : S.val = T.val)

 /-- An instance giving the properties and structures to define an action of `ℚ` on `QuadSols`. -/
 instance quadSolsMulAction (χ : ACCSystemQuad) : MulAction ℚ χ.QuadSols where
-  smul a S := ⟨a • S.toLinSols , by
+  smul a S := ⟨a • S.toLinSols, by
    intro i
    erw [(χ.quadraticACCs i).map_smul]
    rw [S.quadSol i]
-    simp only [mul_zero]
-    ⟩
+    simp only [mul_zero]⟩
  mul_smul a b S := by
    apply QuadSols.ext
    exact mul_smul _ _ _
--- a/HepLean/AnomalyCancellation/GroupActions.lean
+++ b/HepLean/AnomalyCancellation/GroupActions.lean
@ -44,8 +44,7 @@ def linSolMap {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) :
    χ.LinSols →ₗ[ℚ] χ.LinSols where
  toFun S := ⟨G.rep g S.val, by
   intro i
-   rw [G.linearInvariant, S.linearSol]
-   ⟩
+   rw [G.linearInvariant, S.linearSol]⟩
  map_add' S T := by
    apply ACCSystemLinear.LinSols.ext
    exact (G.rep g).map_add' _ _
@ -85,8 +84,7 @@ instance quadSolAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) :
  smul f S := ⟨G.linSolRep f S.1, by
   intro i
   simp only [linSolRep_apply_apply_val]
-   rw [G.quadInvariant, S.quadSol]
-  ⟩
+   rw [G.quadInvariant, S.quadSol]⟩
  mul_smul f1 f2 S := by
    apply ACCSystemQuad.QuadSols.ext
    change (G.rep.toFun (f1 * f2)) S.val = _
--- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
@ -42,7 +42,7 @@ def toSMPlusH : MSSMCharges.Charges ≃ (Fin 18 ⊕ Fin 2 → ℚ) :=
 /-- An equivalence between `Fin 18 ⊕ Fin 2 → ℚ` and `(Fin 18 → ℚ) × (Fin 2 → ℚ)`. -/
@[simps!]
 def splitSMPlusH : (Fin 18 ⊕ Fin 2 → ℚ) ≃ (Fin 18 → ℚ) × (Fin 2 → ℚ) where
-  toFun f := (f ∘ Sum.inl , f ∘ Sum.inr)
+  toFun f := (f ∘ Sum.inl, f ∘ Sum.inr)
  invFun f := Sum.elim f.1 f.2
  left_inv f := Sum.elim_comp_inl_inr f
  right_inv _ := rfl
@ -473,8 +473,7 @@ def AnomalyFreeMk (S : MSSMACC.Charges) (hg : accGrav S = 0)
    intro i
    simp at i
    match i with
-    | 0 => exact hquad
-    ⟩ , by exact hcube ⟩
+    | 0 => exact hquad⟩, hcube⟩

 lemma AnomalyFreeMk_val (S : MSSMACC.Charges) (hg : accGrav S = 0)
    (hsu2 : accSU2 S = 0) (hsu3 : accSU3 S = 0) (hyy : accYY S = 0)
@ -490,8 +489,7 @@ def AnomalyFreeQuadMk' (S : MSSMACC.LinSols) (hquad : accQuad S.val = 0) :
    intro i
    simp at i
    match i with
-    | 0 => exact hquad
-    ⟩
+    | 0 => exact hquad⟩

 /-- A `Sol` from a `LinSol` satisfying the quadratic and cubic ACCs. -/
@[simp]
@ -501,13 +499,12 @@ def AnomalyFreeMk' (S : MSSMACC.LinSols) (hquad : accQuad S.val = 0)
    intro i
    simp at i
    match i with
-    | 0 => exact hquad
-    ⟩ , by exact hcube ⟩
+    | 0 => exact hquad⟩, hcube⟩

 /-- A `Sol` from a `QuadSol` satisfying the cubic ACCs. -/
@[simp]
 def AnomalyFreeMk'' (S : MSSMACC.QuadSols) (hcube : accCube S.val = 0) : MSSMACC.Sols :=
-  ⟨S , by exact hcube ⟩
+  ⟨S, hcube⟩

 lemma AnomalyFreeMk''_val (S : MSSMACC.QuadSols)
    (hcube : accCube S.val = 0) :
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
@ -52,7 +52,7 @@ lemma planeY₃B₃_val_eq' (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (hR' : R
  rw [planeY₃B₃_val, planeY₃B₃_val] at h
  have h1 := congrArg (fun S => dot Y₃.val S) h
  have h2 := congrArg (fun S => dot B₃.val S) h
-  simp only [ Fin.isValue, ACCSystemCharges.chargesAddCommMonoid_add, Fin.reduceFinMk] at h1 h2
+  simp only [Fin.isValue, ACCSystemCharges.chargesAddCommMonoid_add, Fin.reduceFinMk] at h1 h2
  erw [dot.map_add₂, dot.map_add₂] at h1 h2
  erw [dot.map_add₂ Y₃.val (a' • Y₃.val + b' • B₃.val) (c' • R.val)] at h1
  erw [dot.map_add₂ B₃.val (a' • Y₃.val + b' • B₃.val) (c' • R.val)] at h2
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
@ -105,7 +105,7 @@ lemma inQuadSolProp_iff_quadCoeff_zero (T : MSSMACC.Sols) : InQuadSolProp T ↔
  intro h
  rw [quadCoeff] at h
  rw [show dot Y₃.val B₃.val = 108 by rfl] at h
-  simp only [ Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq,
+  simp only [Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq,
    not_false_eq_true, pow_eq_zero_iff, or_self, false_or] at h
  apply (add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)).mp at h
  simp only [Fin.isValue, Fin.reduceFinMk, ne_eq, OfNat.ofNat_ne_zero,
@ -124,7 +124,7 @@ lemma inQuadSolProp_iff_proj_inQuadProp (R : MSSMACC.Sols) :
  simp only [Fin.isValue, Fin.reduceFinMk, mul_zero, add_zero, and_self]
  intro h
  rw [show dot Y₃.val B₃.val = 108 by rfl] at h
-  simp only [Fin.isValue, Fin.reduceFinMk , mul_eq_zero,
+  simp only [Fin.isValue, Fin.reduceFinMk, mul_eq_zero,
    OfNat.ofNat_ne_zero, or_self, false_or] at h
  rw [h.2.1, h.2.2]
  simp
@ -159,7 +159,7 @@ lemma inCubeSolProp_iff_cubicCoeff_zero (T : MSSMACC.Sols) :
  intro h
  rw [cubicCoeff] at h
  rw [show dot Y₃.val B₃.val = 108 by rfl] at h
-  simp only [ Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq,
+  simp only [Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq,
    not_false_eq_true, pow_eq_zero_iff, or_self, false_or] at h
  apply (add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)).mp at h
  simp only [Fin.isValue, Fin.reduceFinMk, ne_eq, OfNat.ofNat_ne_zero,
@ -232,7 +232,7 @@ lemma toSolNSQuad_eq_planeY₃B₃_on_α (R : MSSMACC.AnomalyFreePerp) :

 /-- Given an `R` perpendicular to `Y₃` and `B₃`, an element of `Sols`. This map is
 not surjective. -/
-def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _ , _) =>
+def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _, _) =>
  a • AnomalyFreeMk'' (toSolNSQuad R) (toSolNSQuad_cube R)

 /-- A map from `Sols` to `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` which on elements of
@ -268,7 +268,7 @@ def inLineEqToSol : InLineEq × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, c

 /-- On elements of `inLineEqSol` a right-inverse to `inLineEqSol`. -/
 def inLineEqProj (T : InLineEqSol) : InLineEq × ℚ × ℚ × ℚ :=
-  (⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 ⟩,
+  (⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1⟩,
  (quadCoeff T.val)⁻¹ * quadBiLin B₃.val T.val.val,
  (quadCoeff T.val)⁻¹ * (- quadBiLin Y₃.val T.val.val),
  (quadCoeff T.val)⁻¹ * (
@ -319,7 +319,7 @@ lemma inQuadToSol_smul (R : InQuad) (c₁ c₂ c₃ d : ℚ) :

 /-- On elements of `inQuadSol` a right-inverse to `inQuadToSol`. -/
 def inQuadProj (T : InQuadSol) : InQuad × ℚ × ℚ × ℚ :=
-  (⟨⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 ⟩,
+  (⟨⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1⟩,
    (inQuadSolProp_iff_proj_inQuadProp T.val).mp T.prop.2.1⟩,
  (cubicCoeff T.val)⁻¹ * (cubeTriLin T.val.val T.val.val B₃.val),
  (cubicCoeff T.val)⁻¹ * (- cubeTriLin T.val.val T.val.val Y₃.val),
@ -368,7 +368,7 @@ lemma inQuadCubeToSol_smul (R : InQuadCube) (c₁ c₂ c₃ d : ℚ) :

 /-- On elements of `inQuadCubeSol` a right-inverse to `inQuadCubeToSol`. -/
 def inQuadCubeProj (T : InQuadCubeSol) : InQuadCube × ℚ × ℚ × ℚ :=
-  (⟨⟨⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 ⟩,
+  (⟨⟨⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1⟩,
    (inQuadSolProp_iff_proj_inQuadProp T.val).mp T.prop.2.1⟩,
    (inCubeSolProp_iff_proj_inCubeProp T.val).mp T.prop.2.2⟩,
  (dot Y₃.val B₃.val)⁻¹ * (dot Y₃.val T.val.val - dot B₃.val T.val.val),
--- a/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean
@ -67,7 +67,7 @@ def repCharges : Representation ℚ PermGroup (MSSMCharges).Charges where
    rw [charges_eq_toSpecies_eq]
    refine And.intro ?_ $ Prod.mk.inj_iff.mp rfl
    intro i
-    simp only [ Pi.mul_apply, Pi.inv_apply, Equiv.Perm.coe_mul, LinearMap.mul_apply]
+    simp only [Pi.mul_apply, Pi.inv_apply, Equiv.Perm.coe_mul, LinearMap.mul_apply]
    rw [chargeMap_toSpecies, chargeMap_toSpecies]
    simp only [Pi.mul_apply, Pi.inv_apply]
    rw [chargeMap_toSpecies]
--- a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
@ -60,7 +60,7 @@ def asLinSols (j : Fin n) : (PureU1 n.succ).LinSols :=
    simp at i
    match i with
    | 0 =>
-    simp only [ Fin.isValue, PureU1_linearACCs, accGrav,
+    simp only [Fin.isValue, PureU1_linearACCs, accGrav,
      LinearMap.coe_mk, AddHom.coe_mk, Fin.coe_eq_castSucc]
    rw [Fin.sum_univ_castSucc]
    rw [Finset.sum_eq_single j]
--- a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
+++ b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
@ -148,7 +148,7 @@ lemma not_hasBoundary_zero_le (hnot : ¬ (HasBoundary S)) (h0 : S (0 : Fin n.suc
  induction i
  rfl
  rename_i i hii
-  have hnott := hnot ⟨i, by {simp at hi; linarith} ⟩
+  have hnott := hnot ⟨i, by {simp at hi; linarith}⟩
  have hii := hii (by omega)
  erw [← hii] at hnott
  exact (val_le_zero hS (hnott h0)).symm
--- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
@ -702,7 +702,7 @@ lemma span_basis_swap! {S : (PureU1 (2 * n.succ)).LinSols} (j : Fin n)
    (pairSwap (δ!₁ j) (δ!₂ j))) S = S') (g : Fin n.succ → ℚ) (f : Fin n → ℚ)
     (h : S.val = P g + P! f):
    ∃
-    (g' : Fin n.succ → ℚ) (f' : Fin n → ℚ) ,
+    (g' : Fin n.succ → ℚ) (f' : Fin n → ℚ),
     S'.val = P g' + P! f' ∧ P! f' = P! f +
    (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∧ g' = g := by
  let X := P! f + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j
--- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
@ -37,11 +37,11 @@ open VectorLikeEvenPlane
 /-- A property on `LinSols`, satisfied if every point on the line between the two planes
 in the basis through that point is in the cubic. -/
 def LineInCubic (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
-  ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) ,
+  ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ),
  accCube (2 * n.succ) (a • P g + b • P! f) = 0

 lemma lineInCubic_expand {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) :
-    ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) ,
+    ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ),
    3 * a * b * (a * accCubeTriLinSymm (P g) (P g) (P! f)
    + b * accCubeTriLinSymm (P! f) (P! f) (P g)) = 0 := by
  intro g f hS a b
@ -90,7 +90,7 @@ lemma lineInCubicPerm_permute {S : (PureU1 (2 * n.succ)).LinSols}

 lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ)).LinSols}
    (LIC : LineInCubicPerm S) :
-    ∀ (j : Fin n) (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) ,
+    ∀ (j : Fin n) (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f),
      (S.val (δ!₂ j) - S.val (δ!₁ j))
      * accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := by
  intro j g f h
--- a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
@ -80,7 +80,7 @@ lemma anomalyFree_param {S : (PureU1 (2 * n.succ)).Sols}
 /-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠ 0`.
 In this case our parameterization above will be able to recover this point. -/
 def GenericCase (S : (PureU1 (2 * n.succ)).Sols) : Prop :=
-  ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) ,
+  ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f),
  accCubeTriLinSymm (P g) (P g) (P! f) ≠ 0

 lemma genericCase_exists (S : (PureU1 (2 * n.succ)).Sols)
@ -95,7 +95,7 @@ lemma genericCase_exists (S : (PureU1 (2 * n.succ)).Sols)

 /-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) = 0`. -/
 def SpecialCase (S : (PureU1 (2 * n.succ)).Sols) : Prop :=
-  ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) ,
+  ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f),
  accCubeTriLinSymm (P g) (P g) (P! f) = 0

 lemma specialCase_exists (S : (PureU1 (2 * n.succ)).Sols)
--- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
@ -658,7 +658,7 @@ noncomputable def basisaAsBasis :
  basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card

 lemma span_basis (S : (PureU1 (2 * n.succ + 1)).LinSols) :
-    ∃ (g f : Fin n.succ → ℚ) , S.val = P g + P! f := by
+    ∃ (g f : Fin n.succ → ℚ), S.val = P g + P! f := by
  have h := (mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisaAsBasis S)
  obtain ⟨f, hf⟩ := h
  simp [basisaAsBasis] at hf
--- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
@ -37,11 +37,11 @@ open VectorLikeOddPlane
 /-- A property on `LinSols`, satisfied if every point on the line between the two planes
 in the basis through that point is in the cubic. -/
 def LineInCubic (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
-  ∀ (g f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) ,
+  ∀ (g f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ),
  accCube (2 * n + 1) (a • P g + b • P! f) = 0

 lemma lineInCubic_expand {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S) :
-    ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) (a b : ℚ) ,
+    ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) (a b : ℚ),
    3 * a * b * (a * accCubeTriLinSymm (P g) (P g) (P! f)
    + b * accCubeTriLinSymm (P! f) (P! f) (P g)) = 0 := by
  intro g f hS a b
@ -85,7 +85,7 @@ lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols}

 lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
    (LIC : LineInCubicPerm S) :
-    ∀ (j : Fin n.succ) (g f : Fin n.succ → ℚ) (_ : S.val = Pa g f) ,
+    ∀ (j : Fin n.succ) (g f : Fin n.succ → ℚ) (_ : S.val = Pa g f),
      (S.val (δ!₂ j) - S.val (δ!₁ j))
      * accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := by
  intro j g f h
--- a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
@ -78,7 +78,7 @@ lemma anomalyFree_param {S : (PureU1 (2 * n + 1)).Sols}
 /-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠ 0`.
 In this case our parameterization above will be able to recover this point. -/
 def GenericCase (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
-  ∀ (g f : Fin n.succ → ℚ) (_ : S.val = P g + P! f) ,
+  ∀ (g f : Fin n.succ → ℚ) (_ : S.val = P g + P! f),
  accCubeTriLinSymm (P g) (P g) (P! f) ≠ 0

 lemma genericCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
@ -94,7 +94,7 @@ lemma genericCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
 /-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠ 0`.
 In this case we will show that S is zero if it is true for all permutations. -/
 def SpecialCase (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
-  ∀ (g f : Fin n.succ → ℚ) (_ : S.val = P g + P! f) ,
+  ∀ (g f : Fin n.succ → ℚ) (_ : S.val = P g + P! f),
  accCubeTriLinSymm (P g) (P g) (P! f) = 0

 lemma specialCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@ -116,7 +116,7 @@ lemma cubic_zero_E'_zero (S : linearParameters) (hc : accCube (S.asCharges) = 0)
 def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
  toFun S := S.asLinear
  invFun S := ⟨SMCharges.Q S.val (0 : Fin 1), (SMCharges.U S.val (0 : Fin 1) -
-     SMCharges.D S.val (0 : Fin 1))/2 ,
+     SMCharges.D S.val (0 : Fin 1))/2,
     SMCharges.E S.val (0 : Fin 1)⟩
  left_inv S := by
    apply linearParameters.ext
--- a/HepLean/AnomalyCancellation/SMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Basic.lean
@ -164,7 +164,7 @@ def accSU3 : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
  map_add' S T := by
    simp only
    repeat rw [map_add]
-    simp [ Pi.add_apply, mul_add]
+    simp [Pi.add_apply, mul_add]
    repeat erw [Finset.sum_add_distrib]
    ring
  map_smul' a S := by
--- a/HepLean/FeynmanDiagrams/Basic.lean
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@ -543,7 +543,7 @@ def Cond {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 →

 lemma cond_satisfied {F G : FeynmanDiagram P} (f : Hom F G) :
    Cond f.𝓔 f.𝓥 f.𝓱𝓔 :=
-  ⟨fun x => congrFun f.𝓔𝓞.w x, fun x => congrFun f.𝓥𝓞.w x, fun x => congrFun f.𝓱𝓔To𝓔𝓥.w x ⟩
+  ⟨fun x => congrFun f.𝓔𝓞.w x, fun x => congrFun f.𝓥𝓞.w x, fun x => congrFun f.𝓱𝓔To𝓔𝓥.w x⟩

 lemma cond_symm {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.𝓥 ≃ G.𝓥) (𝓱𝓔 : F.𝓱𝓔 ≃ G.𝓱𝓔)
    (h : Cond 𝓔 𝓥 𝓱𝓔) : Cond 𝓔.symm 𝓥.symm 𝓱𝓔.symm := by
--- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
@ -67,7 +67,7 @@ lemma phaseShift_coe_matrix (a b c : ℝ) : ↑(phaseShift a b c) = phaseShiftMa

 /-- The equivalence relation between CKM matrices. -/
 def PhaseShiftRelation (U V : unitaryGroup (Fin 3) ℂ) : Prop :=
-  ∃ a b c e f g , U = phaseShift a b c * V * phaseShift e f g
+  ∃ a b c e f g, U = phaseShift a b c * V * phaseShift e f g

 lemma phaseShiftRelation_refl (U : unitaryGroup (Fin 3) ℂ) : PhaseShiftRelation U U := by
  use 0, 0, 0, 0, 0, 0
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
@ -47,7 +47,7 @@ lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
    cons_val_fin_one, star_mul', RCLike.star_def, conj_ofReal, cons_val_one, head_cons, star_sub,
    star_neg, ← exp_conj, _root_.map_mul, conj_I, neg_mul, cons_val_two, tail_cons, head_fin_const]
  simp [conj_ofReal]
-  rw [exp_neg ]
+  rw [exp_neg]
  fin_cases i <;> simp
  · ring_nf
    field_simp
@ -182,7 +182,7 @@ lemma mulExpδ₁₃_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤
    (h2 : 0 ≤ Real.cos θ₁₃) (h3 : 0 ≤ Real.sin θ₂₃) (h4 : 0 ≤ Real.cos θ₁₂) :
    mulExpδ₁₃ ⟦standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ =
    sin θ₁₂ * cos θ₁₃ ^ 2 * sin θ₂₃ * sin θ₁₃ * cos θ₁₂ * cos θ₂₃ * cexp (I * δ₁₃) := by
-  rw [mulExpδ₁₃, VusVubVcdSq_eq _ _ _ _ h1 h2 h3 h4 ]
+  rw [mulExpδ₁₃, VusVubVcdSq_eq _ _ _ _ h1 h2 h3 h4]
  simp only [jarlskogℂ, standParam, standParamAsMatrix, neg_mul,
    Quotient.lift_mk, jarlskogℂCKM, Fin.isValue, cons_val', cons_val_one, head_cons,
    empty_val', cons_val_fin_one, cons_val_zero, cons_val_two, tail_cons, _root_.map_mul, ←
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
@ -250,7 +250,7 @@ lemma C₂₃_of_Vub_neq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1
  simp only [VcbAbs, Fin.isValue, VtbAbs, add_sub_cancel_left]
  rw [Real.sqrt_div (sq_nonneg (VAbs 2 2 V))]
  rw [Real.sqrt_sq (VAbs_ge_zero 2 2 V)]
-  rw [VcbAbs_sq_add_VtbAbs_sq, ← VudAbs_sq_add_VusAbs_sq ]
+  rw [VcbAbs_sq_add_VtbAbs_sq, ← VudAbs_sq_add_VusAbs_sq]
  exact VAbsub_neq_zero_Vud_Vus_neq_zero ha
  exact (Left.add_nonneg (sq_nonneg (VAbs 0 0 V)) (sq_nonneg (VAbs 0 1 V)))

@ -506,7 +506,7 @@ lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0
    simp [VAbs, hb]
  have h1 : ofReal (√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) *
    ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2)) = ofReal (VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) := by
-    rw [Real.mul_self_sqrt ]
+    rw [Real.mul_self_sqrt]
    apply add_nonneg (sq_nonneg _) (sq_nonneg _)
  simp at h1
  have hx := Vabs_sq_add_neq_zero hb
--- a/HepLean/Mathematics/SO3/Basic.lean
+++ b/HepLean/Mathematics/SO3/Basic.lean
@ -121,7 +121,7 @@ lemma toGL_embedding : Embedding toGL.toFun where
  induced := by
    refine ((fun {X} {t t'} => TopologicalSpace.ext_iff.mpr) ?_).symm
    intro s
-    rw [TopologicalSpace.ext_iff.mp toProd_embedding.induced s ]
+    rw [TopologicalSpace.ext_iff.mp toProd_embedding.induced s]
    rw [isOpen_induced_iff, isOpen_induced_iff]
    apply Iff.intro ?_ ?_
    · intro h
@ -208,7 +208,7 @@ lemma exists_stationary_vec (A : SO(3)) :
  rw [inner_smul_right, inner_smul_left, real_inner_self_eq_norm_sq v]
  field_simp
  ring
-  rw [_root_.map_smul, End.mem_eigenspace_iff.mp hv.1 ]
+  rw [_root_.map_smul, End.mem_eigenspace_iff.mp hv.1]
  simp

 lemma exists_basis_preserved (A : SO(3)) :
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@ -224,7 +224,7 @@ lemma toGL_embedding : Embedding (@toGL d).toFun where
  induced := by
    refine ((fun {X} {t t'} => TopologicalSpace.ext_iff.mpr) ?_).symm
    intro s
-    rw [TopologicalSpace.ext_iff.mp toProd_embedding.induced s ]
+    rw [TopologicalSpace.ext_iff.mp toProd_embedding.induced s]
    rw [isOpen_induced_iff, isOpen_induced_iff]
    exact exists_exists_and_eq_and

--- a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
@ -143,7 +143,7 @@ lemma mul_markedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
    T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))
    * S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
  apply Finset.sum_congr rfl (fun x _ => ?_)
-  rw [Finset.sum_mul_sum ]
+  rw [Finset.sum_mul_sum]
  apply Finset.sum_congr rfl (fun j _ => ?_)
  apply Finset.sum_congr rfl (fun k _ => ?_)
  ring
@ -189,7 +189,7 @@ lemma mul_unmarkedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
       toTensorRepMat Λ (indexValueSumEquiv i).2 k *
      S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
  apply Finset.sum_congr rfl (fun x _ => ?_)
-  rw [Finset.sum_mul_sum ]
+  rw [Finset.sum_mul_sum]
  apply Finset.sum_congr rfl (fun j _ => ?_)
  apply Finset.sum_congr rfl (fun k _ => ?_)
  ring
--- a/HepLean/SpaceTime/LorentzVector/NormOne.lean
+++ b/HepLean/SpaceTime/LorentzVector/NormOne.lean
@ -160,7 +160,7 @@ variable {v w : NormOneLorentzVector d}
 lemma metric_reflect_mem_mem (h : v ∈ FuturePointing d) (hw : w ∈ FuturePointing d) :
    0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ := by
  apply le_trans (time_abs_sub_space_norm v w)
-  rw [abs_time ⟨v, h⟩, abs_time ⟨w, hw⟩ , sub_eq_add_neg, right_spaceReflection]
+  rw [abs_time ⟨v, h⟩, abs_time ⟨w, hw⟩, sub_eq_add_neg, right_spaceReflection]
  apply (add_le_add_iff_left _).mpr
  rw [neg_le]
  apply le_trans (neg_le_abs _ : _ ≤ |⟪(v.1).space, (w.1).space⟫_ℝ|) ?_
@ -223,7 +223,7 @@ noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFutur
      apply Finset.sum_congr rfl
      intro i _
      ring
-      exact Right.add_nonneg (zero_le_one' ℝ) $ mul_nonneg (sq_nonneg _) (sq_nonneg _) ⟩,
+      exact Right.add_nonneg (zero_le_one' ℝ) $ mul_nonneg (sq_nonneg _) (sq_nonneg _)⟩,
    by
      simp only [space, Function.comp_apply, mem_iff_time_nonneg, time, Real.sqrt_pos]
      exact Real.sqrt_nonneg _⟩
--- a/HepLean/SpaceTime/SL2C/Basic.lean
+++ b/HepLean/SpaceTime/SL2C/Basic.lean
@ -102,7 +102,7 @@ lemma iff_det_selfAdjoint (Λ : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ)
 /-- Given an element `M ∈ SL(2, ℂ)` the corresponding element of the Lorentz group. -/
@[simps!]
 def toLorentzGroupElem (M : SL(2, ℂ)) : LorentzGroup 3 :=
-  ⟨LinearMap.toMatrix LorentzVector.stdBasis LorentzVector.stdBasis (repLorentzVector M) ,
+  ⟨LinearMap.toMatrix LorentzVector.stdBasis LorentzVector.stdBasis (repLorentzVector M),
   by simp [repLorentzVector, iff_det_selfAdjoint]⟩

 /-- The group homomorphism from ` SL(2, ℂ)` to the Lorentz group `𝓛`. -/
--- a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
+++ b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
@ -94,11 +94,11 @@ lemma rep_apply (g : GaugeGroup) (φ : HiggsVec) : rep g φ = g.2.2 ^ 3 • (g.2
 /-- Given a Higgs vector, a rotation matrix which puts the first component of the
 vector to zero, and the second component to a real -/
 def rotateMatrix (φ : HiggsVec) : Matrix (Fin 2) (Fin 2) ℂ :=
-  ![![φ 1 /‖φ‖ , - φ 0 /‖φ‖], ![conj (φ 0) / ‖φ‖ , conj (φ 1) / ‖φ‖] ]
+  ![![φ 1 /‖φ‖, - φ 0 /‖φ‖], ![conj (φ 0) / ‖φ‖, conj (φ 1) / ‖φ‖]]

 lemma rotateMatrix_star (φ : HiggsVec) :
    star φ.rotateMatrix =
-    ![![conj (φ 1) /‖φ‖ , φ 0 /‖φ‖], ![- conj (φ 0) / ‖φ‖ , φ 1 / ‖φ‖] ] := by
+    ![![conj (φ 1) /‖φ‖, φ 0 /‖φ‖], ![- conj (φ 0) / ‖φ‖, φ 1 / ‖φ‖]] := by
  simp_rw [star, rotateMatrix, conjTranspose]
  ext i j
  fin_cases i <;> fin_cases j <;> simp [conj_ofReal]
--- a/scripts/hepLean_style_lint.lean
+++ b/scripts/hepLean_style_lint.lean
@ -84,7 +84,9 @@ def hepLeanLintFile (path : FilePath) : IO Bool := do
    (Array.map (fun (e, n, c) ↦ HepLeanErrorContext.mk e n c path)) (lint lines)))
    #[doubleEmptyLineLinter, doubleSpaceLinter, substringLinter ".-/", substringLinter " )",
    substringLinter "( ", substringLinter "=by", substringLinter "  def ",
-    substringLinter "/-- We "]
+    substringLinter "/-- We ", substringLinter "[ ", substringLinter " ]", substringLinter " ,"
+    , substringLinter "by exact ",
+     substringLinter "⟨ ", substringLinter " ⟩"]
  let errors := allOutput.flatten
  printErrors errors
  return errors.size > 0