From 408a676bbda7c45332328c59a911859918c25f10 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Sun, 5 Jan 2025 17:00:36 +0000
Subject: [PATCH] refactor: style lint

---
 .../ComplexTensor/PauliMatrices/Basis.lean    |   2 +-
 HepLean/Mathematics/Fin/Involutions.lean      | 116 +++++++++---------
 HepLean/Mathematics/List.lean                 |   3 +-
 .../Contractions/Basic.lean                   |  25 ++--
 .../PerturbationTheory/Contractions/Card.lean |   4 +-
 .../Contractions/Involutions.lean             |  63 +++++-----
 .../Wick/CreateAnnihilateSection.lean         |   3 +-
 .../Wick/Signs/InsertSign.lean                |   2 +-
 .../Wick/Signs/KoszulSign.lean                |   4 +-
 .../Wick/StaticTheorem.lean                   |   2 +-
 10 files changed, 111 insertions(+), 113 deletions(-)

diff --git a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean
index 3186a12..84a73ed 100644
--- a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean
+++ b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean
@@ -485,7 +485,7 @@ lemma pauliMatrix_contr_down_3 :
     rw [contrBasisVectorMul_pos _]
   conv =>
     lhs; rhs; rhs; lhs;
-    rw [contrBasisVectorMul_pos  _]
+    rw [contrBasisVectorMul_pos _]
   conv =>
     lhs
     simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
diff --git a/HepLean/Mathematics/Fin/Involutions.lean b/HepLean/Mathematics/Fin/Involutions.lean
index 8baed46..b5d7689 100644
--- a/HepLean/Mathematics/Fin/Involutions.lean
+++ b/HepLean/Mathematics/Fin/Involutions.lean
@@ -25,7 +25,7 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
   toFun f := ⟨⟨
     fun i =>
     if h : f.1 i.succ = 0 then i
-    else Fin.pred (f.1 i.succ) h , by
+    else Fin.pred (f.1 i.succ) h, by
     intro i
     by_cases h : f.1 i.succ = 0
     · simp [h]
@@ -33,7 +33,7 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
       simp only [f.2 i.succ, Fin.pred_succ, dite_eq_ite, ite_eq_right_iff]
       intro h
       exact False.elim (Fin.succ_ne_zero i h)⟩,
-    ⟨if h : f.1 0 = 0 then none else Fin.pred (f.1 0) h , by
+    ⟨if h : f.1 0 = 0 then none else Fin.pred (f.1 0) h, by
     by_cases h0 : f.1 0 = 0
     · simp [h0]
     · simp only [succ_eq_add_one, h0, ↓reduceDIte, Option.isSome_some, Option.get_some,
@@ -43,8 +43,7 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
       if h : (f.2.1).isSome then
         Fin.cons (f.2.1.get h).succ (Function.update (Fin.succ ∘ f.1.1) (f.2.1.get h) 0)
       else
-        Fin.cons 0 (Fin.succ ∘ f.1.1)
-    , by
+        Fin.cons 0 (Fin.succ ∘ f.1.1), by
     by_cases hs : (f.2.1).isSome
     · simp only [Nat.succ_eq_add_one, hs, ↓reduceDIte, Fin.coe_eq_castSucc]
       let a := f.2.1.get hs
@@ -59,7 +58,7 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
         by_cases hja : j = a
         · subst hja
           simp
-        · rw [Function.update_apply ]
+        · rw [Function.update_apply]
           rw [if_neg hja]
           simp only [Function.comp_apply, Fin.cons_succ]
           have hf2 := f.2.2 hs
@@ -145,12 +144,12 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
         · rename_i h
           exact False.elim (Fin.succ_ne_zero (f i) h)
         · rfl
-    · simp only [Nat.succ_eq_add_one,  Option.mem_def,
+    · simp only [Nat.succ_eq_add_one, Option.mem_def,
       Option.dite_none_left_eq_some, Option.some.injEq]
       by_cases hs : f0.isSome
       · simp only [hs, ↓reduceDIte]
         simp only [Fin.cons_zero, Fin.pred_succ, exists_prop]
-        have hx : ¬  (f0.get hs).succ = 0 :=  (Fin.succ_ne_zero (f0.get hs))
+        have hx : ¬ (f0.get hs).succ = 0 := (Fin.succ_ne_zero (f0.get hs))
         simp only [hx, not_false_eq_true, true_and]
         refine Iff.intro (fun hi => ?_) (fun hi => ?_)
         · rw [← hi]
@@ -166,7 +165,7 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
         subst hs
         exact ne_of_beq_false rfl
 
-lemma involutionCons_ext {n : ℕ} {f1 f2 :  (f : {f : Fin n → Fin n // Function.Involutive f}) ×
+lemma involutionCons_ext {n : ℕ} {f1 f2 : (f : {f : Fin n → Fin n // Function.Involutive f}) ×
     {i : Option (Fin n) // ∀ (h : i.isSome), f.1 (Option.get i h) = (Option.get i h)}}
     (h1 : f1.1 = f2.1) (h2 : f1.2 = Equiv.subtypeEquivRight (by rw [h1]; simp) f2.2) : f1 = f2 := by
   cases f1
@@ -181,10 +180,9 @@ lemma involutionCons_ext {n : ℕ} {f1 f2 :  (f : {f : Fin n → Fin n // Functi
   simp_all only
   rfl
 
-
 def involutionAddEquiv {n : ℕ} (f : {f : Fin n → Fin n // Function.Involutive f}) :
     {i : Option (Fin n) // ∀ (h : i.isSome), f.1 (Option.get i h) = (Option.get i h)} ≃
-    Option (Fin (Finset.univ.filter fun i => f.1 i = i).card)  := by
+    Option (Fin (Finset.univ.filter fun i => f.1 i = i).card) := by
   let e1 : {i : Option (Fin n) // ∀ (h : i.isSome), f.1 (Option.get i h) = (Option.get i h)}
         ≃ Option {i : Fin n // f.1 i = i} :=
     { toFun := fun i => match i with
@@ -208,14 +206,13 @@ def involutionAddEquiv {n : ℕ} (f : {f : Fin n → Fin n // Function.Involutiv
     funext i
     simp [s]
   let e2 : {i // i ∈ s} ≃ Fin (Finset.card s) := by
-     refine (Finset.orderIsoOfFin _ ?_).symm.toEquiv
-     simp [s]
+    refine (Finset.orderIsoOfFin _ ?_).symm.toEquiv
+    simp [s]
   refine e1.trans (Equiv.optionCongr (e2'.trans (e2)))
 
-
 lemma involutionAddEquiv_none_image_zero {n : ℕ} :
     {f : {f : Fin n.succ → Fin n.succ // Function.Involutive f}}
-    → involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2  = none
+    → involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2 = none
     → f.1 ⟨0, Nat.zero_lt_succ n⟩ = ⟨0, Nat.zero_lt_succ n⟩ := by
   intro f h
   simp only [Nat.succ_eq_add_one, involutionCons, Equiv.coe_fn_mk, involutionAddEquiv,
@@ -235,28 +232,29 @@ lemma involutionAddEquiv_none_image_zero {n : ℕ} :
     next h_2 => simp_all only [Subtype.mk.injEq, reduceCtorEq]
 
 lemma involutionAddEquiv_cast {n : ℕ} {f1 f2 : {f : Fin n → Fin n // Function.Involutive f}}
-    (hf : f1 = f2):
-    involutionAddEquiv f1 =  (Equiv.subtypeEquivRight  (by rw [hf]; simp)).trans
-      ((involutionAddEquiv f2).trans (Equiv.optionCongr (finCongr (by rw [hf])))):= by
+    (hf : f1 = f2) :
+    involutionAddEquiv f1 = (Equiv.subtypeEquivRight (by rw [hf]; simp)).trans
+      ((involutionAddEquiv f2).trans (Equiv.optionCongr (finCongr (by rw [hf])))) := by
   subst hf
   simp only [finCongr_refl, Equiv.optionCongr_refl, Equiv.trans_refl]
   rfl
 
-
 lemma involutionAddEquiv_cast' {m : ℕ} {f1 f2 : {f : Fin m → Fin m // Function.Involutive f}}
-  {N : ℕ} (hf : f1 = f2) (n : Option (Fin N)) (hn1 : N = (Finset.filter (fun i => f1.1 i = i) Finset.univ).card)
-  (hn2 : N = (Finset.filter (fun i => f2.1 i = i) Finset.univ).card):
-    HEq ((involutionAddEquiv f1).symm (Option.map (finCongr hn1) n)) ((involutionAddEquiv f2).symm (Option.map (finCongr hn2) n)) := by
+  {N : ℕ} (hf : f1 = f2) (n : Option (Fin N))
+  (hn1 : N = (Finset.filter (fun i => f1.1 i = i) Finset.univ).card)
+  (hn2 : N = (Finset.filter (fun i => f2.1 i = i) Finset.univ).card) :
+    HEq ((involutionAddEquiv f1).symm (Option.map (finCongr hn1) n))
+    ((involutionAddEquiv f2).symm (Option.map (finCongr hn2) n)) := by
   subst hf
   rfl
 
 lemma involutionAddEquiv_none_succ {n : ℕ}
     {f : {f : Fin n.succ → Fin n.succ // Function.Involutive f}}
-    (h : involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2  = none)
-    (x : Fin n) : f.1 x.succ  = x.succ ↔ (involutionCons n f).1.1 x = x := by
+    (h : involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2 = none)
+    (x : Fin n) : f.1 x.succ = x.succ ↔ (involutionCons n f).1.1 x = x := by
   simp only [succ_eq_add_one, involutionCons, Fin.cons_update, Equiv.coe_fn_mk, dite_eq_left_iff]
   have hn' := involutionAddEquiv_none_image_zero h
-  have hx : ¬ f.1 x.succ = ⟨0,  Nat.zero_lt_succ n⟩:= by
+  have hx : ¬ f.1 x.succ = ⟨0, Nat.zero_lt_succ n⟩:= by
     rw [← hn']
     exact fun hn => Fin.succ_ne_zero x (Function.Involutive.injective f.2 hn)
   apply Iff.intro
@@ -286,7 +284,7 @@ lemma involutionAddEquiv_isSome_image_zero {n : ℕ} :
 def involutionNoFixedEquivSum {n : ℕ} :
     {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f
     ∧ ∀ i, f i ≠ i} ≃ Σ (k : Fin (2 * n + 1)),
-     {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f
+    {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f
     ∧ (∀ i, f i ≠ i) ∧ f 0 = k.succ} where
   toFun f := ⟨(f.1 0).pred (f.2.2 0), ⟨f.1, f.2.1, by simpa using f.2.2⟩⟩
   invFun f := ⟨f.2.1, ⟨f.2.2.1, f.2.2.2.1⟩⟩
@@ -310,7 +308,7 @@ The main aim of thes equivalences is to define `involutionNoFixedZeroEquivProd`.
 
 def involutionNoFixedZeroSetEquivEquiv {n : ℕ}
     (k : Fin (2 * n + 1)) (e : Fin (2 * n.succ) ≃ Fin (2 * n.succ)) :
-     {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f
+    {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f
     ∧ (∀ i, f i ≠ i) ∧ f 0 = k.succ} ≃
     {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive (e.symm ∘ f ∘ e) ∧
       (∀ i, (e.symm ∘ f ∘ e) i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ} where
@@ -332,11 +330,12 @@ def involutionNoFixedZeroSetEquivEquiv {n : ℕ}
     ext i
     simp
 
-def involutionNoFixedZeroSetEquivSetEquiv {n : ℕ} (k : Fin (2 * n + 1)) (e : Fin (2 * n.succ) ≃ Fin (2 * n.succ)) :
+def involutionNoFixedZeroSetEquivSetEquiv {n : ℕ} (k : Fin (2 * n + 1))
+  (e : Fin (2 * n.succ) ≃ Fin (2 * n.succ)) :
   {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive (e.symm ∘ f ∘ e) ∧
       (∀ i, (e.symm ∘ f ∘ e) i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ} ≃
     {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
-      (∀ i, f i ≠ i) ∧  (e.symm ∘ f ∘ e) 0 = k.succ} := by
+      (∀ i, f i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ} := by
   refine Equiv.subtypeEquivRight ?_
   intro f
   have h1 : Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive f := by
@@ -360,12 +359,12 @@ def involutionNoFixedZeroSetEquivSetEquiv {n : ℕ} (k : Fin (2 * n + 1)) (e : F
     nth_rewrite 2 [← hn] at hi
     simp at hi
 
-
-def involutionNoFixedZeroSetEquivEquiv' {n : ℕ} (k : Fin (2 * n + 1)) (e : Fin (2 * n.succ) ≃ Fin (2 * n.succ)) :
+def involutionNoFixedZeroSetEquivEquiv' {n : ℕ} (k : Fin (2 * n + 1))
+    (e : Fin (2 * n.succ) ≃ Fin (2 * n.succ)) :
     {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
-      (∀ i, f i ≠ i) ∧  (e.symm ∘ f ∘ e) 0 = k.succ}
+      (∀ i, f i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ}
       ≃ {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
-      (∀ i, f i ≠ i) ∧  f (e 0) = e k.succ} := by
+      (∀ i, f i ≠ i) ∧ f (e 0) = e k.succ} := by
   refine Equiv.subtypeEquivRight ?_
   simp only [succ_eq_add_one, ne_eq, Function.comp_apply, and_congr_right_iff]
   intro f hi h1
@@ -373,13 +372,13 @@ def involutionNoFixedZeroSetEquivEquiv' {n : ℕ} (k : Fin (2 * n + 1)) (e : Fin
 
 def involutionNoFixedZeroSetEquivSetOne {n : ℕ} (k : Fin (2 * n + 1)) :
     {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
-      (∀ i, f i ≠ i) ∧  f 0 = k.succ}
+      (∀ i, f i ≠ i) ∧ f 0 = k.succ}
       ≃ {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
-      (∀ i, f i ≠ i) ∧  f 0 = 1} := by
+      (∀ i, f i ≠ i) ∧ f 0 = 1} := by
   refine Equiv.trans (involutionNoFixedZeroSetEquivEquiv k (Equiv.swap k.succ 1)) ?_
   refine Equiv.trans (involutionNoFixedZeroSetEquivSetEquiv k (Equiv.swap k.succ 1)) ?_
   refine Equiv.trans (involutionNoFixedZeroSetEquivEquiv' k (Equiv.swap k.succ 1)) ?_
-  refine  Equiv.subtypeEquivRight ?_
+  refine Equiv.subtypeEquivRight ?_
   simp only [succ_eq_add_one, ne_eq, Equiv.swap_apply_left, and_congr_right_iff]
   intro f hi h1
   rw [Equiv.swap_apply_of_ne_of_ne]
@@ -387,10 +386,9 @@ def involutionNoFixedZeroSetEquivSetOne {n : ℕ} (k : Fin (2 * n + 1)) :
   · exact Fin.zero_ne_one
 
 def involutionNoFixedSetOne {n : ℕ} :
-     {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
-      (∀ i, f i ≠ i) ∧  f 0 = 1} ≃
-      {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧
-      (∀ i, f i ≠ i)} where
+    {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
+    (∀ i, f i ≠ i) ∧ f 0 = 1} ≃ {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧
+    (∀ i, f i ≠ i)} where
   toFun f := by
     have hf1 : f.1 1 = 0 := by
       have hf := f.2.2.2
@@ -444,7 +442,7 @@ def involutionNoFixedSetOne {n : ℕ} :
           rename_i x r
           simp_all only [succ_eq_add_one, Fin.ext_iff, Fin.val_succ, add_left_inj]
           have hfn {a b : ℕ} {ha : a < 2 * n} {hb : b < 2 * n}
-            (hab : ↑(f.1 ⟨a, ha⟩) = b): ↑(f.1 ⟨b, hb⟩) = a := by
+            (hab : ↑(f.1 ⟨a, ha⟩) = b) : ↑(f.1 ⟨b, hb⟩) = a := by
             have ht : f.1 ⟨a, ha⟩ = ⟨b, hb⟩ := by
               simp [hab, Fin.ext_iff]
             rw [← ht, f.2.1]
@@ -504,7 +502,7 @@ def involutionNoFixedSetOne {n : ℕ} :
     simp only [Fin.coe_pred]
     split
     · rename_i h
-      simp [Fin.ext_iff]  at h
+      simp [Fin.ext_iff] at h
     · rename_i h
       simp [Fin.ext_iff] at h
     · rename_i h
@@ -513,22 +511,23 @@ def involutionNoFixedSetOne {n : ℕ} :
       apply congrArg
       simp_all [Fin.ext_iff]
 
-
 def involutionNoFixedZeroSetEquiv {n : ℕ} (k : Fin (2 * n + 1)) :
     {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
-      (∀ i, f i ≠ i) ∧  f 0 = k.succ}
+      (∀ i, f i ≠ i) ∧ f 0 = k.succ}
       ≃ {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
   refine Equiv.trans (involutionNoFixedZeroSetEquivSetOne k) involutionNoFixedSetOne
 
 def involutionNoFixedEquivSumSame {n : ℕ} :
     {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧ (∀ i, f i ≠ i)}
-    ≃  Σ (_ : Fin (2 * n + 1)), {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
+    ≃ Σ (_ : Fin (2 * n + 1)),
+      {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
   refine Equiv.trans involutionNoFixedEquivSum ?_
   refine Equiv.sigmaCongrRight involutionNoFixedZeroSetEquiv
 
 def involutionNoFixedZeroEquivProd {n : ℕ} :
     {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧ (∀ i, f i ≠ i)}
-    ≃ Fin (2 * n + 1) × {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
+    ≃ Fin (2 * n + 1) ×
+    {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
   refine Equiv.trans involutionNoFixedEquivSumSame ?_
   exact Equiv.sigmaEquivProd (Fin (2 * n + 1))
       { f // Function.Involutive f ∧ ∀ (i : Fin (2 * n)), f i ≠ i}
@@ -539,27 +538,24 @@ def involutionNoFixedZeroEquivProd {n : ℕ} :
 
 -/
 
-
-instance {n : ℕ}  : Fintype { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } := by
-  haveI : DecidablePred fun x => Function.Involutive x := by
-    intro f
-    apply Fintype.decidableForallFintype (α := Fin n)
-  haveI : DecidablePred fun x => Function.Involutive x ∧ ∀ (i : Fin n), x i ≠ i := by
-     intro x
-     apply instDecidableAnd
+instance {n : ℕ} : Fintype { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } := by
+  haveI : DecidablePred fun x => Function.Involutive x :=
+    fun f => Fintype.decidableForallFintype (α := Fin n)
+  haveI : DecidablePred fun x => Function.Involutive x ∧ ∀ (i : Fin n), x i ≠ i :=
+    fun x => instDecidableAnd
   apply Subtype.fintype
 
 lemma involutionNoFixed_card_succ {n : ℕ} :
-   Fintype.card {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧ (∀ i, f i ≠ i)}
-    = (2 * n + 1) * Fintype.card {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
-  rw [Fintype.card_congr (involutionNoFixedZeroEquivProd)]
-  rw [Fintype.card_prod ]
+    Fintype.card
+    {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧ (∀ i, f i ≠ i)}
+    = (2 * n + 1) *
+    Fintype.card {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
+  rw [Fintype.card_congr (involutionNoFixedZeroEquivProd), Fintype.card_prod]
   congr
   exact Fintype.card_fin (2 * n + 1)
 
-
 lemma involutionNoFixed_card_mul_two : (n : ℕ) →
-   Fintype.card {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)}
+    Fintype.card {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)}
     = (2 * n - 1)‼
   | 0 => rfl
   | Nat.succ n => by
@@ -568,7 +564,7 @@ lemma involutionNoFixed_card_mul_two : (n : ℕ) →
     exact Eq.symm (Nat.doubleFactorial_add_one (Nat.mul 2 n))
 
 lemma involutionNoFixed_card_even : (n : ℕ) → (he : Even n) →
-    Fintype.card {f : Fin n → Fin n  // Function.Involutive f ∧ (∀ i, f i ≠ i)} = (n - 1)‼ := by
+    Fintype.card {f : Fin n → Fin n // Function.Involutive f ∧ (∀ i, f i ≠ i)} = (n - 1)‼ := by
   intro n he
   obtain ⟨r, hr⟩ := he
   have hr' : n = 2 * r := by omega
diff --git a/HepLean/Mathematics/List.lean b/HepLean/Mathematics/List.lean
index ef5ed81..5966221 100644
--- a/HepLean/Mathematics/List.lean
+++ b/HepLean/Mathematics/List.lean
@@ -662,7 +662,6 @@ def optionErase {I : Type} (l : List I) (i : Option (Fin l.length)) : List I :=
   | none => l
   | some i => List.eraseIdx l i
 
-
 lemma eraseIdx_length {I : Type} (l : List I) (i : Fin l.length) :
     (List.eraseIdx l i).length + 1 = l.length := by
   simp only [List.length_eraseIdx, Fin.is_lt, ↓reduceIte]
@@ -744,7 +743,7 @@ lemma optionEraseZ_some_length {I : Type} (l : List I) (a : I) (i : (Fin l.lengt
 lemma optionEraseZ_ext {I : Type} {l l' : List I} {a a' : I} {i : Option (Fin l.length)}
     {i' : Option (Fin l'.length)} (hl : l = l') (ha : a = a')
     (hi : Option.map (Fin.cast (by rw [hl])) i = i') :
-    optionEraseZ l a i =  optionEraseZ l' a' i' := by
+    optionEraseZ l a i = optionEraseZ l' a' i' := by
   subst hl
   subst ha
   cases hi
diff --git a/HepLean/PerturbationTheory/Contractions/Basic.lean b/HepLean/PerturbationTheory/Contractions/Basic.lean
index f4af2b3..57faf24 100644
--- a/HepLean/PerturbationTheory/Contractions/Basic.lean
+++ b/HepLean/PerturbationTheory/Contractions/Basic.lean
@@ -33,12 +33,12 @@ namespace Contractions
 
 variable {l : List 𝓕} (c : Contractions l)
 
-def auxCongr  : {φs: List 𝓕} →  {φsᵤₙ φsᵤₙ' : List 𝓕} → (h : φsᵤₙ = φsᵤₙ') →
+def auxCongr : {φs: List 𝓕} → {φsᵤₙ φsᵤₙ' : List 𝓕} → (h : φsᵤₙ = φsᵤₙ') →
     ContractionsAux φs φsᵤₙ ≃ ContractionsAux φs φsᵤₙ'
   | _, _, _, Eq.refl _ => Equiv.refl _
 
 lemma auxCongr_ext {φs: List 𝓕} {c c2 : Contractions φs} (h : c.1 = c2.1)
-    (hx : c.2 =  auxCongr h.symm c2.2) : c = c2 := by
+    (hx : c.2 = auxCongr h.symm c2.2) : c = c2 := by
   cases c
   cases c2
   simp only at h
@@ -50,7 +50,7 @@ lemma auxCongr_ext {φs: List 𝓕} {c c2 : Contractions φs} (h : c.1 = c2.1)
 /-- The list of uncontracted fields. -/
 def uncontracted : List 𝓕 := c.1
 
-lemma uncontracted_length_even_iff :  {l : List 𝓕} →  (c : Contractions l) →
+lemma uncontracted_length_even_iff : {l : List 𝓕} → (c : Contractions l) →
     Even l.length ↔ Even c.uncontracted.length
   | [], ⟨[], ContractionsAux.nil⟩ => by
     simp [uncontracted]
@@ -76,7 +76,8 @@ lemma contractions_nil (a : Contractions ([] : List 𝓕)) : a = ⟨[], Contract
   cases c
   rfl
 
-def embedUncontracted {l : List 𝓕} (c : Contractions l) : Fin c.uncontracted.length → Fin l.length :=
+def embedUncontracted {l : List 𝓕} (c : Contractions l) :
+    Fin c.uncontracted.length → Fin l.length :=
   match l, c with
   | [], ⟨[], ContractionsAux.nil⟩ => Fin.elim0
   | φ :: φs, ⟨_, .cons (φsᵤₙ := aux) none c⟩ =>
@@ -93,7 +94,7 @@ def embedUncontracted {l : List 𝓕} (c : Contractions l) : Fin c.uncontracted.
       exact Fin.elim0 n
     omega
 
-lemma embedUncontracted_injective  {l : List 𝓕} (c : Contractions l) :
+lemma embedUncontracted_injective {l : List 𝓕} (c : Contractions l) :
     Function.Injective c.embedUncontracted := by
   match l, c with
   | [], ⟨[], ContractionsAux.nil⟩ =>
@@ -108,12 +109,12 @@ lemma embedUncontracted_injective  {l : List 𝓕} (c : Contractions l) :
       exact fun x => Fin.succ_ne_zero (embedUncontracted ⟨aux, c⟩ x)
     · exact Function.Injective.comp (Fin.succ_injective φs.length)
         (embedUncontracted_injective ⟨aux, c⟩)
-  |  φ :: φs, ⟨_, .cons (φsᵤₙ := aux) (some i) c⟩ =>
-      dsimp only [List.length_cons, embedUncontracted]
-      refine Function.Injective.comp (Fin.succ_injective φs.length) ?hf
-      refine Function.Injective.comp (embedUncontracted_injective ⟨aux, c⟩) ?hf.hf
-      refine Function.Injective.comp (Fin.cast_injective (embedUncontracted.proof_5 φ φs aux i c))
-        Fin.succAbove_right_injective
+  | φ :: φs, ⟨_, .cons (φsᵤₙ := aux) (some i) c⟩ =>
+    dsimp only [List.length_cons, embedUncontracted]
+    refine Function.Injective.comp (Fin.succ_injective φs.length) ?hf
+    refine Function.Injective.comp (embedUncontracted_injective ⟨aux, c⟩) ?hf.hf
+    refine Function.Injective.comp (Fin.cast_injective (embedUncontracted.proof_5 φ φs aux i c))
+      Fin.succAbove_right_injective
 
 /-- Establishes uniqueness of contractions for a single field, showing that any contraction
   of a single field must be equivalent to the trivial contraction with no pairing. -/
@@ -161,7 +162,7 @@ def consEquiv {φ : 𝓕} {φs : List 𝓕} :
 lemma consEquiv_ext {φs : List 𝓕} {c1 c2 : Contractions φs}
     {n1 : Option (Fin c1.uncontracted.length)} {n2 : Option (Fin c2.uncontracted.length)}
     (hc : c1 = c2) (hn : Option.map (finCongr (by rw [hc])) n1 = n2) :
-    (⟨c1, n1⟩ :  (c : Contractions φs) × Option (Fin c.uncontracted.length)) = ⟨c2, n2⟩ := by
+    (⟨c1, n1⟩ : (c : Contractions φs) × Option (Fin c.uncontracted.length)) = ⟨c2, n2⟩ := by
   subst hc
   subst hn
   simp
diff --git a/HepLean/PerturbationTheory/Contractions/Card.lean b/HepLean/PerturbationTheory/Contractions/Card.lean
index 0edb7f9..03a9ef3 100644
--- a/HepLean/PerturbationTheory/Contractions/Card.lean
+++ b/HepLean/PerturbationTheory/Contractions/Card.lean
@@ -17,13 +17,13 @@ open HepLean.Fin
 open Nat
 
 /-- There are `(φs.length - 1)‼` full contractions of a list `φs` with an even number of fields. -/
-lemma card_of_full_contractions_even {φs : List 𝓕} (he : Even φs.length ) :
+lemma card_of_full_contractions_even {φs : List 𝓕} (he : Even φs.length) :
     Fintype.card {c : Contractions φs // IsFull c} = (φs.length - 1)‼ := by
   rw [Fintype.card_congr (isFullInvolutionEquiv (φs := φs))]
   exact involutionNoFixed_card_even φs.length he
 
 /-- There are no full contractions of a list with an odd number of fields. -/
-lemma card_of_full_contractions_odd {φs : List 𝓕} (ho : Odd φs.length ) :
+lemma card_of_full_contractions_odd {φs : List 𝓕} (ho : Odd φs.length) :
     Fintype.card {c : Contractions φs // IsFull c} = 0 := by
   rw [Fintype.card_eq_zero_iff, isEmpty_subtype]
   intro c
diff --git a/HepLean/PerturbationTheory/Contractions/Involutions.lean b/HepLean/PerturbationTheory/Contractions/Involutions.lean
index d624ad1..65b4d4b 100644
--- a/HepLean/PerturbationTheory/Contractions/Involutions.lean
+++ b/HepLean/PerturbationTheory/Contractions/Involutions.lean
@@ -38,7 +38,7 @@ variable {l : List 𝓕}
 
 /-- Given an involution the uncontracted fields associated with it (corresponding
   to the fixed points of that involution). -/
-def uncontractedFromInvolution :  {φs : List 𝓕} →
+def uncontractedFromInvolution : {φs : List 𝓕} →
     (f : {f : Fin φs.length → Fin φs.length // Function.Involutive f}) →
     {l : List 𝓕 // l.length = (Finset.univ.filter fun i => f.1 i = i).card}
   | [], _ => ⟨[], by simp⟩
@@ -46,7 +46,7 @@ def uncontractedFromInvolution :  {φs : List 𝓕} →
     let luc := uncontractedFromInvolution (involutionCons φs.length f).fst
     let n' := involutionAddEquiv (involutionCons φs.length f).1 (involutionCons φs.length f).2
     let np : Option (Fin luc.1.length) := Option.map (finCongr luc.2.symm) n'
-    if  hn : n' = none then
+    if hn : n' = none then
       have hn' := involutionAddEquiv_none_image_zero (n := φs.length) (f := f) hn
       ⟨optionEraseZ luc φ none, by
         simp only [optionEraseZ, Nat.succ_eq_add_one, List.length_cons, Mathlib.Vector.length_val]
@@ -55,7 +55,7 @@ def uncontractedFromInvolution :  {φs : List 𝓕} →
         rw [Fin.sum_univ_succ]
         conv_rhs => erw [if_pos hn']
         ring_nf
-        simp only [Nat.succ_eq_add_one, Mathlib.Vector.length_val,  Nat.cast_id,
+        simp only [Nat.succ_eq_add_one, Mathlib.Vector.length_val, Nat.cast_id,
           add_right_inj]
         rw [Finset.card_filter]
         apply congrArg
@@ -72,17 +72,18 @@ def uncontractedFromInvolution :  {φs : List 𝓕} →
           Option.isSome_none, Equiv.trans_apply, Equiv.coe_fn_mk, Equiv.optionCongr_apply,
           Equiv.coe_trans, RelIso.coe_fn_toEquiv, Option.map_eq_none', n'] at hn
         split at hn
-        · simp_all only [reduceCtorEq, not_false_eq_true, Nat.succ_eq_add_one, Option.isSome_some, k']
+        · simp_all only [reduceCtorEq, not_false_eq_true, Nat.succ_eq_add_one,
+            Option.isSome_some, k']
         · simp_all only [not_true_eq_false]
       let k := k'.1.get hkIsSome
       rw [optionEraseZ_some_length]
       have hksucc : k.succ = f.1 ⟨0, Nat.zero_lt_succ φs.length⟩ := by
         simp [k, k', involutionCons]
-      have hzero : ⟨0, Nat.zero_lt_succ φs.length⟩  = f.1 k.succ := by
+      have hzero : ⟨0, Nat.zero_lt_succ φs.length⟩ = f.1 k.succ := by
         rw [hksucc, f.2]
       have hksuccNe : f.1 k.succ ≠ k.succ := by
         conv_rhs => rw [hksucc]
-        exact fun hn => Fin.succ_ne_zero k (Function.Involutive.injective f.2 hn )
+        exact fun hn => Fin.succ_ne_zero k (Function.Involutive.injective f.2 hn)
       have hluc : 1 ≤ luc.1.length := by
         simp only [Nat.succ_eq_add_one, Mathlib.Vector.length_val, Finset.one_le_card]
         use k
@@ -131,8 +132,8 @@ lemma uncontractedFromInvolution_cons {φs : List 𝓕} {φ : 𝓕}
     (involutionAddEquiv (involutionCons φs.length f).1 (involutionCons φs.length f).2)) := by
   let luc := uncontractedFromInvolution (involutionCons φs.length f).fst
   let n' := involutionAddEquiv (involutionCons φs.length f).1 (involutionCons φs.length f).2
-  change _ = optionEraseZ luc φ
-    (Option.map (finCongr ((uncontractedFromInvolution (involutionCons φs.length f).fst).2.symm)) n')
+  change _ = optionEraseZ luc φ (Option.map
+    (finCongr ((uncontractedFromInvolution (involutionCons φs.length f).fst).2.symm)) n')
   dsimp only [List.length_cons, uncontractedFromInvolution, Nat.succ_eq_add_one, Fin.zero_eta]
   by_cases hn : n' = none
   · have hn' := hn
@@ -165,10 +166,10 @@ lemma uncontractedFromInvolution_cons {φs : List 𝓕} {φ : 𝓕}
       simp_all only [Option.get_some]
 
 /-- The `ContractionsAux` associated to an involution. -/
-def fromInvolutionAux  : {l : List 𝓕} →
+def fromInvolutionAux : {l : List 𝓕} →
     (f : {f : Fin l.length → Fin l.length // Function.Involutive f}) →
     ContractionsAux l (uncontractedFromInvolution f)
-  | [] => fun _ =>  ContractionsAux.nil
+  | [] => fun _ => ContractionsAux.nil
   | _ :: φs => fun f =>
     let f' := involutionCons φs.length f
     let c' := fromInvolutionAux f'.1
@@ -177,8 +178,9 @@ def fromInvolutionAux  : {l : List 𝓕} →
     auxCongr (uncontractedFromInvolution_cons f).symm (ContractionsAux.cons n' c')
 
 /-- The contraction associated with an involution. -/
-def fromInvolution {φs : List 𝓕} (f : {f : Fin φs.length → Fin φs.length // Function.Involutive f}) :
-    Contractions φs := ⟨uncontractedFromInvolution f, fromInvolutionAux f⟩
+def fromInvolution {φs : List 𝓕}
+    (f : {f : Fin φs.length → Fin φs.length // Function.Involutive f}) : Contractions φs :=
+  ⟨uncontractedFromInvolution f, fromInvolutionAux f⟩
 
 lemma fromInvolution_cons {φs : List 𝓕} {φ : 𝓕}
       (f : {f : Fin (φ :: φs).length → Fin (φ :: φs).length // Function.Involutive f}) :
@@ -195,8 +197,8 @@ lemma fromInvolution_cons {φs : List 𝓕} {φ : 𝓕}
     rfl
 
 lemma fromInvolution_of_involutionCons {φs : List 𝓕} {φ : 𝓕}
-    (f : {f : Fin (φs ).length → Fin (φs).length // Function.Involutive f})
-    (n : { i : Option (Fin φs.length) // ∀ (h : i.isSome = true), f.1 (i.get h) = i.get h }):
+    (f : {f : Fin φs.length → Fin φs.length // Function.Involutive f})
+    (n : { i : Option (Fin φs.length) // ∀ (h : i.isSome = true), f.1 (i.get h) = i.get h }) :
     fromInvolution (φs := φ :: φs) ((involutionCons φs.length).symm ⟨f, n⟩) =
     consEquiv.symm ⟨fromInvolution f, Option.map (finCongr ((uncontractedFromInvolution f).2.symm))
       (involutionAddEquiv f n)⟩ := by
@@ -212,7 +214,7 @@ lemma fromInvolution_of_involutionCons {φs : List 𝓕} {φ : 𝓕}
 -/
 
 /-- The involution associated with a contraction. -/
-def toInvolution  : {φs : List 𝓕} →  (c : Contractions φs) →
+def toInvolution : {φs : List 𝓕} → (c : Contractions φs) →
     {f : {f : Fin φs.length → Fin φs.length // Function.Involutive f} //
     uncontractedFromInvolution f = c.1}
   | [], ⟨[], ContractionsAux.nil⟩ => ⟨⟨fun i => i, by
@@ -223,22 +225,23 @@ def toInvolution  : {φs : List 𝓕} →  (c : Contractions φs) →
     let n' : Option (Fin (uncontractedFromInvolution ⟨f', hf1⟩).1.length) :=
       Option.map (finCongr (by rw [hf2])) n
     let F := (involutionCons φs.length).symm ⟨⟨f', hf1⟩,
-       (involutionAddEquiv ⟨f', hf1⟩).symm
-       (Option.map (finCongr ((uncontractedFromInvolution ⟨f', hf1⟩).2))  n')⟩
+        (involutionAddEquiv ⟨f', hf1⟩).symm
+        (Option.map (finCongr ((uncontractedFromInvolution ⟨f', hf1⟩).2)) n')⟩
     refine ⟨F, ?_⟩
     have hF0 : ((involutionCons φs.length) F) = ⟨⟨f', hf1⟩,
-       (involutionAddEquiv  ⟨f', hf1⟩).symm
-       (Option.map (finCongr ((uncontractedFromInvolution ⟨f', hf1⟩).2))  n')⟩ := by
+        (involutionAddEquiv ⟨f', hf1⟩).symm
+        (Option.map (finCongr ((uncontractedFromInvolution ⟨f', hf1⟩).2)) n')⟩ := by
       simp [F]
     have hF1 : ((involutionCons φs.length) F).fst = ⟨f', hf1⟩ := by
       rw [hF0]
     have hF2L : ((uncontractedFromInvolution ⟨f', hf1⟩)).1.length =
       (Finset.filter (fun i => ((involutionCons φs.length) F).1.1 i = i) Finset.univ).card := by
-      apply  Eq.trans ((uncontractedFromInvolution ⟨f', hf1⟩)).2
+      apply Eq.trans ((uncontractedFromInvolution ⟨f', hf1⟩)).2
       congr
       rw [hF1]
-    have hF2 : ((involutionCons φs.length) F).snd = (involutionAddEquiv ((involutionCons φs.length) F).fst).symm
-      (Option.map (finCongr hF2L) n') := by
+    have hF2 : ((involutionCons φs.length) F).snd =
+        (involutionAddEquiv ((involutionCons φs.length) F).fst).symm
+        (Option.map (finCongr hF2L) n') := by
       rw [@Sigma.subtype_ext_iff] at hF0
       ext1
       rw [hF0.2]
@@ -314,8 +317,9 @@ lemma toInvolution_fromInvolution : {φs : List 𝓕} → (c : Contractions φs)
       simp only [Option.mem_def, Option.map_eq_some', Function.comp_apply, Fin.cast_trans,
         Fin.cast_eq_self, exists_eq_right]
 
-lemma fromInvolution_toInvolution : {φs : List 𝓕} →  (f : {f : Fin (φs ).length → Fin (φs).length // Function.Involutive f})
-    → toInvolution (fromInvolution f) = f
+lemma fromInvolution_toInvolution : {φs : List 𝓕} →
+    (f : {f : Fin φs.length → Fin φs.length // Function.Involutive f}) →
+    toInvolution (fromInvolution f) = f
   | [], _ => by
     ext x
     exact Fin.elim0 x
@@ -331,7 +335,7 @@ lemma fromInvolution_toInvolution : {φs : List 𝓕} →  (f : {f : Fin (φs ).
       rw [Equiv.symm_apply_eq]
       conv_rhs =>
         lhs
-        rw  [involutionAddEquiv_cast hx]
+        rw [involutionAddEquiv_cast hx]
       simp only [Nat.succ_eq_add_one, Equiv.trans_apply]
       rfl
 
@@ -339,7 +343,7 @@ lemma fromInvolution_toInvolution : {φs : List 𝓕} →  (f : {f : Fin (φs ).
   Note: This shows that the type of contractions only depends on the length of the list `φs`. -/
 def equivInvolutions {φs : List 𝓕} :
     Contractions φs ≃ {f : Fin φs.length → Fin φs.length // Function.Involutive f} where
-  toFun := fun c =>  toInvolution c
+  toFun := fun c => toInvolution c
   invFun := fromInvolution
   left_inv := toInvolution_fromInvolution
   right_inv := fromInvolution_toInvolution
@@ -355,7 +359,7 @@ lemma isFull_iff_uncontractedFromInvolution_empty {φs : List 𝓕} (c : Contrac
   erw [l.2]
   rfl
 
-lemma isFull_iff_filter_card_involution_zero  {φs : List 𝓕} (c : Contractions φs) :
+lemma isFull_iff_filter_card_involution_zero {φs : List 𝓕} (c : Contractions φs) :
     IsFull c ↔ (Finset.univ.filter fun i => (equivInvolutions c).1 i = i).card = 0 := by
   rw [isFull_iff_uncontractedFromInvolution_empty, List.ext_get_iff]
   simp
@@ -372,21 +376,18 @@ lemma isFull_iff_involution_no_fixed_points {φs : List 𝓕} (c : Contractions
   · intro i h
     exact fun a => i h
 
-
 /-- The equivalence between full contractions and fixed-point free involutions. -/
 def isFullInvolutionEquiv {φs : List 𝓕} : {c : Contractions φs // IsFull c} ≃
     {f : Fin φs.length → Fin φs.length // Function.Involutive f ∧ (∀ i, f i ≠ i)} where
   toFun c := ⟨equivInvolutions c.1, by
     apply And.intro (equivInvolutions c.1).2
     rw [← isFull_iff_involution_no_fixed_points]
-    exact c.2
-    ⟩
+    exact c.2⟩
   invFun f := ⟨equivInvolutions.symm ⟨f.1, f.2.1⟩, by
     rw [isFull_iff_involution_no_fixed_points]
     simpa using f.2.2⟩
   left_inv c := by simp
   right_inv f := by simp
 
-
 end Contractions
 end Wick
diff --git a/HepLean/PerturbationTheory/Wick/CreateAnnihilateSection.lean b/HepLean/PerturbationTheory/Wick/CreateAnnihilateSection.lean
index 1d43b95..68ffbcf 100644
--- a/HepLean/PerturbationTheory/Wick/CreateAnnihilateSection.lean
+++ b/HepLean/PerturbationTheory/Wick/CreateAnnihilateSection.lean
@@ -26,7 +26,8 @@ namespace CreateAnnihilateSect
 
 section basic_defs
 
-variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] {φs : List 𝓕} (a : CreateAnnihilateSect f φs)
+variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] {φs : List 𝓕}
+  (a : CreateAnnihilateSect f φs)
 
 /-- The type `CreateAnnihilateSect f φs` is finite. -/
 instance fintype : Fintype (CreateAnnihilateSect f φs) := Pi.fintype
diff --git a/HepLean/PerturbationTheory/Wick/Signs/InsertSign.lean b/HepLean/PerturbationTheory/Wick/Signs/InsertSign.lean
index c6d21dd..4a7b818 100644
--- a/HepLean/PerturbationTheory/Wick/Signs/InsertSign.lean
+++ b/HepLean/PerturbationTheory/Wick/Signs/InsertSign.lean
@@ -84,7 +84,7 @@ def insertSign (n : ℕ) (φ : 𝓕) (φs : List 𝓕) : ℂ :=
   superCommuteCoef q [φ] (List.take n φs)
 
 /-- If `φ` is bosonic, there is no sign associated with inserting it into a list of fields. -/
-lemma insertSign_bosonic (n : ℕ)  (φ : 𝓕) (φs : List 𝓕) (hφ : q φ = bosonic) :
+lemma insertSign_bosonic (n : ℕ) (φ : 𝓕) (φs : List 𝓕) (hφ : q φ = bosonic) :
     insertSign q n φ φs = 1 := by
   simp only [insertSign, superCommuteCoef, ofList_singleton, hφ, reduceCtorEq, false_and,
     ↓reduceIte]
diff --git a/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean b/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean
index dfc2a2e..31ce0bc 100644
--- a/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean
+++ b/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean
@@ -160,10 +160,10 @@ lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) :
       rw [← insertionSortEquiv_get]
       simp only [Function.comp_apply, Equiv.symm_apply_apply, List.get_eq_getElem, ni]
       simp_all only [List.length_cons, add_le_add_iff_right, List.getElem_insertIdx_self]
-    have hc1 (hninro : ni.castSucc < nro) :  ¬ le φ1 φ := by
+    have hc1 (hninro : ni.castSucc < nro) : ¬ le φ1 φ := by
       rw [← hns]
       exact lt_orderedInsertPos_rel le φ1 rs ni hninro
-    have hc2 (hninro : ¬ ni.castSucc < nro) :  le φ1 φ := by
+    have hc2 (hninro : ¬ ni.castSucc < nro) : le φ1 φ := by
       rw [← hns]
       refine gt_orderedInsertPos_rel le φ1 rs ?_ ni hninro
       exact List.sorted_insertionSort le (List.insertIdx n φ φs)
diff --git a/HepLean/PerturbationTheory/Wick/StaticTheorem.lean b/HepLean/PerturbationTheory/Wick/StaticTheorem.lean
index 16bad3a..ab50d86 100644
--- a/HepLean/PerturbationTheory/Wick/StaticTheorem.lean
+++ b/HepLean/PerturbationTheory/Wick/StaticTheorem.lean
@@ -29,7 +29,7 @@ lemma static_wick_nil {A : Type} [Semiring A] [Algebra ℂ A]
   rw [← Contractions.nilEquiv.symm.sum_comp]
   simp only [Finset.univ_unique, PUnit.default_eq_unit, Contractions.nilEquiv, Equiv.coe_fn_symm_mk,
     Finset.sum_const, Finset.card_singleton, one_smul]
-  dsimp [Contractions.uncontracted, Contractions.toCenterTerm]
+  dsimp only [Contractions.toCenterTerm, Contractions.uncontracted]
   simp [ofListLift_empty]
 
 lemma static_wick_cons [IsTrans ((i : 𝓕) × f i) le] [IsTotal ((i : 𝓕) × f i) le]