diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
index 07f3e12..d5a99b0 100644
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
@@ -175,7 +175,7 @@ lemma normalOrder_swap_create_annihlate_ofCrAnList (φc φa : 𝓕.CrAnStates)
   rfl
 
 lemma normalOrder_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
-    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)  (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
+    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
     (a b : 𝓕.CrAnAlgebra) :
     normalOrder (a * ofCrAnState φc * ofCrAnState φa * b) =
     𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa) •
@@ -258,7 +258,6 @@ Using the results from above.
 
 -/
 
-
 lemma normalOrder_swap_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
     normalOrder (a * (anPart (StateAlgebra.ofState φ)) * (crPart (StateAlgebra.ofState φ')) * b) =
     𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • normalOrder (a * (crPart (StateAlgebra.ofState φ')) *
diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean
index 47b89f9..a2f2757 100644
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean
@@ -209,7 +209,6 @@ lemma superCommute_anPart_anPart (φ φ' : 𝓕.States) :
     rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
     simp [crAnStatistics, ← ofCrAnList_append]
 
-
 lemma superCommute_crPart_ofStateList (φ : 𝓕.States) (φs : List 𝓕.States) :
     ⟨crPart (StateAlgebra.ofState φ), ofStateList φs⟩ₛca =
     crPart (StateAlgebra.ofState φ) * ofStateList φs - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofStateList φs *
@@ -294,7 +293,6 @@ lemma ofStateList_mul_ofState_eq_superCommute (φs : List 𝓕.States) (φ : 
   rw [superCommute_ofStateList_ofState]
   simp
 
-
 lemma crPart_mul_anPart_eq_superCommute (φ φ' : 𝓕.States) :
     crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') =
     𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • anPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) +
@@ -406,7 +404,6 @@ lemma superCommute_ofCrAnList_ofStateList_cons (φ : 𝓕.States) (φs : List 
   rw [ofStateList_cons, mul_assoc, smul_smul, FieldStatistic.ofList_cons_eq_mul]
   simp [mul_comm]
 
-
 lemma superCommute_ofCrAnList_ofCrAnList_eq_sum (φs : List 𝓕.CrAnStates) :
     (φs' : List 𝓕.CrAnStates) →
     ⟨ofCrAnList φs, ofCrAnList φs'⟩ₛca =
diff --git a/HepLean/PerturbationTheory/FieldSpecification/Examples.lean b/HepLean/PerturbationTheory/FieldSpecification/Examples.lean
index dfb714c..c93cbbb 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/Examples.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/Examples.lean
@@ -8,7 +8,6 @@ import HepLean.PerturbationTheory.FieldSpecification.Basic
 
 # Specific examples of field specifications
 
-
 -/
 
 namespace FieldSpecification
diff --git a/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean b/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
index c7bfac4..9bdacdf 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
@@ -10,8 +10,6 @@ import HepLean.PerturbationTheory.FieldSpecification.Filters
 
 # Normal Ordering of states
 
-
-
 -/
 
 namespace FieldSpecification
diff --git a/HepLean/PerturbationTheory/WickContraction/Sign.lean b/HepLean/PerturbationTheory/WickContraction/Sign.lean
index 7804cfc..2c1091a 100644
--- a/HepLean/PerturbationTheory/WickContraction/Sign.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Sign.lean
@@ -903,7 +903,7 @@ lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.S
 
 lemma signInsertSomeCoef_eq_finset (φ : 𝓕.States) (φs : List 𝓕.States)
     (c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted)
-    (hφj : (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[j.1])) :  c.signInsertSomeCoef φ φs i j =
+    (hφj : (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[j.1])) : c.signInsertSomeCoef φ φs i j =
     if i < i.succAbove j then
       𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get,
       (Finset.univ.filter (fun x => i < i.succAbove x ∧ x < j ∧ ((c.getDual? x = none) ∨
diff --git a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean
index 260eeb3..362045a 100644
--- a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean
+++ b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean
@@ -18,12 +18,6 @@ namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)
 open HepLean.List
 
-/-!
-
-## Time contract.
-
--/
-
 /-- Given a Wick contraction `c` associated with a list `φs`, the
   product of all time-contractions of pairs of contracted elements in `φs`,
   as a member of the center of `𝓞.A`. -/
diff --git a/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean b/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean
index fafc8c3..e3aed04 100644
--- a/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean
+++ b/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean
@@ -219,7 +219,6 @@ lemma uncontractedList_length_eq_card (c : WickContraction n) :
   rw [uncontractedList_eq_sort]
   exact Finset.length_sort fun x1 x2 => x1 ≤ x2
 
-
 lemma filter_uncontractedList (c : WickContraction n) (p : Fin n → Prop) [DecidablePred p] :
     (c.uncontractedList.filter p) = (c.uncontracted.filter p).sort (· ≤ ·) := by
   have h1 : (c.uncontractedList.filter p).Sorted (· ≤ ·) := by
@@ -237,14 +236,12 @@ lemma filter_uncontractedList (c : WickContraction n) (p : Fin n → Prop) [Deci
   have hx := (List.toFinset_sort (· ≤ ·) h2).mpr h1
   rw [← hx, h3]
 
-
 /-!
 
 ## uncontractedIndexEquiv
 
 -/
 
-
 /-- The equivalence between the positions of `c.uncontractedList` i.e. elements of
   `Fin (c.uncontractedList).length` and the finite set `c.uncontracted` considered as a finite type.
 -/
@@ -315,7 +312,6 @@ lemma uncontractedStatesEquiv_list_sum [AddCommMonoid α] (φs : List 𝓕.State
 
 -/
 
-
 lemma uncontractedList_succAboveEmb_sorted (c : WickContraction n) (i : Fin n.succ) :
     ((List.map i.succAboveEmb c.uncontractedList)).Sorted (· ≤ ·) := by
   apply fin_list_sorted_succAboveEmb_sorted