diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean
index b732f8b..9a4e16d 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean
@@ -55,7 +55,7 @@ lemma staticWickTerm_insert_zero_some (φ : 𝓕.FieldOp) (φs : List 𝓕.Field
   simp only [← mul_assoc]
   rw [← smul_mul_assoc]
   congr 1
-  rw [staticConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt]
+  rw [staticContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt]
   swap
   · simp
   rw [smul_smul]
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
index dfaf193..0f5903c 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
@@ -114,7 +114,7 @@ lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   rw [wickTerm]
   by_cases hg : GradingCompliant φs φsΛ ∧ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[k.1])
   · by_cases hk : i.succAbove k < i
-    · rw [WickContraction.timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt]
+    · rw [WickContraction.timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt]
       swap
       · exact hn _ hk
       · rw [normalOrder_uncontracted_some, sign_insert_some_of_lt φ φs φsΛ i k hk hg]
@@ -134,7 +134,7 @@ lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
         rw [mul_assoc, mul_assoc, mul_comm, mul_assoc, mul_assoc]
         simp
       · omega
-  · rw [timeConract_insertAndContract_some]
+  · rw [timeContract_insertAndContract_some]
     simp only [Fin.getElem_fin, not_and] at hg
     by_cases hg' : GradingCompliant φs φsΛ
     · have hg := hg hg'
diff --git a/HepLean/PerturbationTheory/WickContraction/StaticContract.lean b/HepLean/PerturbationTheory/WickContraction/StaticContract.lean
index e16a083..c98be1a 100644
--- a/HepLean/PerturbationTheory/WickContraction/StaticContract.lean
+++ b/HepLean/PerturbationTheory/WickContraction/StaticContract.lean
@@ -66,7 +66,7 @@ lemma staticContract_insertAndContract_some
 
 open FieldStatistic
 
-lemma staticConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
+lemma staticContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
     (hik : i < i.succAbove k) :
diff --git a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean
index bd2bff2..58941be 100644
--- a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean
+++ b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean
@@ -50,7 +50,7 @@ lemma timeContract_insertAndContract_none (φ : 𝓕.FieldOp) (φs : List 𝓕.F
 This follows from the fact that `(φsΛ ↩Λ φ i (some j))` has one more contracted pair than `φsΛ`,
 corresponding to `φ` contracted with `φⱼ`. The order depends on whether we insert `φ` before
 or after `φⱼ`. -/
-lemma timeConract_insertAndContract_some
+lemma timeContract_insertAndContract_some
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
     (φsΛ ↩Λ φ i (some j)).timeContract =
@@ -85,7 +85,7 @@ lemma timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
     𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < k))⟩)
     • (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) *
       φsΛ.timeContract) := by
-  rw [timeConract_insertAndContract_some]
+  rw [timeContract_insertAndContract_some]
   simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1,
     contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,
     Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast,
@@ -110,7 +110,7 @@ lemma timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
     simp only [exchangeSign_mul_self]
     · exact ht
 
-lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt
+lemma timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
     (ht : ¬ 𝓕.timeOrderRel φs[k.1] φ) (hik : ¬ i < i.succAbove k) :
@@ -118,7 +118,7 @@ lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt
     𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x ≤ k))⟩)
     • (contractStateAtIndex φ [φsΛ]ᵘᶜ
       ((uncontractedFieldOpEquiv φs φsΛ) (some k)) * φsΛ.timeContract) := by
-  rw [timeConract_insertAndContract_some]
+  rw [timeContract_insertAndContract_some]
   simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1,
     contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,
     Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast,