From f03d063c86c4b01c589344ce4c0a5d2708cf6671 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 3 Jul 2024 07:56:30 -0400
Subject: [PATCH] refactor: Remove double empty lines

---
 .../MSSMNu/OrthogY3B3/PlaneWithY3B3.lean         |  5 -----
 .../MSSMNu/OrthogY3B3/ToSols.lean                |  4 ----
 HepLean/AnomalyCancellation/PureU1/Basic.lean    |  3 ---
 .../AnomalyCancellation/PureU1/BasisLinear.lean  |  2 --
 HepLean/AnomalyCancellation/PureU1/ConstAbs.lean |  5 -----
 .../PureU1/Even/BasisLinear.lean                 |  5 -----
 .../PureU1/Even/Parameterization.lean            |  3 ---
 .../PureU1/LineInPlaneCond.lean                  |  5 -----
 .../AnomalyCancellation/PureU1/LowDim/Three.lean |  1 -
 .../PureU1/Odd/BasisLinear.lean                  |  7 -------
 .../PureU1/Odd/LineInCubic.lean                  |  4 ----
 .../PureU1/Odd/Parameterization.lean             |  1 -
 .../AnomalyCancellation/PureU1/Permutations.lean |  4 ----
 HepLean/AnomalyCancellation/PureU1/Sort.lean     |  1 -
 .../AnomalyCancellation/PureU1/VectorLike.lean   |  2 --
 HepLean/AnomalyCancellation/SM/Basic.lean        |  1 -
 .../SM/NoGrav/One/Lemmas.lean                    |  4 ----
 .../SM/NoGrav/One/LinearParameterization.lean    |  3 ---
 HepLean/AnomalyCancellation/SM/Permutations.lean |  6 ------
 HepLean/AnomalyCancellation/SMNu/Basic.lean      |  5 -----
 HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean |  1 -
 .../AnomalyCancellation/SMNu/NoGrav/Basic.lean   |  1 -
 .../AnomalyCancellation/SMNu/Ordinary/Basic.lean |  2 --
 .../SMNu/Ordinary/DimSevenPlane.lean             |  3 ---
 .../AnomalyCancellation/SMNu/Permutations.lean   |  7 -------
 .../AnomalyCancellation/SMNu/PlusU1/BMinusL.lean |  1 -
 .../AnomalyCancellation/SMNu/PlusU1/Basic.lean   |  1 -
 .../SMNu/PlusU1/BoundPlaneDim.lean               |  2 --
 .../SMNu/PlusU1/HyperCharge.lean                 |  2 --
 .../SMNu/PlusU1/PlaneNonSols.lean                |  3 ---
 .../AnomalyCancellation/SMNu/PlusU1/QuadSol.lean |  1 -
 .../SMNu/PlusU1/QuadSolToSol.lean                |  2 --
 HepLean/FeynmanDiagrams/Basic.lean               | 10 ----------
 .../FeynmanDiagrams/Instances/ComplexScalar.lean |  6 ------
 HepLean/FeynmanDiagrams/Instances/Phi4.lean      |  4 ----
 HepLean/FeynmanDiagrams/Momentum.lean            |  6 ------
 HepLean/FlavorPhysics/CKMMatrix/Basic.lean       |  7 -------
 HepLean/FlavorPhysics/CKMMatrix/Invariants.lean  |  4 ----
 .../FlavorPhysics/CKMMatrix/PhaseFreedom.lean    |  3 ---
 HepLean/FlavorPhysics/CKMMatrix/Relations.lean   | 13 -------------
 HepLean/FlavorPhysics/CKMMatrix/Rows.lean        |  2 --
 .../StandardParameterization/Basic.lean          |  3 ---
 .../StandardParameters.lean                      | 16 ----------------
 HepLean/Mathematics/LinearMaps.lean              |  5 -----
 HepLean/Mathematics/SO3/Basic.lean               |  5 -----
 HepLean/SpaceTime/Basic.lean                     |  1 -
 HepLean/SpaceTime/LorentzAlgebra/Basic.lean      |  8 --------
 HepLean/SpaceTime/LorentzGroup/Basic.lean        |  1 -
 HepLean/SpaceTime/LorentzGroup/Boosts.lean       |  4 ----
 .../SpaceTime/LorentzGroup/Orthochronous.lean    |  3 ---
 HepLean/SpaceTime/LorentzGroup/Proper.lean       |  4 ----
 HepLean/SpaceTime/LorentzGroup/Rotations.lean    |  2 --
 .../LorentzVector/AsSelfAdjointMatrix.lean       |  1 -
 HepLean/SpaceTime/LorentzVector/Basic.lean       |  1 -
 HepLean/SpaceTime/LorentzVector/NormOne.lean     | 10 ----------
 HepLean/SpaceTime/MinkowskiMetric.lean           |  9 ---------
 HepLean/SpaceTime/SL2C/Basic.lean                |  2 --
 HepLean/StandardModel/HiggsBoson/Basic.lean      |  2 --
 .../StandardModel/HiggsBoson/TargetSpace.lean    |  2 --
 HepLean/StandardModel/Representations.lean       |  1 -
 60 files changed, 232 deletions(-)

diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
index d7d984d..9832ed2 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
@@ -18,8 +18,6 @@ The plane spanned by Y₃, B₃ and third orthogonal point.
 
 -/
 
-
-
 universe v u
 
 namespace MSSMACC
@@ -93,7 +91,6 @@ lemma planeY₃B₃_val_eq' (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (hR' : R
   rw [ha, hb, hc]
   simp
 
-
 lemma planeY₃B₃_quad (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
     accQuad (planeY₃B₃ R a b c).val = c * (2 * a * quadBiLin Y₃.val R.val
     + 2 * b * quadBiLin B₃.val R.val + c * quadBiLin R.val R.val) := by
@@ -184,7 +181,6 @@ def lineCube (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
     (3 * a₃ * cubeTriLin R.val R.val Y₃.val -  a₁ * cubeTriLin R.val R.val R.val)
     (3 * (a₁ * cubeTriLin R.val R.val B₃.val - a₂ * cubeTriLin R.val R.val Y₃.val))
 
-
 lemma lineCube_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
     lineCube R (d * a) (d * b) (d * c) = d • lineCube R a b c := by
   apply ACCSystemLinear.LinSols.ext
@@ -241,5 +237,4 @@ lemma α₂_proj_zero (T : MSSMACC.Sols) (h1 : α₃ (proj T.1.1) = 0) :
 
 end proj
 
-
 end MSSMACC
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
index 2023709..659f847 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
@@ -18,7 +18,6 @@ To define `toSols` we define a series of other maps from various subtypes of
 `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` to `MSSMACC.Sols`. And show that these maps form a
 surjection on certain subtypes of `MSSMACC.Sols`.
 
-
 # References
 
 The main reference for the material in this file is:
@@ -78,7 +77,6 @@ lemma linEqPropSol_iff_proj_linEqProp (R : MSSMACC.Sols) :
   rw [h.2.2]
   simp
 
-
 /-- A condition which is satisfied if the plane spanned by `R`, `Y₃` and `B₃` lies
 entirely in the quadratic surface. -/
 def InQuadProp (R : MSSMACC.AnomalyFreePerp) : Prop :=
@@ -237,7 +235,6 @@ not surjective. -/
 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
 `notInLineEqSol` will produce a right inverse to `toSolNS`. -/
 def toSolNSProj (T : MSSMACC.Sols) : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ :=
@@ -457,7 +454,6 @@ theorem toSol_surjective : Function.Surjective toSol := by
   simp at h₃
   exact toSol_inQuadCube ⟨T, And.intro h₁ (And.intro h₂ h₃)⟩
 
-
 end AnomalyFreePerp
 
 end MSSMACC
diff --git a/HepLean/AnomalyCancellation/PureU1/Basic.lean b/HepLean/AnomalyCancellation/PureU1/Basic.lean
index c26827f..b5ab703 100644
--- a/HepLean/AnomalyCancellation/PureU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Basic.lean
@@ -16,7 +16,6 @@ We define the anomaly cancellation conditions for a pure U(1) gauge theory with
 universe v u
 open Nat
 
-
 open  Finset
 
 namespace PureU1
@@ -35,7 +34,6 @@ def accGrav (n : ℕ) : ((PureU1Charges n).Charges →ₗ[ℚ] ℚ) where
    simp [HSMul.hSMul, SMul.smul]
    rw [← Finset.mul_sum]
 
-
 /-- The symmetric trilinear form used to define the cubic anomaly. -/
 @[simps!]
 def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).Charges := TriLinearSymm.mk₃
@@ -162,7 +160,6 @@ lemma sum_of_charges {n : ℕ} (f : Fin k → (PureU1 n).Charges) (j : Fin n) :
   erw [← hlt]
   simp
 
-
 lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
     (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) := by
   induction k
diff --git a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
index f9bbcc4..746e2d6 100644
--- a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
@@ -75,7 +75,6 @@ def asLinSols (j : Fin n) : (PureU1 n.succ).LinSols :=
     intro hk
     simp at hk⟩
 
-
 lemma sum_of_vectors {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
     (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) :=
   sum_of_anomaly_free_linear (fun i => f i) j
@@ -134,5 +133,4 @@ lemma finrank_AnomalyFreeLinear :
 
 end BasisLinear
 
-
 end PureU1
diff --git a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
index a5e4004..3189e4c 100644
--- a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
+++ b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
@@ -120,7 +120,6 @@ lemma boundary_accGrav' (k : Fin n) : accGrav n.succ S =
   intro i
   simp
 
-
 lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) :
     accGrav n.succ S = (2 * ↑↑k + 1 - ↑n) * S (0 : Fin n.succ) := by
   rw [boundary_accGrav' k]
@@ -165,7 +164,6 @@ lemma not_hasBoundary_grav (hnot :  ¬ (HasBoundary S)) :
     accGrav n.succ S = n.succ * S (0 : Fin n.succ) := by
   simp [accGrav, ← not_hasBoundry_zero hS hnot]
 
-
 lemma AFL_hasBoundary (h : A.val (0 : Fin n.succ) ≠ 0) : HasBoundary A.val := by
   by_contra hn
   have h0 := not_hasBoundary_grav hA hn
@@ -253,12 +251,10 @@ lemma AFL_even_above (A : (PureU1 (2 * n.succ)).LinSols) (h : ConstAbsSorted A.v
   rfl
   exact AFL_even_above' h hA i
 
-
 end charges
 
 end ConstAbsSorted
 
-
 namespace ConstAbs
 
 theorem boundary_value_odd (S : (PureU1 (2 * n + 1)).LinSols) (hs : ConstAbs S.val) :
@@ -266,7 +262,6 @@ theorem boundary_value_odd (S : (PureU1 (2 * n + 1)).LinSols) (hs : ConstAbs S.v
   have hS := And.intro (constAbs_sort hs) (sort_sorted S.val)
   sortAFL_zero S (ConstAbsSorted.AFL_odd (sortAFL S) hS)
 
-
 theorem boundary_value_even (S : (PureU1 (2 * n.succ)).LinSols) (hs : ConstAbs S.val) :
     VectorLikeEven S.val := by
   have hS := And.intro (constAbs_sort hs) (sort_sorted S.val)
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
index 994c01c..1d7e915 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
@@ -190,7 +190,6 @@ lemma basis!_on_other {k : Fin n} {j : Fin (2 * n.succ)} (h1 : j ≠ δ!₁ k)
   simp [basis!AsCharges]
   simp_all only [ne_eq, ↓reduceIte]
 
-
 lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
     basis!AsCharges k (δ!₁ j) = 0 := by
   simp [basis!AsCharges]
@@ -310,7 +309,6 @@ lemma basis!_accCube (j : Fin n) :
   simp [basis!_δ!₂_eq_minus_δ!₁]
   ring
 
-
 /-- The first part of the basis as `LinSols`. -/
 @[simps!]
 def basis (j : Fin n.succ) : (PureU1 (2 * n.succ)).LinSols :=
@@ -587,7 +585,6 @@ theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by
   rw [P!'_val] at h1
   exact P!_zero f h1
 
-
 theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n) := by
   apply Fintype.linearIndependent_iff.mpr
   intro f h
@@ -663,7 +660,6 @@ lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) :
   rw [← join_ext]
   exact Pa'_eq _ _
 
-
 lemma basisa_card :  Fintype.card ((Fin n.succ) ⊕ (Fin n)) =
     FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ)).LinSols := by
   erw [BasisLinear.finrank_AnomalyFreeLinear]
@@ -675,7 +671,6 @@ noncomputable def basisaAsBasis :
     Basis (Fin (succ n) ⊕ Fin n) ℚ (PureU1 (2 * succ n)).LinSols :=
   basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card
 
-
 lemma span_basis (S : (PureU1 (2 * n.succ)).LinSols) :
     ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f  := by
   have h := (mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisaAsBasis S)
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
index aa58459..db11575 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
@@ -134,7 +134,6 @@ theorem generic_case {S : (PureU1 (2 * n.succ)).Sols} (h : GenericCase S) :
   simp at h
   exact h
 
-
 lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols}
     (h : SpecialCase S) : LineInCubic S.1.1 := by
   intro g f hS a b
@@ -152,7 +151,6 @@ lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols}
   erw [h]
   simp
 
-
 lemma special_case_lineInCubic_perm {S : (PureU1 (2 * n.succ)).Sols}
     (h : ∀ (M : (FamilyPermutations (2 * n.succ)).group),
     SpecialCase ((FamilyPermutations (2 * n.succ)).solAction.toFun S M)) :
@@ -160,7 +158,6 @@ lemma special_case_lineInCubic_perm {S : (PureU1 (2 * n.succ)).Sols}
   intro M
   exact special_case_lineInCubic (h M)
 
-
 theorem special_case {S : (PureU1 (2 * n.succ.succ)).Sols}
     (h : ∀ (M : (FamilyPermutations (2 * n.succ.succ)).group),
     SpecialCase ((FamilyPermutations (2 * n.succ.succ)).solAction.toFun S M)) :
diff --git a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
index 97f0209..4cfb260 100644
--- a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
@@ -26,7 +26,6 @@ We will show that `n ≥ 4` the `line in plane` condition on solutions implies t
 
 -/
 
-
 namespace PureU1
 
 open BigOperators
@@ -52,7 +51,6 @@ lemma lineInPlaneCond_perm {S : (PureU1 (n)).LinSols} (hS : LineInPlaneCond S)
   all_goals simp_all only [ne_eq, Equiv.invFun_as_coe, EmbeddingLike.apply_eq_iff_eq,
     not_false_eq_true]
 
-
 lemma lineInPlaneCond_eq_last' {S : (PureU1 (n.succ.succ)).LinSols} (hS : LineInPlaneCond S)
     (h : ¬ (S.val ((Fin.last n).castSucc))^2 = (S.val ((Fin.last n).succ))^2 ) :
     (2 - n) * S.val (Fin.last (n + 1)) =
@@ -157,7 +155,6 @@ lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : LineInPlaneCond S.1.1) :
   simp at h6
   simp_all
 
-
 lemma linesInPlane_eq_sq_four {S : (PureU1 4).Sols}
     (hS : LineInPlaneCond S.1.1) : ∀ (i j : Fin 4) (_ : i ≠ j),
     ConstAbsProp (S.val i, S.val j) := by
@@ -168,7 +165,6 @@ lemma linesInPlane_eq_sq_four {S : (PureU1 4).Sols}
     (lineInPlaneCond_perm hS M)
   exact linesInPlane_four S' hS'
 
-
 lemma linesInPlane_constAbs_four (S : (PureU1 4).Sols)
     (hS : LineInPlaneCond S.1.1) : ConstAbs S.val := by
   intro i j
@@ -183,5 +179,4 @@ theorem linesInPlane_constAbs_AF (S : (PureU1 (n.succ.succ.succ.succ)).Sols)
   exact linesInPlane_constAbs_four S hS
   exact linesInPlane_constAbs hS
 
-
 end PureU1
diff --git a/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean b/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean
index 15552a3..be0d389 100644
--- a/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean
@@ -50,7 +50,6 @@ def solOfLinear (S : (PureU1 3).LinSols)
   ⟨⟨S, by intro i; simp at i; exact Fin.elim0 i⟩,
     (cube_for_linSol S).mp hS⟩
 
-
 theorem solOfLinear_surjects (S : (PureU1 3).Sols) :
     ∃ (T : (PureU1 3).LinSols) (hT : T.val (0 : Fin 3) = 0 ∨ T.val (1 : Fin 3) = 0
     ∨ T.val (2 : Fin 3) = 0), solOfLinear T hT = S := by
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
index c6132d0..c7dc70e 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
@@ -23,7 +23,6 @@ namespace PureU1
 
 variable {n : ℕ}
 
-
 namespace VectorLikeOddPlane
 
 lemma split_odd! (n : ℕ) : (1 + n) + n = 2 * n +1 := by
@@ -484,7 +483,6 @@ lemma P_P_P!_accCube (g : Fin n → ℚ) (j : Fin n) :
   simp only [mul_zero, add_zero]
   simp
 
-
 lemma P_zero (f : Fin n → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by
   intro i
   erw [← P_δ₁ f]
@@ -572,7 +570,6 @@ theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by
   rw [P!'_val] at h1
   exact P!_zero f h1
 
-
 theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n.succ) := by
   apply Fintype.linearIndependent_iff.mpr
   intro f h
@@ -648,8 +645,6 @@ lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) :
   rw [← join_ext]
   exact Pa'_eq _ _
 
-
-
 lemma basisa_card :  Fintype.card ((Fin n.succ) ⊕ (Fin n.succ)) =
     FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ + 1)).LinSols := by
   erw [BasisLinear.finrank_AnomalyFreeLinear]
@@ -706,8 +701,6 @@ lemma span_basis_swap! {S : (PureU1 (2 * n.succ + 1)).LinSols} (j : Fin n.succ)
   apply swap!_as_add at hS
   exact hS
 
-
 end VectorLikeOddPlane
 
-
 end PureU1
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
index 477c597..3cc030f 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
@@ -54,7 +54,6 @@ lemma lineInCubic_expand {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S)
   rw [← h1]
   ring
 
-
 lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S) :
     ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val =  P g + P! f),
     accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by
@@ -62,8 +61,6 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S
   linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1 ) -
      (lineInCubic_expand h g f hS 1 2 ) / 6
 
-
-
 /-- We say a `LinSol` satisfies  `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
 def LineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
   ∀ (M : (FamilyPermutations (2 * n + 1)).group ),
@@ -86,7 +83,6 @@ lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols}
   rw [ht]
   exact hS (M * M')
 
-
 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) ,
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
index 1ded1c6..56ddddd 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
@@ -133,7 +133,6 @@ theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : GenericCase S) :
   simp at h
   exact h
 
-
 lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols}
     (h : SpecialCase S) :
       LineInCubic S.1.1 := by
diff --git a/HepLean/AnomalyCancellation/PureU1/Permutations.lean b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
index 084e2ce..c585e5c 100644
--- a/HepLean/AnomalyCancellation/PureU1/Permutations.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
@@ -96,7 +96,6 @@ def FamilyPermutations (n : ℕ) : ACCSystemGroupAction (PureU1 n) where
     exact Fin.elim0 i
   cubicInvariant := accCube_invariant
 
-
 lemma FamilyPermutations_charges_apply (S : (PureU1 n).Charges)
     (i : Fin n) (f : (FamilyPermutations n).group) :
     ((FamilyPermutations n).rep f S) i = S (f.invFun i) := by
@@ -107,7 +106,6 @@ lemma FamilyPermutations_anomalyFreeLinear_apply (S : (PureU1 n).LinSols)
     ((FamilyPermutations n).linSolRep f S).val i = S.val (f.invFun i) := by
   rfl
 
-
 /-- The permutation which swaps i and j. TODO: Replace with: `Equiv.swap`. -/
 def pairSwap {n : ℕ} (i j : Fin n) : (FamilyPermutations n).group where
   toFun s :=
@@ -247,7 +245,6 @@ lemma permThreeInj_fst_apply :
     ⟨i, permThreeInj_fst  hij hjk hik⟩ = 0 := by
   exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permThreeInj hij hjk hik))).mpr rfl
 
-
 lemma permThreeInj_snd : j ∈ Set.range ⇑(permThreeInj hij hjk hik) := by
   simp only [Set.mem_range]
   use 1
@@ -338,5 +335,4 @@ lemma Prop_three (P : ℚ × ℚ × ℚ → Prop) {S : (PureU1 n).LinSols}
   erw [permThree_fst,permThree_snd, permThree_thd] at h1
   exact h1
 
-
 end PureU1
diff --git a/HepLean/AnomalyCancellation/PureU1/Sort.lean b/HepLean/AnomalyCancellation/PureU1/Sort.lean
index 3438d32..eccf84b 100644
--- a/HepLean/AnomalyCancellation/PureU1/Sort.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Sort.lean
@@ -67,7 +67,6 @@ def sortAFL  {n : ℕ} (S : (PureU1 n).LinSols) : (PureU1 n).LinSols :=
 lemma sortAFL_val {n : ℕ} (S : (PureU1 n).LinSols) :  (sortAFL S).val = sort S.val := by
   rfl
 
-
 lemma sortAFL_zero {n : ℕ} (S : (PureU1 n).LinSols)  (hS : sortAFL S = 0) : S = 0 := by
   apply ACCSystemLinear.LinSols.ext
   have h1 : sort S.val = 0 := by
diff --git a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
index 29d6daa..2eed792 100644
--- a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
+++ b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
@@ -30,7 +30,6 @@ variable {n : ℕ}
 -/
 lemma split_equal (n : ℕ) : n + n = 2 * n := (Nat.two_mul n).symm
 
-
 lemma split_odd (n : ℕ) : n + 1 + n = 2 * n + 1 := by omega
 
 /-- A charge configuration for n even is vector like if when sorted the `i`th element
@@ -40,5 +39,4 @@ def VectorLikeEven  (S : (PureU1 (2 * n)).Charges) : Prop :=
   ∀ (i : Fin n), (sort S) (Fin.cast (split_equal n)  (Fin.castAdd n i))
   = - (sort S) (Fin.cast (split_equal n)  (Fin.natAdd n i))
 
-
 end PureU1
diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean
index 81f6804..f067f5e 100644
--- a/HepLean/AnomalyCancellation/SM/Basic.lean
+++ b/HepLean/AnomalyCancellation/SM/Basic.lean
@@ -319,5 +319,4 @@ lemma accCube_ext {S T : (SMCharges n).Charges}
     rfl
   repeat rw [h1]
 
-
 end SMACCs
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
index a14233f..c8d46eb 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
@@ -24,7 +24,6 @@ open SMCharges
 open SMACCs
 open BigOperators
 
-
 lemma E_zero_iff_Q_zero {S : (SMNoGrav 1).Sols} : Q S.val (0 : Fin 1) = 0 ↔
     E S.val  (0 : Fin 1) = 0 := by
   let S' := linearParameters.bijection.symm S.1.1
@@ -38,8 +37,6 @@ lemma E_zero_iff_Q_zero {S : (SMNoGrav 1).Sols} : Q S.val (0 : Fin 1) = 0 ↔
   intro hE
   exact S'.cubic_zero_E'_zero hC hE
 
-
-
 lemma accGrav_Q_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val  (0 : Fin 1) = 0) :
     accGrav S.val = 0 := by
   rw [accGrav]
@@ -74,7 +71,6 @@ theorem accGravSatisfied {S : (SMNoGrav 1).Sols} (FLTThree : FermatLastTheoremWi
   exact accGrav_Q_zero hQ
   exact accGrav_Q_neq_zero hQ FLTThree
 
-
 end One
 end SMNoGrav
 end SM
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
index 43ddbd0..126bf37 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@@ -183,7 +183,6 @@ lemma grav (S : linearParameters) :
 
 end linearParameters
 
-
 /-- The parameters for solutions to the linear ACCs with the condition that Q and E are non-zero.-/
 structure linearParametersQENeqZero where
   /-- The parameter `x`. -/
@@ -280,7 +279,6 @@ lemma cubic (S : linearParametersQENeqZero) :
   simp_all
   exact add_eq_zero_iff_eq_neg
 
-
 lemma cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
     (FLTThree : FermatLastTheoremWith ℚ 3) :
     S.v = 0 ∨ S.w = 0 := by
@@ -364,7 +362,6 @@ lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1
 
 end linearParametersQENeqZero
 
-
 end One
 end SMNoGrav
 end SM
diff --git a/HepLean/AnomalyCancellation/SM/Permutations.lean b/HepLean/AnomalyCancellation/SM/Permutations.lean
index 5c6af44..0dda836 100644
--- a/HepLean/AnomalyCancellation/SM/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SM/Permutations.lean
@@ -33,7 +33,6 @@ variable {n : ℕ}
 @[simp]
 instance : Group (PermGroup n) := Pi.group
 
-
 /-- The image of an element of `permGroup n` under the representation on charges. -/
 @[simps!]
 def chargeMap (f : PermGroup n) : (SMCharges n).Charges →ₗ[ℚ] (SMCharges n).Charges where
@@ -66,7 +65,6 @@ lemma repCharges_toSpecies (f : PermGroup n) (S : (SMCharges n).Charges) (j : Fi
     toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j := by
   erw [toSMSpecies_toSpecies_inv]
 
-
 lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMCharges n).Charges) (j : Fin 5) :
     ∑ i, ((fun a => a ^ m) ∘ toSpecies j (repCharges f S)) i =
     ∑ i, ((fun a => a ^ m) ∘ toSpecies j S) i := by
@@ -74,20 +72,16 @@ lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMCharges n).Cha
   exact Fintype.sum_equiv (f⁻¹ j) (fun x => ((fun a => a ^ m) ∘ (toSpecies j) S ∘ ⇑(f⁻¹ j)) x)
    (fun x => ((fun a => a ^ m) ∘ (toSpecies j) S) x) (congrFun rfl)
 
-
-
 lemma accGrav_invariant (f : PermGroup n) (S : (SMCharges n).Charges)  :
     accGrav (repCharges f S) = accGrav S :=
   accGrav_ext
     (by simpa using toSpecies_sum_invariant 1 f S)
 
-
 lemma accSU2_invariant (f : PermGroup n) (S : (SMCharges n).Charges)  :
     accSU2 (repCharges f S) = accSU2 S :=
   accSU2_ext
     (by simpa using toSpecies_sum_invariant 1 f S)
 
-
 lemma accSU3_invariant (f : PermGroup n) (S : (SMCharges n).Charges)  :
     accSU3 (repCharges f S) = accSU3 S :=
   accSU3_ext
diff --git a/HepLean/AnomalyCancellation/SMNu/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Basic.lean
index e4874a1..625adf9 100644
--- a/HepLean/AnomalyCancellation/SMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Basic.lean
@@ -14,7 +14,6 @@ import Mathlib.Logic.Equiv.Fin
 # Anomaly cancellation conditions for n family SM.
 -/
 
-
 universe v u
 open Nat
 open BigOperators
@@ -83,7 +82,6 @@ abbrev E := @toSpecies n 4
 /-- The `N` charges as a map `Fin n → ℚ`. -/
 abbrev N := @toSpecies n 5
 
-
 end SMνCharges
 
 namespace SMνACCs
@@ -111,7 +109,6 @@ def accGrav : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
     -- rw [show Rat.cast a = a from rfl]
     ring
 
-
 lemma accGrav_decomp (S : (SMνCharges n).Charges) :
     accGrav S = 6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i +
       ∑ i, N S i := by
@@ -127,7 +124,6 @@ lemma accGrav_ext {S T : (SMνCharges n).Charges}
   rw [accGrav_decomp, accGrav_decomp]
   repeat erw [hj]
 
-
 /-- The `SU(2)` anomaly equation. -/
 @[simp]
 def accSU2 : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
@@ -344,7 +340,6 @@ lemma cubeTriLin_decomp (S T R : (SMνCharges n).Charges) :
   repeat erw [Finset.sum_add_distrib]
   repeat erw [← Finset.mul_sum]
 
-
 /-- The cubic ACC. -/
 @[simp]
 def accCube : HomogeneousCubic (SMνCharges n).Charges := cubeTriLin.toCubic
diff --git a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
index cd4f051..801ae0d 100644
--- a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
@@ -79,7 +79,6 @@ def speciesEmbed (m n : ℕ) :
     erw [dif_neg hi, dif_neg hi]
     exact Eq.symm (Rat.mul_zero a)
 
-
 /-- The embedding of the `m`-family charges onto the `n`-family charges, with all
 other charges zero.  -/
 def familyEmbedding (m n : ℕ) : (SMνCharges m).Charges →ₗ[ℚ] (SMνCharges n).Charges :=
diff --git a/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean b/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
index 54a9737..4f854b2 100644
--- a/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
@@ -110,7 +110,6 @@ def perm (n : ℕ) : ACCSystemGroupAction (SMNoGrav n) where
     exact Fin.elim0 i
   cubicInvariant := accCube_invariant
 
-
 end SMNoGrav
 
 end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
index e27eda9..df41764 100644
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
@@ -37,7 +37,6 @@ def SM (n : ℕ) : ACCSystem where
 
 namespace SM
 
-
 variable {n : ℕ}
 
 lemma gravSol  (S : (SM n).LinSols) : accGrav S.val = 0 := by
@@ -119,7 +118,6 @@ def perm (n : ℕ) : ACCSystemGroupAction (SM n) where
     exact Fin.elim0 i
   cubicInvariant := accCube_invariant
 
-
 end SM
 
 end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean b/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
index 04d8315..a8201a3 100644
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
@@ -137,7 +137,6 @@ lemma B₀_Bi_cubic {i : Fin 7} (hi : 0 ≠ i) (S : (SM 3).Charges) :
     simp at hi <;>
     simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
-
 lemma B₁_Bi_cubic {i : Fin 7} (hi : 1 ≠ i) (S : (SM 3).Charges) :
     cubeTriLin (B 1) (B i) S = 0 := by
   change cubeTriLin B₁ (B i) S = 0
@@ -246,7 +245,6 @@ lemma B₆_B₆_Bi_cubic {i : Fin 7} :
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
-
 lemma Bi_Bi_Bj_cubic (i j : Fin 7) :
     cubeTriLin (B i) (B i) (B j) = 0 := by
   fin_cases i
@@ -344,6 +342,5 @@ theorem seven_dim_plane_exists : ∃ (B : Fin 7 → (SM 3).Charges),
   exact PlaneSeven.basis_linear_independent
   exact PlaneSeven.B_sum_is_sol
 
-
 end SM
 end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/Permutations.lean b/HepLean/AnomalyCancellation/SMNu/Permutations.lean
index 4306f2a..3a1cb19 100644
--- a/HepLean/AnomalyCancellation/SMNu/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Permutations.lean
@@ -65,7 +65,6 @@ lemma repCharges_toSpecies (f : PermGroup n) (S : (SMνCharges n).Charges) (j :
     toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j := by
   erw [toSMSpecies_toSpecies_inv]
 
-
 lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMνCharges n).Charges) (j : Fin 6) :
     ∑ i, ((fun a => a ^ m) ∘ toSpecies j (repCharges f S)) i =
     ∑ i, ((fun a => a ^ m) ∘ toSpecies j S) i := by
@@ -74,19 +73,16 @@ lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMνCharges n).C
   refine Equiv.Perm.sum_comp _ _ _ ?_
   simp only [PermGroup, Fin.isValue, Pi.inv_apply, ne_eq, coe_univ, Set.subset_univ]
 
-
 lemma accGrav_invariant (f : PermGroup n) (S : (SMνCharges n).Charges)  :
     accGrav (repCharges f S) = accGrav S :=
   accGrav_ext
     (by simpa using toSpecies_sum_invariant 1 f S)
 
-
 lemma accSU2_invariant (f : PermGroup n) (S : (SMνCharges n).Charges)  :
     accSU2 (repCharges f S) = accSU2 S :=
   accSU2_ext
     (by simpa using toSpecies_sum_invariant 1 f S)
 
-
 lemma accSU3_invariant (f : PermGroup n) (S : (SMνCharges n).Charges)  :
     accSU3 (repCharges f S) = accSU3 S :=
   accSU3_ext
@@ -97,7 +93,6 @@ lemma accYY_invariant (f : PermGroup n) (S : (SMνCharges n).Charges)  :
   accYY_ext
     (by simpa using toSpecies_sum_invariant 1 f S)
 
-
 lemma accQuad_invariant (f : PermGroup n) (S : (SMνCharges n).Charges)  :
     accQuad (repCharges f S) = accQuad S :=
   accQuad_ext
@@ -108,6 +103,4 @@ lemma accCube_invariant (f : PermGroup n) (S : (SMνCharges n).Charges)  :
   accCube_ext
     (by simpa using toSpecies_sum_invariant 3 f S)
 
-
-
 end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
index 91a2fa4..6e08870 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
@@ -114,7 +114,6 @@ lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
     add_zero, BL_val, mul_zero]
   ring
 
-
 end BL
 end PlusU1
 end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
index 250a365..5da3f0e 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
@@ -37,7 +37,6 @@ def PlusU1 (n : ℕ) : ACCSystem where
 
 namespace PlusU1
 
-
 variable {n : ℕ}
 
 lemma gravSol  (S : (PlusU1 n).LinSols) : accGrav S.val = 0 := by
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
index be6b935..ac6aaa0 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
@@ -58,7 +58,6 @@ lemma exists_plane_exists_basis {n : ℕ} (hE : ExistsPlane n) :
   | Sum.inl i => exact h3 i
   | Sum.inr i => exact h4 i
 
-
 theorem plane_exists_dim_le_7 {n : ℕ} (hn : ExistsPlane n) : n ≤ 7 := by
   obtain ⟨B, hB⟩ := exists_plane_exists_basis hn
   have h1 := LinearIndependent.fintype_card_le_finrank hB
@@ -67,6 +66,5 @@ theorem plane_exists_dim_le_7 {n : ℕ} (hn : ExistsPlane n) : n ≤ 7 := by
     FiniteDimensional.finrank_fin_fun ℚ] at h1
   exact Nat.le_of_add_le_add_left h1
 
-
 end PlusU1
 end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
index fd84c9b..afb8aa9 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
@@ -68,7 +68,6 @@ lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin (Y n).val S.val = 0
   rw [on_quadBiLin]
   rw [YYsol S]
 
-
 lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
     accQuad (a • S.val + b • (Y n).val) = a ^ 2 * accQuad S.val := by
   erw [BiLinearSymm.toHomogeneousQuad_add, quadSol (b • (Y n)).1]
@@ -144,7 +143,6 @@ lemma add_AF_cube (S : (PlusU1 n).Sols) (a b : ℚ) :
 def addCube (S : (PlusU1 n).Sols) (a b : ℚ) : (PlusU1 n).Sols :=
   quadToAF (addQuad S.1 a b) (add_AF_cube S a b)
 
-
 end Y
 end PlusU1
 end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
index a1d54f8..54c3860 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
@@ -104,7 +104,6 @@ lemma on_accQuad (f : Fin 11 → ℚ) :
   rw [quadBiLin.map_smul₁, Bi_sum_quad, quadCoeff_eq_bilinear]
   ring
 
-
 lemma isSolution_quadCoeff_f_sq_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i))
     (k : Fin 11)  : quadCoeff k * (f k)^2 = 0 := by
   obtain ⟨S, hS⟩ := hS
@@ -231,7 +230,6 @@ lemma isSolution_f_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i,
   exact isSolution_f9 f hS
   exact isSolution_f10 f hS
 
-
 lemma isSolution_only_if_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
     ∑ i, f i • B i = 0 := by
   rw [isSolution_sum_part f hS]
@@ -239,7 +237,6 @@ lemma isSolution_only_if_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (
   rw [isSolution_f9 f hS]
   simp
 
-
 theorem basis_linear_independent : LinearIndependent ℚ B := by
   apply Fintype.linearIndependent_iff.mpr
   intro f h
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
index 912464c..e4965c1 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
@@ -74,7 +74,6 @@ lemma genericToQuad_neq_zero (S : (PlusU1 n).QuadSols) (h : α₁ C S.1 ≠ 0) :
     (α₁ C S.1)⁻¹ • genericToQuad C S.1 = S := by
   rw [genericToQuad_on_quad, smul_smul, inv_mul_cancel h, one_smul]
 
-
 /-- The construction of a `QuadSol` from a `LinSols` in the special case when `α₁ C S = 0` and
   `α₂ S = 0`. -/
 def specialToQuad (S : (PlusU1 n).LinSols) (a b : ℚ) (h1 : α₁ C S = 0)
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
index da6f205..7488e75 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
@@ -78,10 +78,8 @@ lemma special_on_AF (S : (PlusU1 n).Sols)  (h1 : α₁ S.1 = 0) :
   rw [BL.addQuad_zero]
   simp
 
-
 end QuadSolToSol
 
-
 open QuadSolToSol
 /-- A map from `QuadSols × ℚ × ℚ` to `Sols` taking account of the special and generic cases.
 We will show that this map is a surjection. -/
diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/FeynmanDiagrams/Basic.lean
index 33fa443..9c41239 100644
--- a/HepLean/FeynmanDiagrams/Basic.lean
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@@ -22,7 +22,6 @@ import Mathlib.SetTheory.Cardinal.Basic
 Feynman diagrams are a graphical representation of the terms in the perturbation expansion of
 a quantum field theory.
 
-
 -/
 
 open CategoryTheory
@@ -106,7 +105,6 @@ def preimageEdge {𝓔 𝓥 : Type} (v : 𝓔) :
   map {f g} F := Over.homMk ((P.toEdge ⋙ preimageType' v).map F)
     (funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1)
 
-
 /-!
 
 ## Finitness of pre-Feynman rules
@@ -304,7 +302,6 @@ instance diagramEdgePropDecidable
     (fun _ =>  P.preFeynmanRuleDecEq𝓱𝓔) _ _ _)) _ ) _)
     (P.diagramEdgeProp_iff F f).symm
 
-
 end PreFeynmanRule
 
 /-!
@@ -378,7 +375,6 @@ instance CondDecidable [IsFinitePreFeynmanRule P] {𝓔 𝓥 𝓱𝓔 : Type} (
     (@diagramEdgePropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓔𝓞)
     (@diagramVertexPropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓥𝓞)
 
-
 /-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
 def mk' {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel)
     (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥)
@@ -491,7 +487,6 @@ structure Hom (F G : FeynmanDiagram P) where
   /-- The morphism of half-edge objects. -/
   𝓱𝓔To𝓔𝓥 : (edgeVertexFunc 𝓔𝓞.left 𝓥𝓞.left).obj F.𝓱𝓔To𝓔𝓥 ⟶ G.𝓱𝓔To𝓔𝓥
 
-
 namespace Hom
 variable {F G : FeynmanDiagram P}
 variable (f : Hom F G)
@@ -508,12 +503,10 @@ def 𝓥 : F.𝓥 → G.𝓥 := f.𝓥𝓞.left
 @[simp]
 def 𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔 := f.𝓱𝓔To𝓔𝓥.left
 
-
 /-- The morphism `F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞` induced by a homomorphism of Feynman diagrams. -/
 @[simp]
 def 𝓱𝓔𝓞 : F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞 := P.toHalfEdge.map f.𝓱𝓔To𝓔𝓥
 
-
 /-- The identity morphism for a Feynman diagram. -/
 def id (F : FeynmanDiagram P) : Hom F F where
   𝓔𝓞 := 𝟙 F.𝓔𝓞
@@ -579,7 +572,6 @@ instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFin
     (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Decidable (Cond 𝓔 𝓥 𝓱𝓔) :=
   And.decidable
 
-
 /-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
 @[simps! 𝓔𝓞_left 𝓥𝓞_left 𝓱𝓔To𝓔𝓥_left]
 def mk' {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔)
@@ -667,7 +659,6 @@ We show that the symmetry factor for a finite Feynman diagram is finite.
 /-- The type of isomorphisms of a Feynman diagram. -/
 def SymmetryType : Type := F ≅ F
 
-
 /-- An equivalence between `SymmetryType` and permutation of edges, vertices and half-edges
   satisfying `Hom.Cond`. -/
 def symmetryTypeEquiv :
@@ -728,7 +719,6 @@ instance [IsFiniteDiagram F] : DecidableRel F.AdjRelation := fun _ _ =>
     @And.decidable _ _ (instDecidableEq𝓥OfIsFiniteDiagram _ _)
     (instDecidableEq𝓥OfIsFiniteDiagram _ _)) _ ) _
 
-
 /-- From a Feynman diagram the simple graph showing those vertices which are connected. -/
 def toSimpleGraph : SimpleGraph F.𝓥 where
   Adj := AdjRelation F
diff --git a/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean b/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
index 6b77219..6c081c2 100644
--- a/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
+++ b/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
@@ -7,11 +7,8 @@ import HepLean.FeynmanDiagrams.Basic
 /-!
 # Feynman diagrams in a complex scalar field theory
 
-
-
 -/
 
-
 namespace PhiFour
 open CategoryTheory
 open FeynmanDiagram
@@ -65,7 +62,4 @@ instance : IsFinitePreFeynmanRule complexScalarFeynmanRules where
     match v with
     | 0 => instDecidableEqFin _
 
-
-
-
 end PhiFour
diff --git a/HepLean/FeynmanDiagrams/Instances/Phi4.lean b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
index 06413ec..0c780ad 100644
--- a/HepLean/FeynmanDiagrams/Instances/Phi4.lean
+++ b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
@@ -10,10 +10,8 @@ import HepLean.FeynmanDiagrams.Basic
 The aim of this file is to start building up the theory of Feynman diagrams in the context of
 Phi^4 theory.
 
-
 -/
 
-
 namespace PhiFour
 open CategoryTheory
 open FeynmanDiagram
@@ -45,7 +43,6 @@ instance (a : ℕ) : OfNat phi4PreFeynmanRules.HalfEdgeLabel a where
 instance (a : ℕ) : OfNat phi4PreFeynmanRules.VertexLabel a where
   ofNat := (a : Fin _)
 
-
 instance : IsFinitePreFeynmanRule phi4PreFeynmanRules where
   edgeLabelDecidable :=  instDecidableEqFin _
   vertexLabelDecidable := instDecidableEqFin _
@@ -92,5 +89,4 @@ lemma figureEight_symmetryFactor : symmetryFactor figureEight = 8 := by decide
 
 end Example
 
-
 end PhiFour
diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/FeynmanDiagrams/Momentum.lean
index 65cb033..bf57569 100644
--- a/HepLean/FeynmanDiagrams/Momentum.lean
+++ b/HepLean/FeynmanDiagrams/Momentum.lean
@@ -26,7 +26,6 @@ vector space.
 This section is non-computable as we depend on the norm on `F.HalfEdgeMomenta`.
 -/
 
-
 namespace FeynmanDiagram
 
 open CategoryTheory
@@ -78,7 +77,6 @@ def euclidInner : F.HalfEdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta →ₗ[ℝ] 
     simp only [euclidInnerAux_symm, LinearMapClass.map_smul, smul_eq_mul, RingHom.id_apply,
       LinearMap.smul_apply]
 
-
 /-- The type which assocaites to each ege a `1`-dimensional vector space.
  Corresponding to that spanned by its total outflowing momentum.  -/
 def EdgeMomenta : Type := F.𝓔 → ℝ
@@ -87,7 +85,6 @@ instance : AddCommGroup F.EdgeMomenta := Pi.addCommGroup
 
 instance : Module ℝ F.EdgeMomenta := Pi.module _ _ _
 
-
 /-- The type which assocaites to each ege a `1`-dimensional vector space.
  Corresponding to that spanned by its total inflowing momentum.  -/
 def VertexMomenta : Type := F.𝓥 → ℝ
@@ -119,7 +116,6 @@ instance : AddCommGroup F.EdgeVertexMomenta := DirectSum.instAddCommGroup _
 
 instance : Module ℝ F.EdgeVertexMomenta := DirectSum.instModule
 
-
 /-!
 
 ## Linear maps between the vector spaces.
@@ -199,7 +195,6 @@ for specific Feynman diagrams.
 
 - Complete this section.
 
-
 -/
 
 /-!
@@ -210,7 +205,6 @@ for specific Feynman diagrams.
 
 - Complete this section.
 
-
 -/
 
 end FeynmanDiagram
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
index 7e6922c..ddcf854 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
@@ -17,12 +17,10 @@ related by phase shifts.
 The notation `[V]ud` etc can be used for the elements of a CKM matrix, and
 `[V]ud|us` etc for the ratios of elements.
 
-
 -/
 
 open Matrix Complex
 
-
 noncomputable section
 
 /-- Given three real numbers `a b c` the complex matrix with `exp (I * a)` etc on the
@@ -107,7 +105,6 @@ lemma phaseShiftRelation_trans {U V W : unitaryGroup (Fin 3) ℂ} :
   rw [phaseShiftMatrix_mul]
   rw [add_comm k e, add_comm l f, add_comm m g]
 
-
 lemma phaseShiftRelation_equiv : Equivalence PhaseShiftRelation where
   refl := phaseShiftRelation_refl
   symm := phaseShiftRelation_symm
@@ -270,7 +267,6 @@ lemma tb (V : CKMMatrix) (a b c d e f : ℝ) :
 
 end phaseShiftApply
 
-
 /-- The aboslute value of the `(i,j)`th element of `V`. -/
 @[simp]
 def VAbs' (V : unitaryGroup (Fin 3) ℂ) (i j : Fin 3) : ℝ := Complex.abs (V i j)
@@ -341,11 +337,9 @@ abbrev VtsAbs := VAbs 2 1
 @[simp]
 abbrev VtbAbs := VAbs 2 2
 
-
 namespace CKMMatrix
 open ComplexConjugate
 
-
 section ratios
 
 /-- The ratio of the `ub` and `ud` elements of a CKM matrix. -/
@@ -394,7 +388,6 @@ lemma Rcscb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0): [V]cs = Rcscb V * [V]cb :=
 
 end ratios
 
-
 end CKMMatrix
 
 end
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
index 79a7e70..9b9b024 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
@@ -15,17 +15,14 @@ this equivalence.
 
 Of note, this file defines the complex jarlskog invariant.
 
-
 -/
 open Matrix Complex
 open ComplexConjugate
 open CKMMatrix
 
-
 noncomputable section
 namespace Invariant
 
-
 /-- The complex jarlskog invariant for a CKM matrix. -/
 @[simps!]
 def jarlskogℂCKM (V : CKMMatrix) : ℂ :=
@@ -62,6 +59,5 @@ standard parameterization. -/
 def mulExpδ₁₃ (V : Quotient CKMMatrixSetoid) : ℂ :=
   jarlskogℂ V + VusVubVcdSq V
 
-
 end Invariant
 end
diff --git a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
index 974f81d..29c9bbf 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
@@ -19,11 +19,9 @@ In this file we define two sets of conditions on the CKM matrices
 and `ubOnePhaseCond` which we show can be satisfied by any CKM matrix up to equivalence as long as
 the ub element as absolute value 1.
 
-
 -/
 open Matrix Complex
 
-
 noncomputable section
 namespace CKMMatrix
 open ComplexConjugate
@@ -260,7 +258,6 @@ lemma fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) :
   apply shift_cross_product_phase_zero _ _ _ _ _ _ hτ.symm
   ring
 
-
 lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0))
     (hV : FstRowThdColRealCond V)  :
     ∃ (U : CKMMatrix), V ≈ U ∧ ubOnePhaseCond U:= by
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
index 2dad76b..bbf9dff 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
@@ -16,7 +16,6 @@ matrix.
 
 open Matrix Complex
 
-
 noncomputable section
 
 namespace CKMMatrix
@@ -121,9 +120,6 @@ lemma VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero {V : Quotient CKMMatrixSetoid}
   rw [← ud_us_neq_zero_iff_ub_neq_one V] at hV
   simpa [← Complex.sq_abs] using (normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hV)
 
-
-
-
 lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℂ  {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) :
     (normSq [V]ud : ℂ) + normSq [V]us ≠ 0 := by
   have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hb
@@ -131,7 +127,6 @@ lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℂ  {V : CKMMatrix} (hb : [V]ud ≠ 0
   rw [← ofReal_inj] at h1
   simp_all
 
-
 lemma Vabs_sq_add_neq_zero {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) :
     ((VudAbs ⟦V⟧ : ℂ) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧)) ≠ 0 := by
   have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℂ hb
@@ -230,7 +225,6 @@ lemma conj_Vtb_mul_Vus {V : CKMMatrix} {τ : ℝ}
   simp only [Fin.isValue, neg_mul]
   ring
 
-
 lemma cs_of_ud_us_ub_cb_tb {V : CKMMatrix}  (h : [V]ud ≠ 0 ∨ [V]us ≠ 0)
     {τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) :
     [V]cs = (- conj [V]ub * [V]us  * [V]cb +
@@ -249,10 +243,8 @@ lemma cd_of_ud_us_ub_cb_tb {V : CKMMatrix}  (h : [V]ud ≠ 0 ∨ [V]us ≠ 0)
   field_simp
   ring
 
-
 end rows
 
-
 section individual
 
 lemma VAbs_ge_zero  (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : 0 ≤ VAbs i j V := by
@@ -270,12 +262,10 @@ lemma VAbs_leq_one (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : VAbs i j V ≤
   change VAbs i 2 V ≤ 1
   nlinarith
 
-
 end individual
 
 section columns
 
-
 lemma VAbs_sum_sq_col_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
     (VAbs 0 i V) ^ 2 + (VAbs 1 i V) ^ 2 + (VAbs 2 i V) ^ 2 = 1 := by
   obtain ⟨V, hV⟩ := Quot.exists_rep V
@@ -312,7 +302,6 @@ lemma cb_eq_zero_of_ud_us_zero {V : CKMMatrix} (h :  [V]ud = 0 ∧ [V]us = 0) :
   simp at h1
   exact h1.1
 
-
 lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) :
     VcsAbs ⟦V⟧ = √(1 - VcdAbs ⟦V⟧ ^ 2) := by
   have h1 := snd_row_normalized_abs V
@@ -336,8 +325,6 @@ lemma VcbAbs_sq_add_VtbAbs_sq (V : Quotient CKMMatrixSetoid) :
     VcbAbs V ^ 2 + VtbAbs V ^ 2 = 1 - VubAbs V ^2 := by
   linear_combination (VAbs_sum_sq_col_eq_one V 2)
 
-
-
 lemma cb_tb_neq_zero_iff_ub_neq_one (V : CKMMatrix) :
     [V]cb ≠ 0 ∨ [V]tb ≠ 0 ↔ abs [V]ub ≠ 1 := by
   have h2 := V.thd_col_normalized_abs
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
index e8d7f5b..39e7c15 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
@@ -14,7 +14,6 @@ proves some properties between them.
 
 The first row can be extracted as `[V]u` for a CKM matrix `V`.
 
-
 -/
 
 open Matrix Complex
@@ -24,7 +23,6 @@ noncomputable section
 
 namespace CKMMatrix
 
-
 /-- The `u`th row of the CKM matrix. -/
 def uRow (V : CKMMatrix) : Fin 3 → ℂ := ![[V]ud, [V]us, [V]ub]
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
index 42ab86b..3beb917 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
@@ -16,7 +16,6 @@ four real numbers `θ₁₂`, `θ₁₃`, `θ₂₃` and `δ₁₃`.
 We will show that every CKM matrix can be written within this standard parameterization
 in the file `FlavorPhysics.CKMMatrix.StandardParameters`.
 
-
 -/
 open Matrix Complex
 open ComplexConjugate
@@ -194,7 +193,5 @@ lemma mulExpδ₁₃_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤
   have h1 : cexp (I * δ₁₃) ≠ 0 := exp_ne_zero _
   field_simp
 
-
-
 end standParam
 end
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
index 60ce478..ef7c1d3 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
@@ -18,7 +18,6 @@ These, when used in the standard parameterization return `V` up to equivalence.
 This leads to the theorem `standParam.exists_for_CKMatrix` which says that up to equivalence every
 CKM matrix can be written using the standard parameterization.
 
-
 -/
 open Matrix Complex
 open ComplexConjugate
@@ -333,7 +332,6 @@ lemma Vs_zero_iff_cos_sin_zero (V : CKMMatrix) :
 
 end VAbs
 
-
 namespace standParam
 open Invariant
 
@@ -409,7 +407,6 @@ lemma on_param_cos_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
   rfl
   rfl
 
-
 lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₂ ⟦V⟧) = 0) :
     standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
   use 0, δ₁₃, δ₁₃, -δ₁₃, 0, - δ₁₃
@@ -434,7 +431,6 @@ lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
   ring_nf
   field_simp
 
-
 lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₂₃ ⟦V⟧) = 0) :
     standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
   use 0, δ₁₃, 0, 0, 0, - δ₁₃
@@ -451,7 +447,6 @@ lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
   ring
   field_simp
 
-
 lemma on_param_sin_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₃ ⟦V⟧) = 0) :
     standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
   use 0, 0, 0, 0, 0, 0
@@ -488,8 +483,6 @@ lemma on_param_sin_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
   ring_nf
   field_simp
 
-
-
 lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₂₃ ⟦V⟧) = 0) :
     standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
   use 0, 0, δ₁₃, 0, 0, - δ₁₃
@@ -506,9 +499,6 @@ lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
   ring
   field_simp
 
-
-
-
 lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0)
     (hV : FstRowThdColRealCond V) : V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (- arg [V]ub) := by
   have hb' : VubAbs ⟦V⟧ ≠ 1 := by
@@ -565,7 +555,6 @@ lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 
   rw [VcbAbs_eq_S₂₃_mul_C₁₃ ⟦V⟧, S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, C₁₃]
   simp
 
-
 lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) :
     V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
   have h1 : VubAbs ⟦V⟧ = 1 := by
@@ -610,7 +599,6 @@ lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) :
   rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.2.2.1]
   simp
 
-
 theorem exists_δ₁₃ (V : CKMMatrix) :
     ∃ (δ₃ : ℝ), V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₃ := by
   obtain ⟨U, hU⟩ := fstRowThdColRealCond_holds_up_to_equiv V
@@ -670,7 +658,6 @@ theorem eq_standardParameterization_δ₃ (V : CKMMatrix) :
   exact on_param_sin_θ₁₃_eq_zero δ₁₃' h
   exact on_param_sin_θ₂₃_eq_zero δ₁₃' h
 
-
 theorem exists_for_CKMatrix (V : CKMMatrix) :
     ∃ (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ), V ≈ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by
   use θ₁₂ ⟦V⟧, θ₁₃ ⟦V⟧, θ₂₃ ⟦V⟧, δ₁₃ ⟦V⟧
@@ -678,9 +665,6 @@ theorem exists_for_CKMatrix (V : CKMMatrix) :
 
 end standParam
 
-
 open CKMMatrix
 
-
-
 end
diff --git a/HepLean/Mathematics/LinearMaps.lean b/HepLean/Mathematics/LinearMaps.lean
index 5fda3b0..d56b6e7 100644
--- a/HepLean/Mathematics/LinearMaps.lean
+++ b/HepLean/Mathematics/LinearMaps.lean
@@ -40,7 +40,6 @@ lemma map_smul (f : HomogeneousQuadratic V) (a : ℚ) (S : V) : f (a • S) = a
 
 end HomogeneousQuadratic
 
-
 /-- The structure of a symmetric bilinear function. -/
 structure BiLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] extends V →ₗ[ℚ] V →ₗ[ℚ] ℚ where
   swap' : ∀ S T, toFun S T = toFun T S
@@ -126,7 +125,6 @@ lemma map_sum₂ {n : ℕ} (f : BiLinearSymm V) (S : Fin n → V) (T : V) :
   intro i
   rw [swap]
 
-
 /-- The homogenous quadratic equation obtainable from a bilinear function. -/
 @[simps!]
 def toHomogeneousQuad {V : Type} [AddCommMonoid V] [Module ℚ V]
@@ -146,7 +144,6 @@ lemma toHomogeneousQuad_add {V : Type} [AddCommMonoid V] [Module ℚ V]
   rw [τ.map_add₁, τ.map_add₁, τ.swap T S]
   ring
 
-
 end BiLinearSymm
 
 /-- The structure of a homogeneous cubic equation. -/
@@ -222,7 +219,6 @@ def mk₃ (f : V × V × V→ ℚ) (map_smul : ∀ a S T L, f (a • S, T, L) =
   swap₁' := swap₁
   swap₂' := swap₂
 
-
 lemma swap₁ (f : TriLinearSymm V) (S T L : V) : f S T L = f T S L :=
   f.swap₁' S T L
 
@@ -300,7 +296,6 @@ lemma map_sum₁₂₃ {n1 n2 n3 : ℕ} (f : TriLinearSymm V) (S : Fin n1 → V)
   intro i
   rw [map_sum₃]
 
-
 /-- The homogenous cubic equation obtainable from a symmetric trilinear function. -/
 @[simps!]
 def toCubic {charges : Type} [AddCommMonoid charges] [Module ℚ charges]
diff --git a/HepLean/Mathematics/SO3/Basic.lean b/HepLean/Mathematics/SO3/Basic.lean
index ff34705..e31b657 100644
--- a/HepLean/Mathematics/SO3/Basic.lean
+++ b/HepLean/Mathematics/SO3/Basic.lean
@@ -11,7 +11,6 @@ import Mathlib.Analysis.InnerProductSpace.PiL2
 /-!
 # The group SO(3)
 
-
 -/
 
 namespace GroupTheory
@@ -107,7 +106,6 @@ lemma toProd_continuous : Continuous toProd := by
   refine Continuous.matrix_transpose ?_
   exact continuous_iff_le_induced.mpr fun U a => a
 
-
 /-- The embedding of `SO(3)` into the monoid of matrices times the opposite of
   the monoid of matrices. -/
 lemma toProd_embedding : Embedding toProd where
@@ -223,10 +221,7 @@ lemma exists_basis_preserved (A : SO(3)) :
   use b
   rw [hb, hv.2]
 
-
-
 end action
 end SO3
 
-
 end GroupTheory
diff --git a/HepLean/SpaceTime/Basic.lean b/HepLean/SpaceTime/Basic.lean
index fae801a..9e78437 100644
--- a/HepLean/SpaceTime/Basic.lean
+++ b/HepLean/SpaceTime/Basic.lean
@@ -29,7 +29,6 @@ instance euclideanNormedAddCommGroup : NormedAddCommGroup SpaceTime := Pi.normed
 
 instance euclideanNormedSpace : NormedSpace ℝ SpaceTime := Pi.normedSpace
 
-
 namespace SpaceTime
 
 open Manifold
diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
index 8f14a5d..c585a52 100644
--- a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
+++ b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
@@ -17,7 +17,6 @@ We define
 
 -/
 
-
 namespace SpaceTime
 open Matrix
 open TensorProduct
@@ -34,7 +33,6 @@ lemma transpose_eta (A : lorentzAlgebra) :  A.1ᵀ * η  = - η * A.1  := by
   erw [mem_skewAdjointMatricesLieSubalgebra] at h1
   simpa [LieAlgebra.Orthogonal.so', IsSkewAdjoint, IsAdjointPair] using h1
 
-
 lemma mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ}
     (h :  Aᵀ * η  = - η * A) : A ∈ lorentzAlgebra := by
   erw [mem_skewAdjointMatricesLieSubalgebra]
@@ -58,7 +56,6 @@ lemma mem_iff'  (A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) :
     rw [minkowskiMatrix.sq]
     all_goals noncomm_ring
 
-
 lemma diag_comp (Λ : lorentzAlgebra) (μ : Fin 1 ⊕ Fin 3) : Λ.1 μ μ = 0 := by
   have h := congrArg (fun M ↦ M μ μ) $ mem_iff.mp Λ.2
   simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal,
@@ -67,22 +64,18 @@ lemma diag_comp (Λ : lorentzAlgebra) (μ : Fin 1 ⊕ Fin 3) : Λ.1 μ μ = 0 :=
   simpa using h
   simpa using h
 
-
-
 lemma time_comps (Λ : lorentzAlgebra) (i : Fin 3) :
     Λ.1 (Sum.inr i) (Sum.inl 0) = Λ.1 (Sum.inl 0) (Sum.inr i) := by
   simpa only [Fin.isValue, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal,
     transpose_apply, Sum.elim_inr, mul_neg, mul_one, diagonal_neg, diagonal_mul, Sum.elim_inl,
     neg_mul, one_mul, neg_inj] using congrArg (fun M ↦ M (Sum.inl 0) (Sum.inr i)) $ mem_iff.mp Λ.2
 
-
 lemma space_comps (Λ : lorentzAlgebra) (i j : Fin 3) :
     Λ.1 (Sum.inr i) (Sum.inr j) = - Λ.1 (Sum.inr j) (Sum.inr i) := by
   simpa only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_neg, diagonal_mul,
     Sum.elim_inr, neg_neg, one_mul, mul_diagonal, transpose_apply, mul_neg, mul_one] using
     (congrArg (fun M ↦ M (Sum.inr i) (Sum.inr j)) $ mem_iff.mp Λ.2).symm
 
-
 end lorentzAlgebra
 
 @[simps!]
@@ -104,5 +97,4 @@ instance spaceTimeAsLieModule : LieModule ℝ lorentzAlgebra (LorentzVector 3) w
     simp [Bracket.bracket]
     rw [mulVec_smul]
 
-
 end SpaceTime
diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean
index 5c737b5..61cb6c0 100644
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@@ -44,7 +44,6 @@ def LorentzGroup (d : ℕ) : Set (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ
     {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ |
      ∀ (x y : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ y⟫ₘ = ⟪x, y⟫ₘ}
 
-
 namespace LorentzGroup
 /-- Notation for the Lorentz group. -/
 scoped[LorentzGroup] notation (name := lorentzGroup_notation) "𝓛" => LorentzGroup
diff --git a/HepLean/SpaceTime/LorentzGroup/Boosts.lean b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
index 38e46e6..1618fb0 100644
--- a/HepLean/SpaceTime/LorentzGroup/Boosts.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
@@ -140,7 +140,6 @@ lemma toMatrix_continuous (u : FuturePointing d) : Continuous (toMatrix u) := by
   exact FuturePointing.metric_continuous _
   exact fun x => FuturePointing.one_add_metric_non_zero u x
 
-
 lemma toMatrix_in_lorentzGroup (u v : FuturePointing d) : (toMatrix u v) ∈ LorentzGroup d:= by
   intro x y
   rw [toMatrix_mulVec, toMatrix_mulVec, genBoost, genBoostAux₁, genBoostAux₂]
@@ -161,7 +160,6 @@ lemma toLorentz_continuous (u : FuturePointing d) : Continuous (toLorentz u) :=
   refine Continuous.subtype_mk ?_ (fun x => toMatrix_in_lorentzGroup u x)
   exact toMatrix_continuous u
 
-
 lemma toLorentz_joined_to_1 (u v : FuturePointing d) : Joined 1 (toLorentz u v) := by
   obtain ⟨f, _⟩ := FuturePointing.isPathConnected.joinedIn u trivial v trivial
   use ContinuousMap.comp ⟨toLorentz u, toLorentz_continuous u⟩ f
@@ -180,8 +178,6 @@ lemma isProper (u v : FuturePointing d) : IsProper (toLorentz u v) :=
 
 end genBoost
 
-
 end LorentzGroup
 
-
 end
diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
index ea7c655..6ef2e6b 100644
--- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
@@ -17,10 +17,8 @@ matrices.
 
 -/
 
-
 noncomputable section
 
-
 open Matrix
 open Complex
 open ComplexConjugate
@@ -66,7 +64,6 @@ lemma not_orthochronous_iff_le_zero :
   rw [IsOrthochronous_iff_ge_one]
   linarith
 
-
 /-- The continuous map taking a Lorentz transformation to its `0 0` element. -/
 def timeCompCont : C(LorentzGroup d, ℝ) := ⟨fun Λ => timeComp Λ  ,
    Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) (Sum.inl 0) (Sum.inl 0)⟩
diff --git a/HepLean/SpaceTime/LorentzGroup/Proper.lean b/HepLean/SpaceTime/LorentzGroup/Proper.lean
index 2457446..e7bc25d 100644
--- a/HepLean/SpaceTime/LorentzGroup/Proper.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Proper.lean
@@ -11,10 +11,8 @@ We define the give a series of lemmas related to the determinant of the lorentz
 
 -/
 
-
 noncomputable section
 
-
 open Matrix
 open Complex
 open ComplexConjugate
@@ -31,7 +29,6 @@ lemma det_eq_one_or_neg_one (Λ : 𝓛 d) : Λ.1.det = 1 ∨ Λ.1.det = -1 := by
   simp [det_mul, det_dual] at h1
   exact mul_self_eq_one_iff.mp h1
 
-
 local notation  "ℤ₂" => Multiplicative (ZMod 2)
 
 instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin
@@ -76,7 +73,6 @@ lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup d) :
   · intro h
     simp [detContinuous, h]
 
-
 /-- The representation taking a lorentz matrix to its determinant. -/
 @[simps!]
 def detRep : 𝓛 d →* ℤ₂ where
diff --git a/HepLean/SpaceTime/LorentzGroup/Rotations.lean b/HepLean/SpaceTime/LorentzGroup/Rotations.lean
index 5172b3f..cdc9558 100644
--- a/HepLean/SpaceTime/LorentzGroup/Rotations.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Rotations.lean
@@ -54,8 +54,6 @@ def SO3ToLorentz : SO(3) →* LorentzGroup 3 where
     apply Subtype.eq
     simp [Matrix.fromBlocks_multiply]
 
-
 end LorentzGroup
 
-
 end
diff --git a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
index 6fbdcb5..b8399a8 100644
--- a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
+++ b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
@@ -52,7 +52,6 @@ noncomputable def fromSelfAdjointMatrix' (x : selfAdjoint (Matrix (Fin 2) (Fin 2
   | Sum.inr 1 => (x.1 1 0).im
   | Sum.inr 2 => 1/2 * (x.1 0 0 - x.1 1 1).re
 
-
 /-- The linear equivalence between the vector-space `spaceTime` and self-adjoint
   2×2-complex matrices. -/
 noncomputable def toSelfAdjointMatrix :
diff --git a/HepLean/SpaceTime/LorentzVector/Basic.lean b/HepLean/SpaceTime/LorentzVector/Basic.lean
index c3d2a5a..060e348 100644
--- a/HepLean/SpaceTime/LorentzVector/Basic.lean
+++ b/HepLean/SpaceTime/LorentzVector/Basic.lean
@@ -77,7 +77,6 @@ lemma timeVec_space : (@timeVec d).space = 0 := by
 lemma timeVec_time: (@timeVec d).time = 1 := by
   simp only [time, Fin.isValue, stdBasis_apply, ↓reduceIte]
 
-
 /-!
 
 # Reflection of space
diff --git a/HepLean/SpaceTime/LorentzVector/NormOne.lean b/HepLean/SpaceTime/LorentzVector/NormOne.lean
index 2866976..905e448 100644
--- a/HepLean/SpaceTime/LorentzVector/NormOne.lean
+++ b/HepLean/SpaceTime/LorentzVector/NormOne.lean
@@ -63,7 +63,6 @@ lemma time_nonpos_iff : v.1.time ≤ 0 ↔ v.1.time ≤ - 1 := by
   · intro h
     linarith
 
-
 lemma time_nonneg_iff : 0 ≤ v.1.time ↔ 1 ≤ v.1.time := by
   apply Iff.intro
   · intro h
@@ -167,14 +166,12 @@ lemma metric_reflect_mem_mem (h : v ∈ FuturePointing d) (hw : w ∈ FuturePoin
   apply le_trans (neg_le_abs _ : _ ≤ |⟪(v.1).space, (w.1).space⟫_ℝ|) ?_
   exact abs_real_inner_le_norm (v.1).space (w.1).space
 
-
 lemma metric_reflect_not_mem_not_mem (h : v ∉ FuturePointing d) (hw : w ∉ FuturePointing d) :
     0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ  := by
   have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) ((not_mem_iff_neg w).mp hw)
   apply le_of_le_of_eq h1 ?_
   simp [neg]
 
-
 lemma metric_reflect_mem_not_mem (h : v ∈ FuturePointing d) (hw : w ∉ FuturePointing d) :
     ⟪v.1, w.1.spaceReflection⟫ₘ ≤ 0 := by
   rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg]
@@ -209,7 +206,6 @@ noncomputable def timeVecNormOneFuture : FuturePointing d := ⟨⟨timeVec, by
   rw [NormOneLorentzVector.mem_iff, on_timeVec]⟩, by
   rw [mem_iff, timeVec_time]; exact Real.zero_lt_one⟩
 
-
 /-- A continuous path from `timeVecNormOneFuture` to any other. -/
 noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFuture u where
   toFun t := ⟨
@@ -266,9 +262,6 @@ noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFutur
       simp only [Set.Icc.coe_one, one_pow, space, one_mul, Fin.isValue]
       exact rfl
 
-
-
-
 lemma isPathConnected : IsPathConnected (@Set.univ (FuturePointing d)) := by
   use timeVecNormOneFuture
   apply And.intro trivial  ?_
@@ -276,7 +269,6 @@ lemma isPathConnected : IsPathConnected (@Set.univ (FuturePointing d)) := by
   use pathFromTime y
   exact fun _ => a
 
-
 lemma metric_continuous (u : LorentzVector d) :
     Continuous (fun (a : FuturePointing d) => ⟪u, a.1.1⟫ₘ) := by
   simp only [minkowskiMetric.eq_time_minus_inner_prod]
@@ -289,8 +281,6 @@ lemma metric_continuous (u : LorentzVector d) :
      (Continuous.comp' (Pi.continuous_precomp Sum.inr) (Continuous.comp'
       continuous_subtype_val continuous_subtype_val))
 
-
 end FuturePointing
 
-
 end NormOneLorentzVector
diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean
index 884945e..4160fed 100644
--- a/HepLean/SpaceTime/MinkowskiMetric.lean
+++ b/HepLean/SpaceTime/MinkowskiMetric.lean
@@ -16,7 +16,6 @@ of Lorentz vectors in d dimensions.
 
 -/
 
-
 open Matrix
 
 /-!
@@ -55,7 +54,6 @@ lemma sq : @minkowskiMatrix d * minkowskiMatrix  = 1 := by
 lemma eq_transpose : minkowskiMatrixᵀ = @minkowskiMatrix d := by
   simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_transpose]
 
-
 @[simp]
 lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by
   simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
@@ -71,10 +69,8 @@ lemma as_block :  @minkowskiMatrix d =  (
   rw [← diagonal_neg]
   rfl
 
-
 end minkowskiMatrix
 
-
 /-!
 
 # The definition of the Minkowski Metric
@@ -133,7 +129,6 @@ lemma as_sum :
     Function.comp_apply, minkowskiMatrix]
   ring
 
-
 /-- The Minkowski metric expressed as a sum for a single vector. -/
 lemma as_sum_self : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 := by
   rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum]
@@ -167,7 +162,6 @@ lemma right_spaceReflection : ⟪v, w.spaceReflection⟫ₘ = v.time * w.time +
   simp only [time, Fin.isValue, space, inner_neg_right, PiLp.inner_apply, Function.comp_apply,
     RCLike.inner_apply, conj_trivial, sub_neg_eq_add]
 
-
 lemma self_spaceReflection_eq_zero_iff : ⟪v, v.spaceReflection⟫ₘ = 0 ↔ v = 0 := by
   refine Iff.intro (fun h => ?_) (fun h => ?_)
   · rw [right_spaceReflection] at h
@@ -195,7 +189,6 @@ lemma nondegenerate : (∀ w, ⟪w, v⟫ₘ = 0) ↔ v = 0 := by
   · exact (self_spaceReflection_eq_zero_iff _ ).mp ((symm _ _).trans $ h v.spaceReflection)
   · simp [h]
 
-
 /-!
 
 # Inequalitites involving the Minkowski metric
@@ -215,7 +208,6 @@ lemma ge_sub_norm : v.time * w.time - ‖v.space‖ * ‖w.space‖ ≤ ⟪v, w
   rw [sub_le_sub_iff_left]
   exact norm_inner_le_norm v.space w.space
 
-
 /-!
 
 # The Minkowski metric and matrices
@@ -303,7 +295,6 @@ lemma matrix_eq_id_iff : Λ = 1 ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫
   rw [matrix_eq_iff_eq_forall]
   simp
 
-
 /-!
 
 # The Minkowski metric and the standard basis
diff --git a/HepLean/SpaceTime/SL2C/Basic.lean b/HepLean/SpaceTime/SL2C/Basic.lean
index d24152c..e58d09b 100644
--- a/HepLean/SpaceTime/SL2C/Basic.lean
+++ b/HepLean/SpaceTime/SL2C/Basic.lean
@@ -130,8 +130,6 @@ Complete this section.
 
 -/
 
-
-
 end
 end SL2C
 
diff --git a/HepLean/StandardModel/HiggsBoson/Basic.lean b/HepLean/StandardModel/HiggsBoson/Basic.lean
index 62a19ec..70f15e4 100644
--- a/HepLean/StandardModel/HiggsBoson/Basic.lean
+++ b/HepLean/StandardModel/HiggsBoson/Basic.lean
@@ -98,7 +98,6 @@ lemma apply_im_smooth (φ : HiggsField) (i : Fin 2):
 /-- Given two `higgsField`, the map `spaceTime → ℂ` obtained by taking their inner product. -/
 def innerProd (φ1 φ2 : HiggsField) : SpaceTime → ℂ := fun x => ⟪φ1 x, φ2 x⟫_ℂ
 
-
 /-- Given a `higgsField`, the map `spaceTime → ℝ` obtained by taking the square norm of the
  higgs vector.  -/
 @[simp]
@@ -154,7 +153,6 @@ lemma potential_apply (φ : HiggsField) (μSq lambda : ℝ) (x : SpaceTime) :
   simp [HiggsVec.potential, toHiggsVec_norm]
   ring
 
-
 /-- A higgs field is constant if it is equal for all `x` `y` in `spaceTime`. -/
 def IsConst (Φ : HiggsField) : Prop := ∀ x y, Φ x = Φ y
 
diff --git a/HepLean/StandardModel/HiggsBoson/TargetSpace.lean b/HepLean/StandardModel/HiggsBoson/TargetSpace.lean
index 350d2b5..b494d1c 100644
--- a/HepLean/StandardModel/HiggsBoson/TargetSpace.lean
+++ b/HepLean/StandardModel/HiggsBoson/TargetSpace.lean
@@ -39,7 +39,6 @@ open ComplexConjugate
 /-- The complex vector space in which the Higgs field takes values. -/
 abbrev HiggsVec := EuclideanSpace ℂ (Fin 2)
 
-
 /-- The continuous linear map from the vector space `higgsVec` to `(Fin 2 → ℂ)` achieved by
 casting vectors. -/
 def higgsVecToFin2ℂ : HiggsVec →L[ℝ] (Fin 2 → ℂ) where
@@ -144,7 +143,6 @@ lemma potential_snd_term_nonneg (φ : HiggsVec) :
   simp_all only [ge_iff_le, norm_nonneg, pow_nonneg, and_true]
   exact le_of_lt hLam
 
-
 lemma zero_le_potential_discrim  (φ : HiggsVec) :
     0 ≤ discrim (λ) (- μSq ) (- potential μSq (λ) φ) := by
   have h1 := potential_as_quad μSq (λ) φ
diff --git a/HepLean/StandardModel/Representations.lean b/HepLean/StandardModel/Representations.lean
index 4500ee5..4fe843c 100644
--- a/HepLean/StandardModel/Representations.lean
+++ b/HepLean/StandardModel/Representations.lean
@@ -53,5 +53,4 @@ lemma repU1_fundamentalSU2_commute (u1 : unitary ℂ) (g : specialUnitaryGroup (
   apply Subtype.ext
   simp
 
-
 end StandardModel