Merge pull request #293 from HEPLean/pitmonticone/golf

2025-01-23 10:36:32 +01:00 · 2025-01-23 10:36:32 +01:00 · a326d40ae9
commit a326d40ae9
parent 9bea3bd1cb 902434cb08
16 changed files with 161 additions and 312 deletions
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
@ -286,11 +286,8 @@ lemma inLineEqToSol_proj (T : InLineEqSol) : inLineEqToSol (inLineEqProj T) = T.
 /-- Given an element of `inQuad × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
 def inQuadToSol : InQuad × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a₁, a₂, a₃) =>
  AnomalyFreeMk' (lineCube R.val.val a₁ a₂ a₃)
-    (by
-      erw [planeY₃B₃_quad]
-      rw [R.prop.1, R.prop.2.1, R.prop.2.2]
-      simp)
-    (lineCube_cube R.val.val a₁ a₂ a₃)
+    (by erw [planeY₃B₃_quad, R.prop.1, R.prop.2.1, R.prop.2.2]; simp)
+      (lineCube_cube R.val.val a₁ a₂ a₃)

 lemma inQuadToSol_smul (R : InQuad) (c₁ c₂ c₃ d : ℚ) :
    inQuadToSol (R, (d * c₁), (d * c₂), (d * c₃)) = d • inQuadToSol (R, c₁, c₂, c₃) := by
@ -314,9 +311,7 @@ lemma inQuadToSol_proj (T : InQuadSol) : inQuadToSol (inQuadProj T) = T.val := b
  rw [inQuadProj, inQuadToSol_smul]
  apply ACCSystem.Sols.ext
  change _ • (planeY₃B₃ _ _ _ _).val = _
-  rw [planeY₃B₃_val]
-  rw [Y₃_plus_B₃_plus_proj]
-  rw [cube_proj, cube_proj_proj_B₃, cube_proj_proj_Y₃]
+  rw [planeY₃B₃_val, Y₃_plus_B₃_plus_proj, cube_proj, cube_proj_proj_B₃, cube_proj_proj_Y₃]
  ring_nf
  simp only [zero_smul, add_zero, Fin.isValue, Fin.reduceFinMk, zero_add]
  have h1 : (cubeTriLin T.val.val T.val.val Y₃.val ^ 2 * dot Y₃.val B₃.val ^ 3 * 3 +
@ -331,14 +326,8 @@ lemma inQuadToSol_proj (T : InQuadSol) : inQuadToSol (inQuadProj T) = T.val := b
 /-- Given a element of `inQuadCube × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
 def inQuadCubeToSol : InQuadCube × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, b₁, b₂, b₃) =>
  AnomalyFreeMk' (planeY₃B₃ R.val.val.val b₁ b₂ b₃)
-  (by
-    rw [planeY₃B₃_quad]
-    rw [R.val.prop.1, R.val.prop.2.1, R.val.prop.2.2]
-    simp)
-  (by
-    rw [planeY₃B₃_cubic]
-    rw [R.prop.1, R.prop.2.1, R.prop.2.2]
-    simp)
+  (by rw [planeY₃B₃_quad, R.val.prop.1, R.val.prop.2.1, R.val.prop.2.2]; simp)
+  (by rw [planeY₃B₃_cubic, R.prop.1, R.prop.2.1, R.prop.2.2]; simp)

 lemma inQuadCubeToSol_smul (R : InQuadCube) (c₁ c₂ c₃ d : ℚ) :
    inQuadCubeToSol (R, (d * c₁), (d * c₂), (d * c₃)) = d • inQuadCubeToSol (R, c₁, c₂, c₃) := by
@ -361,8 +350,7 @@ lemma inQuadCubeToSol_proj (T : InQuadCubeSol) :
  rw [inQuadCubeProj, inQuadCubeToSol_smul]
  apply ACCSystem.Sols.ext
  change _ • (planeY₃B₃ _ _ _ _).val = _
-  rw [planeY₃B₃_val]
-  rw [Y₃_plus_B₃_plus_proj]
+  rw [planeY₃B₃_val, Y₃_plus_B₃_plus_proj]
  ring_nf
  simp only [Fin.isValue, Fin.reduceFinMk, zero_smul, add_zero, zero_add]
  rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel₀]
@ -389,8 +377,7 @@ lemma toSol_toSolNSProj (T : NotInLineEqSol) :
  use toSolNSProj T.val
  have h1 : ¬ LineEqProp (toSolNSProj T.val).1 :=
    (linEqPropSol_iff_proj_linEqProp T.val).mpr.mt T.prop
-  rw [toSol]
-  simp_all
+  simp_rw [toSol, h1]
  exact toSolNS_proj T

 lemma toSol_inLineEq (T : InLineEqSol) : ∃ X, toSol X = T.val := by
@ -398,8 +385,7 @@ lemma toSol_inLineEq (T : InLineEqSol) : ∃ X, toSol X = T.val := by
  use ⟨X.1.val, X.2.1, X.2.2⟩
  have : ¬ InQuadProp X.1.val := (inQuadSolProp_iff_proj_inQuadProp T.val).mpr.mt T.prop.2
  have : LineEqProp X.1.val := (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1
-  rw [toSol]
-  simp_all
+  simp_all only [toSol]
  exact inLineEqToSol_proj T

 lemma toSol_inQuad (T : InQuadSol) : ∃ X, toSol X = T.val := by
@ -408,8 +394,7 @@ lemma toSol_inQuad (T : InQuadSol) : ∃ X, toSol X = T.val := by
  have : ¬ InCubeProp X.1.val.val := (inCubeSolProp_iff_proj_inCubeProp T.val).mpr.mt T.prop.2.2
  have : InQuadProp X.1.val.val := (inQuadSolProp_iff_proj_inQuadProp T.val).mp T.prop.2.1
  have : LineEqProp X.1.val.val := (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1
-  rw [toSol]
-  simp_all
+  simp_all only [toSol]
  exact inQuadToSol_proj T

 lemma toSol_inQuadCube (T : InQuadCubeSol) : ∃ X, toSol X = T.val := by
@ -418,8 +403,7 @@ lemma toSol_inQuadCube (T : InQuadCubeSol) : ∃ X, toSol X = T.val := by
  have : InCubeProp X.1.val.val.val := (inCubeSolProp_iff_proj_inCubeProp T.val).mp T.prop.2.2
  have : InQuadProp X.1.val.val.val := (inQuadSolProp_iff_proj_inQuadProp T.val).mp T.prop.2.1
  have : LineEqProp X.1.val.val.val := (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1
-  rw [toSol]
-  simp_all
+  simp_all only [toSol]
  exact inQuadCubeToSol_proj T

 theorem toSol_surjective : Function.Surjective toSol := by
--- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
@ -136,7 +136,7 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}
  rw [P_P_P!_accCube' g f hfg] at h1
  simp only [Nat.succ_eq_add_one, neg_add_rev, mul_eq_zero] at h1
  cases h1 <;> rename_i h1
-  · apply Or.inl
+  · left
    linear_combination h1
  · cases h1 <;> rename_i h1
    · refine Or.inr (Or.inl ?_)
--- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
@ -123,7 +123,7 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols}
  rw [P_P_P!_accCube' g f hfg] at h1
  simp only [Nat.succ_eq_add_one, mul_eq_zero] at h1
  cases h1 <;> rename_i h1
-  · apply Or.inl
+  · left
    linear_combination h1
  · cases h1 <;> rename_i h1
    · refine Or.inr (Or.inl ?_)
--- a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
+++ b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
@ -75,7 +75,7 @@ lemma swap_fields : P.toFun Φ1 Φ2 =
    normSq_apply_im_zero, mul_zero, zero_add, RingHomCompTriple.comp_apply, RingHom.id_apply]
  ring_nf
  simp only [one_div, add_left_inj, add_right_inj, mul_eq_mul_left_iff]
-  apply Or.inl
+  left
  rw [HiggsField.innerProd, HiggsField.innerProd, ← InnerProductSpace.conj_symm, Complex.abs_conj]

 /-- If `Φ₂` is zero the potential reduces to the Higgs potential on `Φ₁`. -/
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
@ -69,8 +69,7 @@ section sines
 /-- For a CKM matrix `sin θ₁₂` is non-negative. -/
 lemma S₁₂_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₁₂ V := by
  rw [S₁₂, div_nonneg_iff]
-  apply Or.inl
-  apply (And.intro (VAbs_ge_zero 0 1 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2)))
+  exact .inl (.intro (VAbs_ge_zero 0 1 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2)))

 /-- For a CKM matrix `sin θ₁₃` is non-negative. -/
 lemma S₁₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₁₃ V :=
@ -82,8 +81,7 @@ lemma S₂₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₂₃ V := by
  · rw [S₂₃, if_pos ha]
    exact VAbs_ge_zero 1 0 V
  · rw [S₂₃, if_neg ha, @div_nonneg_iff]
-    apply Or.inl
-    apply And.intro (VAbs_ge_zero 1 2 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2))
+    exact .inl (.intro (VAbs_ge_zero 1 2 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2)))

 /-- For a CKM matrix `sin θ₁₂` is less then or equal to 1. -/
 lemma S₁₂_leq_one (V : Quotient CKMMatrixSetoid) : S₁₂ V ≤ 1 := by
@ -95,7 +93,7 @@ lemma S₁₂_leq_one (V : Quotient CKMMatrixSetoid) : S₁₂ V ≤ 1 := by
      cases' h2 with h2 h2
      simp_all
      exact h2
-    apply Or.inl
+    left
    simp_all only [VudAbs, VusAbs, or_true, Real.sqrt_pos, true_and]
    rw [Real.le_sqrt (VAbs_ge_zero 0 1 V) (le_of_lt h3)]
    simp only [Fin.isValue, le_add_iff_nonneg_left]
--- a/HepLean/Lorentz/Group/Boosts.lean
+++ b/HepLean/Lorentz/Group/Boosts.lean
@ -150,7 +150,7 @@ lemma toMatrix_apply (u v : FuturePointing d) (μ ν : Fin 1 ⊕ Fin d) :
    Action.instMonoidalCategory_tensorUnit_V, CategoryTheory.Equivalence.symm_inverse,
    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
    Pi.smul_apply, smul_eq_mul, Pi.sub_apply, Pi.neg_apply]
-  apply Or.inl
+  left
  ring

 open minkowskiMatrix in
--- a/HepLean/Mathematics/Fin/Involutions.lean
+++ b/HepLean/Mathematics/Fin/Involutions.lean
@ -208,8 +208,7 @@ def involutionAddEquiv {n : ℕ} (f : {f : Fin n → Fin n // Function.Involutiv
        simp_all only [Subtype.coe_eta] }
  let s : Finset (Fin n) := Finset.univ.filter fun i => f.1 i = i
  let e2' : { i : Fin n // f.1 i = i} ≃ {i // i ∈ s} := by
-    refine Equiv.subtypeEquivProp ?h
-    funext i
+    apply Equiv.subtypeEquivProp
    simp [s]
  let e2 : {i // i ∈ s} ≃ Fin (Finset.card s) := by
    refine (Finset.orderIsoOfFin _ ?_).symm.toEquiv
@ -242,7 +241,7 @@ lemma involutionAddEquiv_cast {n : ℕ} {f1 f2 : {f : Fin n → Fin n // Functio
    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]
+  rw [finCongr_refl, Equiv.optionCongr_refl]
  rfl

 lemma involutionAddEquiv_cast' {m : ℕ} {f1 f2 : {f : Fin m → Fin m // Function.Involutive f}}
@ -259,33 +258,18 @@ lemma involutionAddEquiv_none_succ {n : ℕ}
    (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
-    rw [← hn']
-    exact fun hn => Fin.succ_ne_zero x (Function.Involutive.injective f.2 hn)
-  apply Iff.intro
-  · intro h2 h3
-    rw [Fin.ext_iff]
-    simp [h2]
-  · intro h2
-    have h2' := h2 hx
-    conv_rhs => rw [← h2']
-    simp
+  have hx : ¬ f.1 x.succ = ⟨0, Nat.zero_lt_succ n⟩:=
+    involutionAddEquiv_none_image_zero h ▸
+      fun hn => Fin.succ_ne_zero x (Function.Involutive.injective f.2 hn)
+  exact Iff.intro (fun h2 ↦ by simp [h2]) (fun h2 ↦ (Fin.pred_eq_iff_eq_succ hx).mp (h2 hx))

 lemma involutionAddEquiv_isSome_image_zero {n : ℕ} :
    {f : {f : Fin n.succ → Fin n.succ // Function.Involutive f}}
    → (involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2).isSome
    → ¬ f.1 ⟨0, Nat.zero_lt_succ n⟩ = ⟨0, Nat.zero_lt_succ n⟩ := by
-  intro f hf
-  simp only [succ_eq_add_one, involutionCons, Equiv.coe_fn_mk, involutionAddEquiv,
-    Option.isSome_some, Option.get_some, Option.isSome_none, Equiv.trans_apply,
-    Equiv.optionCongr_apply, Equiv.coe_trans, RelIso.coe_fn_toEquiv, Option.isSome_map'] at hf
-  simp_all only [List.length_cons, Fin.zero_eta]
-  obtain ⟨val, property⟩ := f
-  simp_all only [List.length_cons]
-  apply Aesop.BuiltinRules.not_intro
-  intro a
-  simp_all only [↓reduceDIte, Option.isSome_none, Bool.false_eq_true]
+  intro f hf a
+  simp only [succ_eq_add_one, involutionCons, Equiv.coe_fn_mk, involutionAddEquiv] at hf
+  simp_all

 /-!

@ -303,15 +287,11 @@ def involutionNoFixedEquivSum {n : ℕ} :
    ∧ (∀ 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⟩⟩
-  left_inv f := by
-    rfl
+  left_inv f := rfl
  right_inv f := by
-    simp only [succ_eq_add_one, ne_eq, mul_eq]
    ext
-    · simp only [Fin.coe_pred]
-      rw [f.2.2.2.2]
-      simp
-    · simp
+    · simp [f.2.2.2.2]
+    · rfl

 /-- The condition on fixed point free involutions of `Fin n.succ` for a fixed value of `f 0`,
  can be modified by conjugation with an equivalence. -/
@ -329,8 +309,7 @@ def involutionNoFixedZeroSetEquivEquiv {n : ℕ}
    intro i
    simp only [succ_eq_add_one, Function.comp_apply, ne_eq, Equiv.apply_symm_apply]
    have hf2 := f.2.1 i
-    simpa using hf2, by
-      simpa using f.2.2.1, by simpa using f.2.2.2⟩
+    simpa using hf2, by simpa using f.2.2.1, by simpa using f.2.2.2⟩
  left_inv f := by
    ext i
    simp
@ -485,7 +464,7 @@ def involutionNoFixedSetOne {n : ℕ} :
          simp [Fin.ext_iff] at h
      | ⟨(Nat.succ (Nat.succ m)), h⟩ =>
        simp only [succ_eq_add_one, ne_eq, Fin.ext_iff, Fin.val_succ, add_left_inj, f']
-        have hf:= f.2.2 ⟨m, by exact Nat.add_lt_add_iff_right.mp h⟩
+        have hf:= f.2.2 ⟨m, Nat.add_lt_add_iff_right.mp h⟩
        simp only [ne_eq, Fin.ext_iff] at hf
        omega
    · simp only [succ_eq_add_one, ne_eq, f']
@ -505,13 +484,9 @@ def involutionNoFixedSetOne {n : ℕ} :
    ext i
    simp only
    split
-    · simp only [Fin.val_one, succ_eq_add_one, Fin.zero_eta]
-      rw [f.2.2.2]
-      simp
-    · simp only [Fin.val_zero, succ_eq_add_one, Fin.mk_one]
-      rw [hf1]
-      simp
-    · rfl
+    · simp [Fin.val_one, succ_eq_add_one, Fin.zero_eta, f.2.2.2]
+    · exact congrArg Fin.val (id (Eq.symm hf1))
+    · exact rfl
  right_inv f := by
    simp only [ne_eq, mul_eq, succ_eq_add_one, Function.comp_apply]
    ext i
@ -521,8 +496,7 @@ def involutionNoFixedSetOne {n : ℕ} :
      simp [Fin.ext_iff] at h
    · rename_i h
      simp [Fin.ext_iff] at h
-    · rename_i h
-      simp only [Fin.val_succ, add_tsub_cancel_right]
+    · simp only [Fin.val_succ, add_tsub_cancel_right]
      congr
      apply congrArg
      simp_all [Fin.ext_iff]
@ -552,8 +526,7 @@ def involutionNoFixedZeroEquivProd {n : ℕ} :
    ≃ Fin n.succ ×
    {f : Fin n → Fin n // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
  refine Equiv.trans involutionNoFixedEquivSumSame ?_
-  exact Equiv.sigmaEquivProd (Fin n.succ)
-      { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i}
+  exact Equiv.sigmaEquivProd (Fin n.succ) { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }

 /-!

--- a/HepLean/Mathematics/List.lean
+++ b/HepLean/Mathematics/List.lean
@ -707,7 +707,7 @@ lemma eraseIdx_get {I : Type} (l : List I) (i : Fin l.length) :
  ext x
  simp only [Function.comp_apply, List.get_eq_getElem, List.eraseIdx, List.getElem_eraseIdx]
  simp only [Fin.succAbove, Fin.coe_cast]
-  by_cases hi: x.castSucc < Fin.cast (by exact Eq.symm (eraseIdx_length l i)) i
+  by_cases hi: x.castSucc < Fin.cast (Eq.symm (eraseIdx_length l i)) i
  · simp only [hi, ↓reduceIte, Fin.coe_castSucc, dite_eq_left_iff, not_lt]
    intro h
    rw [Fin.lt_def] at hi
--- a/HepLean/Mathematics/List/InsertionSort.lean
+++ b/HepLean/Mathematics/List/InsertionSort.lean
@ -34,7 +34,7 @@ lemma insertionSortMin_lt_mem_insertionSortDropMinPos {α : Type} (r : α → α
    (i : Fin (insertionSortDropMinPos r a l).length) :
    r (insertionSortMin r a l) ((insertionSortDropMinPos r a l)[i]) := by
  let l1 := List.insertionSort r (a :: l)
-  have hl1 : l1.Sorted r := by exact List.sorted_insertionSort r (a :: l)
+  have hl1 : l1.Sorted r := List.sorted_insertionSort r (a :: l)
  simp only [l1] at hl1
  rw [insertionSort_eq_insertionSortMin_cons r a l] at hl1
  simp only [List.sorted_cons, List.mem_insertionSort] at hl1
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean
@ -61,12 +61,10 @@ lemma ofCrAnList_cons (φ : 𝓕.CrAnStates) (φs : List 𝓕.CrAnStates) :

 lemma ofCrAnList_append (φs φs' : List 𝓕.CrAnStates) :
    ofCrAnList (φs ++ φs') = ofCrAnList φs * ofCrAnList φs' := by
-  dsimp only [ofCrAnList]
-  rw [List.map_append, List.prod_append]
+  simp [ofCrAnList, List.map_append]

 lemma ofCrAnList_singleton (φ : 𝓕.CrAnStates) :
-    ofCrAnList [φ] = ofCrAnState φ := by
-  simp [ofCrAnList]
+    ofCrAnList [φ] = ofCrAnState φ := by simp [ofCrAnList]

 /-- Maps a state to the sum of creation and annihilation operators in
  creation and annihilation free-algebra. -/
@ -94,8 +92,7 @@ lemma ofStateList_cons (φ : 𝓕.States) (φs : List 𝓕.States) :
    ofStateList (φ :: φs) = ofState φ * ofStateList φs := rfl

 lemma ofStateList_singleton (φ : 𝓕.States) :
-    ofStateList [φ] = ofState φ := by
-  simp [ofStateList]
+    ofStateList [φ] = ofState φ := by simp [ofStateList]

 lemma ofStateList_append (φs φs' : List 𝓕.States) :
    ofStateList (φs ++ φs') = ofStateList φs * ofStateList φs' := by
@ -104,13 +101,11 @@ lemma ofStateList_append (φs φs' : List 𝓕.States) :

 lemma ofStateAlgebra_ofList_eq_ofStateList : (φs : List 𝓕.States) →
    ofStateAlgebra (ofList φs) = ofStateList φs
-  | [] => by
-    simp [ofStateList]
+  | [] => by simp [ofStateList]
  | φ :: φs => by
-    rw [ofStateList_cons, StateAlgebra.ofList_cons]
-    rw [map_mul]
-    simp only [ofStateAlgebra_ofState, mul_eq_mul_left_iff]
-    apply Or.inl (ofStateAlgebra_ofList_eq_ofStateList φs)
+    rw [ofStateList_cons, StateAlgebra.ofList_cons, map_mul, ofStateAlgebra_ofState,
+      mul_eq_mul_left_iff]
+    exact .inl (ofStateAlgebra_ofList_eq_ofStateList φs)

 lemma ofStateList_sum (φs : List 𝓕.States) :
    ofStateList φs = ∑ (s : CrAnSection φs), ofCrAnList s.1 := by
@ -144,21 +139,18 @@ def crPart : 𝓕.StateAlgebra →ₐ[ℂ] 𝓕.CrAnAlgebra :=
@[simp]
 lemma crPart_negAsymp (φ : 𝓕.AsymptoticNegTime) :
    crPart (StateAlgebra.ofState (States.negAsymp φ)) = ofCrAnState ⟨States.negAsymp φ, ()⟩ := by
-  dsimp only [crPart, StateAlgebra.ofState]
-  rw [FreeAlgebra.lift_ι_apply]
+  simp [crPart, StateAlgebra.ofState]

@[simp]
 lemma crPart_position (φ : 𝓕.PositionStates) :
    crPart (StateAlgebra.ofState (States.position φ)) =
    ofCrAnState ⟨States.position φ, CreateAnnihilate.create⟩ := by
-  dsimp only [crPart, StateAlgebra.ofState]
-  rw [FreeAlgebra.lift_ι_apply]
+  simp [crPart, StateAlgebra.ofState]

@[simp]
 lemma crPart_posAsymp (φ : 𝓕.AsymptoticPosTime) :
    crPart (StateAlgebra.ofState (States.posAsymp φ)) = 0 := by
-  dsimp only [crPart, StateAlgebra.ofState]
-  rw [FreeAlgebra.lift_ι_apply]
+  simp [crPart, StateAlgebra.ofState]

 /-- The algebra map taking an element of the free-state algbra to
  the part of it in the creation and annihilation free algebra
@ -173,36 +165,26 @@ def anPart : 𝓕.StateAlgebra →ₐ[ℂ] 𝓕.CrAnAlgebra :=
@[simp]
 lemma anPart_negAsymp (φ : 𝓕.AsymptoticNegTime) :
    anPart (StateAlgebra.ofState (States.negAsymp φ)) = 0 := by
-  dsimp only [anPart, StateAlgebra.ofState]
-  rw [FreeAlgebra.lift_ι_apply]
+  simp [anPart, StateAlgebra.ofState]

@[simp]
 lemma anPart_position (φ : 𝓕.PositionStates) :
    anPart (StateAlgebra.ofState (States.position φ)) =
    ofCrAnState ⟨States.position φ, CreateAnnihilate.annihilate⟩ := by
-  dsimp only [anPart, StateAlgebra.ofState]
-  rw [FreeAlgebra.lift_ι_apply]
+  simp [anPart, StateAlgebra.ofState]

@[simp]
 lemma anPart_posAsymp (φ : 𝓕.AsymptoticPosTime) :
    anPart (StateAlgebra.ofState (States.posAsymp φ)) = ofCrAnState ⟨States.posAsymp φ, ()⟩ := by
-  dsimp only [anPart, StateAlgebra.ofState]
-  rw [FreeAlgebra.lift_ι_apply]
+  simp [anPart, StateAlgebra.ofState]

 lemma ofState_eq_crPart_add_anPart (φ : 𝓕.States) :
    ofState φ = crPart (StateAlgebra.ofState φ) + anPart (StateAlgebra.ofState φ) := by
  rw [ofState]
  cases φ with
-  | negAsymp φ =>
-    dsimp only [statesToCrAnType]
-    simp
-  | position φ =>
-    dsimp only [statesToCrAnType]
-    rw [CreateAnnihilate.sum_eq]
-    simp
-  | posAsymp φ =>
-    dsimp only [statesToCrAnType]
-    simp
+  | negAsymp φ => simp [statesToCrAnType]
+  | position φ => simp [statesToCrAnType, CreateAnnihilate.sum_eq]
+  | posAsymp φ => simp [statesToCrAnType]

 /-!

@ -223,11 +205,9 @@ lemma ofListBasis_eq_ofList (φs : List 𝓕.CrAnStates) :
  erw [MonoidAlgebra.lift_apply]
  simp only [zero_smul, Finsupp.sum_single_index, one_smul]
  rw [@FreeMonoid.lift_apply]
-  simp only [List.prod]
  match φs with
  | [] => rfl
-  | φ :: φs =>
-    erw [List.map_cons]
+  | φ :: φs => erw [List.map_cons]

 /-!

@ -239,8 +219,7 @@ lemma ofListBasis_eq_ofList (φs : List 𝓕.CrAnStates) :
 noncomputable def mulLinearMap : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 where
  toFun a := {
    toFun := fun b => a * b,
-    map_add' := fun c d => by
-      simp [mul_add]
+    map_add' := fun c d => by simp [mul_add]
    map_smul' := by simp}
  map_add' := fun a b => by
    ext c
@ -251,15 +230,13 @@ noncomputable def mulLinearMap : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕
    simp [smul_mul']

 lemma mulLinearMap_apply (a b : CrAnAlgebra 𝓕) :
-    mulLinearMap a b = a * b := by rfl
+    mulLinearMap a b = a * b := rfl

 /-- The linear map associated with scalar-multiplication in `CrAnAlgebra`. -/
 noncomputable def smulLinearMap (c : ℂ) : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 where
  toFun a := c • a
  map_add' := by simp
-  map_smul' m x := by
-    simp only [smul_smul, RingHom.id_apply]
-    rw [NonUnitalNormedCommRing.mul_comm]
+  map_smul' m x := by simp [smul_smul, RingHom.id_apply, NonUnitalNormedCommRing.mul_comm]

 end CrAnAlgebra

--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
@ -38,20 +38,16 @@ def normalOrder : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 :=

 lemma normalOrder_ofCrAnList (φs : List 𝓕.CrAnStates) :
    normalOrder (ofCrAnList φs) = normalOrderSign φs • ofCrAnList (normalOrderList φs) := by
-  rw [← ofListBasis_eq_ofList]
-  simp only [normalOrder, Basis.constr_basis]
+  rw [← ofListBasis_eq_ofList, normalOrder, Basis.constr_basis]

 lemma ofCrAnList_eq_normalOrder (φs : List 𝓕.CrAnStates) :
    ofCrAnList (normalOrderList φs) = normalOrderSign φs • normalOrder (ofCrAnList φs) := by
-  rw [normalOrder_ofCrAnList, normalOrderList]
-  rw [smul_smul]
-  simp only [normalOrderSign]
-  rw [Wick.koszulSign_mul_self]
-  simp
+  rw [normalOrder_ofCrAnList, normalOrderList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self,
+    one_smul]

 lemma normalOrder_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by
-  rw [← ofCrAnList_nil, normalOrder_ofCrAnList]
-  simp
+  rw [← ofCrAnList_nil, normalOrder_ofCrAnList, normalOrderSign_nil, normalOrderList_nil,
+    ofCrAnList_nil, one_smul]

 /-!

@ -63,8 +59,7 @@ lemma normalOrder_ofCrAnList_cons_create (φ : 𝓕.CrAnStates)
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnStates) :
    normalOrder (ofCrAnList (φ :: φs)) =
    ofCrAnState φ * normalOrder (ofCrAnList φs) := by
-  rw [normalOrder_ofCrAnList]
-  rw [normalOrderSign_cons_create φ hφ, normalOrderList_cons_create φ hφ φs]
+  rw [normalOrder_ofCrAnList, normalOrderSign_cons_create φ hφ, normalOrderList_cons_create φ hφ φs]
  rw [ofCrAnList_cons, normalOrder_ofCrAnList, mul_smul_comm]

 lemma normalOrder_create_mul (φ : 𝓕.CrAnStates)
@ -73,21 +68,18 @@ lemma normalOrder_create_mul (φ : 𝓕.CrAnStates)
    normalOrder (ofCrAnState φ * a) = ofCrAnState φ * normalOrder a := by
  change (normalOrder ∘ₗ mulLinearMap (ofCrAnState φ)) a =
    (mulLinearMap (ofCrAnState φ) ∘ₗ normalOrder) a
-  refine LinearMap.congr_fun ?h a
-  apply ofCrAnListBasis.ext
-  intro l
+  refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a
  simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList,
    LinearMap.coe_comp, Function.comp_apply]
-  rw [← ofCrAnList_cons]
-  rw [normalOrder_ofCrAnList_cons_create φ hφ]
+  rw [← ofCrAnList_cons, normalOrder_ofCrAnList_cons_create φ hφ]

 lemma normalOrder_ofCrAnList_append_annihilate (φ : 𝓕.CrAnStates)
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnStates) :
    normalOrder (ofCrAnList (φs ++ [φ])) =
    normalOrder (ofCrAnList φs) * ofCrAnState φ := by
-  rw [normalOrder_ofCrAnList]
-  rw [normalOrderSign_append_annihlate φ hφ φs, normalOrderList_append_annihilate φ hφ φs]
-  rw [ofCrAnList_append, ofCrAnList_singleton, normalOrder_ofCrAnList, smul_mul_assoc]
+  rw [normalOrder_ofCrAnList, normalOrderSign_append_annihlate φ hφ φs,
+    normalOrderList_append_annihilate φ hφ φs, ofCrAnList_append, ofCrAnList_singleton,
+      normalOrder_ofCrAnList, smul_mul_assoc]

 lemma normalOrder_mul_annihilate (φ : 𝓕.CrAnStates)
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate)
@ -95,46 +87,35 @@ lemma normalOrder_mul_annihilate (φ : 𝓕.CrAnStates)
    normalOrder (a * ofCrAnState φ) = normalOrder a * ofCrAnState φ := by
  change (normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φ)) a =
    (mulLinearMap.flip (ofCrAnState φ) ∘ₗ normalOrder) a
-  refine LinearMap.congr_fun ?h a
-  apply ofCrAnListBasis.ext
-  intro l
+  refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a
  simp only [mulLinearMap, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
    LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk]
-  rw [← ofCrAnList_singleton, ← ofCrAnList_append, ofCrAnList_singleton]
-  rw [normalOrder_ofCrAnList_append_annihilate φ hφ]
+  rw [← ofCrAnList_singleton, ← ofCrAnList_append, ofCrAnList_singleton,
+    normalOrder_ofCrAnList_append_annihilate φ hφ]

 lemma normalOrder_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
    normalOrder (crPart (StateAlgebra.ofState φ) * a) =
    crPart (StateAlgebra.ofState φ) * normalOrder a := by
  match φ with
  | .negAsymp φ =>
-    dsimp only [crPart, StateAlgebra.ofState]
-    simp only [FreeAlgebra.lift_ι_apply]
+    rw [crPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
    exact normalOrder_create_mul ⟨States.negAsymp φ, ()⟩ rfl a
  | .position φ =>
-    dsimp only [crPart, StateAlgebra.ofState]
-    simp only [FreeAlgebra.lift_ι_apply]
-    refine normalOrder_create_mul _ ?_ _
-    simp [crAnStatesToCreateAnnihilate]
-  | .posAsymp φ =>
-    simp
+    rw [crPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
+    exact normalOrder_create_mul _ rfl _
+  | .posAsymp φ => simp

 lemma normalOrder_mul_anPart (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
    normalOrder (a * anPart (StateAlgebra.ofState φ)) =
    normalOrder a * anPart (StateAlgebra.ofState φ) := by
  match φ with
-  | .negAsymp φ =>
-    simp
+  | .negAsymp φ => simp
  | .position φ =>
-    dsimp only [anPart, StateAlgebra.ofState]
-    simp only [FreeAlgebra.lift_ι_apply]
-    refine normalOrder_mul_annihilate _ ?_ _
-    simp [crAnStatesToCreateAnnihilate]
+    rw [anPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
+    exact normalOrder_mul_annihilate _ rfl _
  | .posAsymp φ =>
-    dsimp only [anPart, StateAlgebra.ofState]
-    simp only [FreeAlgebra.lift_ι_apply]
-    refine normalOrder_mul_annihilate _ ?_ _
-    simp [crAnStatesToCreateAnnihilate]
+    rw [anPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
+    refine normalOrder_mul_annihilate _ rfl _

 /-!

@ -151,9 +132,7 @@ lemma normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList (φc φa : 𝓕.Cr
    normalOrder (ofCrAnList φs' * ofCrAnState φa * ofCrAnState φc * ofCrAnList φs) := by
  rw [mul_assoc, mul_assoc, ← ofCrAnList_cons, ← ofCrAnList_cons, ← ofCrAnList_append]
  rw [normalOrder_ofCrAnList, normalOrderSign_swap_create_annihlate φc φa hφc hφa]
-  rw [normalOrderList_swap_create_annihlate φc φa hφc hφa]
-  rw [← smul_smul, ← normalOrder_ofCrAnList]
-  congr
+  rw [normalOrderList_swap_create_annihlate φc φa hφc hφa, ← smul_smul, ← normalOrder_ofCrAnList]
  rw [ofCrAnList_append, ofCrAnList_cons, ofCrAnList_cons]
  noncomm_ring

@ -166,9 +145,7 @@ lemma normalOrder_swap_create_annihlate_ofCrAnList (φc φa : 𝓕.CrAnStates)
  change (normalOrder ∘ₗ mulLinearMap (ofCrAnList φs * ofCrAnState φc * ofCrAnState φa)) a =
    (smulLinearMap _ ∘ₗ normalOrder ∘ₗ
    mulLinearMap (ofCrAnList φs * ofCrAnState φa * ofCrAnState φc)) a
-  refine LinearMap.congr_fun ?h a
-  apply ofCrAnListBasis.ext
-  intro l
+  refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a
  simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList,
    LinearMap.coe_comp, Function.comp_apply, instCommGroup.eq_1]
  rw [normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList φc φa hφc hφa]
@ -184,26 +161,20 @@ lemma normalOrder_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
  change (normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φc * (ofCrAnState φa * b))) a =
    (smulLinearMap (𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa)) ∘ₗ
    normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φa * (ofCrAnState φc * b))) a
-  apply LinearMap.congr_fun
-  apply ofCrAnListBasis.ext
-  intro l
+  refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) _
  simp only [mulLinearMap, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
-    LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk, instCommGroup.eq_1]
-  repeat rw [← mul_assoc]
-  rw [normalOrder_swap_create_annihlate_ofCrAnList φc φa hφc hφa]
+    LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk, instCommGroup.eq_1, ← mul_assoc,
+      normalOrder_swap_create_annihlate_ofCrAnList φc φa hφc hφa]
  rfl

 lemma normalOrder_superCommute_create_annihilate (φc φa : 𝓕.CrAnStates)
    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
    (a b : 𝓕.CrAnAlgebra) :
    normalOrder (a * superCommute (ofCrAnState φc) (ofCrAnState φa) * b) = 0 := by
-  rw [superCommute_ofCrAnState_ofCrAnState]
-  simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc]
-  rw [mul_sub, sub_mul, map_sub, ← smul_mul_assoc]
-  rw [← mul_assoc, ← mul_assoc]
-  rw [normalOrder_swap_create_annihlate φc φa hφc hφa]
-  simp only [FieldStatistic.instCommGroup.eq_1, Algebra.mul_smul_comm, Algebra.smul_mul_assoc,
-    map_smul, sub_self]
+  simp only [superCommute_ofCrAnState_ofCrAnState, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+  rw [mul_sub, sub_mul, map_sub, ← smul_mul_assoc, ← mul_assoc, ← mul_assoc,
+    normalOrder_swap_create_annihlate φc φa hφc hφa]
+  simp

 lemma normalOrder_superCommute_annihilate_create (φc φa : 𝓕.CrAnStates)
    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
@ -212,8 +183,7 @@ lemma normalOrder_superCommute_annihilate_create (φc φa : 𝓕.CrAnStates)
  rw [superCommute_ofCrAnState_ofCrAnState_symm]
  simp only [instCommGroup.eq_1, neg_smul, mul_neg, Algebra.mul_smul_comm, neg_mul,
    Algebra.smul_mul_assoc, map_neg, map_smul, neg_eq_zero, smul_eq_zero]
-  apply Or.inr
-  exact normalOrder_superCommute_create_annihilate φc φa hφc hφa a b
+  exact Or.inr (normalOrder_superCommute_create_annihilate φc φa hφc hφa ..)

 lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
    normalOrder (a * (crPart (StateAlgebra.ofState φ)) * (anPart (StateAlgebra.ofState φ')) * b) =
@ -221,34 +191,28 @@ lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra
    normalOrder (a * (anPart (StateAlgebra.ofState φ')) *
      (crPart (StateAlgebra.ofState φ)) * b) := by
  match φ, φ' with
-  | _, .negAsymp φ' =>
-    simp
-  | .posAsymp φ, _ =>
-    simp
+  | _, .negAsymp φ' => simp
+  | .posAsymp φ, _ => simp
  | .position φ, .position φ' =>
    simp only [crPart_position, anPart_position, instCommGroup.eq_1]
    rw [normalOrder_swap_create_annihlate]
    simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
-    rfl
-    rfl
+    rfl; rfl
  | .negAsymp φ, .posAsymp φ' =>
    simp only [crPart_negAsymp, anPart_posAsymp, instCommGroup.eq_1]
    rw [normalOrder_swap_create_annihlate]
    simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
-    rfl
-    rfl
+    rfl; rfl
  | .negAsymp φ, .position φ' =>
    simp only [crPart_negAsymp, anPart_position, instCommGroup.eq_1]
    rw [normalOrder_swap_create_annihlate]
    simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
-    rfl
-    rfl
+    rfl; rfl
  | .position φ, .posAsymp φ' =>
    simp only [crPart_position, anPart_posAsymp, instCommGroup.eq_1]
    rw [normalOrder_swap_create_annihlate]
    simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
-    rfl
-    rfl
+    rfl; rfl

 /-!

@ -262,51 +226,45 @@ lemma normalOrder_swap_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra
    normalOrder (a * (anPart (StateAlgebra.ofState φ)) * (crPart (StateAlgebra.ofState φ')) * b) =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • normalOrder (a * (crPart (StateAlgebra.ofState φ')) *
      (anPart (StateAlgebra.ofState φ)) * b) := by
-  rw [normalOrder_swap_crPart_anPart]
-  rw [smul_smul, FieldStatistic.exchangeSign_symm, FieldStatistic.exchangeSign_mul_self]
-  simp
+  simp [normalOrder_swap_crPart_anPart, smul_smul]

 lemma normalOrder_superCommute_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
    normalOrder (a * superCommute
    (crPart (StateAlgebra.ofState φ)) (anPart (StateAlgebra.ofState φ')) * b) = 0 := by
  match φ, φ' with
-  | _, .negAsymp φ' =>
-    simp
-  | .posAsymp φ', _ =>
-    simp
+  | _, .negAsymp φ' => simp
+  | .posAsymp φ', _ => simp
  | .position φ, .position φ' =>
-    simp only [crPart_position, anPart_position]
-    refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _
+    rw [crPart_position, anPart_position]
+    exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..
  | .negAsymp φ, .posAsymp φ' =>
-    simp only [crPart_negAsymp, anPart_posAsymp]
-    refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _
+    rw [crPart_negAsymp, anPart_posAsymp]
+    exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..
  | .negAsymp φ, .position φ' =>
-    simp only [crPart_negAsymp, anPart_position]
-    refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _
+    rw [crPart_negAsymp, anPart_position]
+    exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..
  | .position φ, .posAsymp φ' =>
-    simp only [crPart_position, anPart_posAsymp]
-    refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _
+    rw [crPart_position, anPart_posAsymp]
+    exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..

 lemma normalOrder_superCommute_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
    normalOrder (a * superCommute
    (anPart (StateAlgebra.ofState φ)) (crPart (StateAlgebra.ofState φ')) * b) = 0 := by
  match φ, φ' with
-  | .negAsymp φ', _ =>
-    simp
-  | _, .posAsymp φ' =>
-    simp
+  | .negAsymp φ', _ => simp
+  | _, .posAsymp φ' => simp
  | .position φ, .position φ' =>
-    simp only [anPart_position, crPart_position]
-    refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _
+    rw [anPart_position, crPart_position]
+    exact normalOrder_superCommute_annihilate_create _ _ rfl rfl ..
  | .posAsymp φ', .negAsymp φ =>
    simp only [anPart_posAsymp, crPart_negAsymp]
-    refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _
+    exact normalOrder_superCommute_annihilate_create _ _ rfl rfl ..
  | .position φ', .negAsymp φ =>
    simp only [anPart_position, crPart_negAsymp]
-    refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _
+    exact normalOrder_superCommute_annihilate_create _ _ rfl rfl ..
  | .posAsymp φ, .position φ' =>
    simp only [anPart_posAsymp, crPart_position]
-    refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _
+    exact normalOrder_superCommute_annihilate_create _ _ rfl rfl ..

 /-!

@ -359,8 +317,7 @@ lemma normalOrder_ofState_mul_ofState (φ φ' : 𝓕.States) :
    (crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ)) +
    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') +
    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') := by
-  rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart]
-  rw [mul_add, add_mul, add_mul]
+  rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart, mul_add, add_mul, add_mul]
  simp only [map_add, normalOrder_crPart_mul_crPart, normalOrder_anPart_mul_crPart,
    instCommGroup.eq_1, normalOrder_crPart_mul_anPart, normalOrder_anPart_mul_anPart]
  abel
@ -381,17 +338,14 @@ lemma normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
      normalOrderSign (φs ++ φc' :: φc :: φs') •
    (ofCrAnList (createFilter φs) * superCommute (ofCrAnState φc) (ofCrAnState φc') *
      ofCrAnList (createFilter φs') * ofCrAnList (annihilateFilter (φs ++ φs'))) := by
-  rw [superCommute_ofCrAnState_ofCrAnState]
-  rw [mul_sub, sub_mul, map_sub]
+  rw [superCommute_ofCrAnState_ofCrAnState, mul_sub, sub_mul, map_sub]
  conv_lhs =>
-    lhs
-    rhs
+    lhs; rhs
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, ← ofCrAnList_append, ← ofCrAnList_append,
      ← ofCrAnList_append]
  conv_lhs =>
    lhs
-    rw [normalOrder_ofCrAnList]
-    rw [normalOrderList_eq_createFilter_append_annihilateFilter]
+    rw [normalOrder_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
    rw [createFilter_append, createFilter_append, createFilter_append,
      createFilter_singleton_create _ hφc, createFilter_singleton_create _ hφc']
    rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append,
@ -401,10 +355,8 @@ lemma normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
      instCommGroup.eq_1, Algebra.smul_mul_assoc, Algebra.mul_smul_comm, map_smul]
    rw [← annihilateFilter_append]
  conv_lhs =>
-    rhs
-    rhs
-    rw [smul_mul_assoc]
-    rw [Algebra.mul_smul_comm, smul_mul_assoc]
+    rhs; rhs
+    rw [smul_mul_assoc, Algebra.mul_smul_comm, smul_mul_assoc]
    rhs
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, ← ofCrAnList_append, ← ofCrAnList_append,
      ← ofCrAnList_append]
@ -412,8 +364,7 @@ lemma normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
    rhs
    rw [map_smul]
    rhs
-    rw [normalOrder_ofCrAnList]
-    rw [normalOrderList_eq_createFilter_append_annihilateFilter]
+    rw [normalOrder_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
    rw [createFilter_append, createFilter_append, createFilter_append,
      createFilter_singleton_create _ hφc, createFilter_singleton_create _ hφc']
    rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append,
@ -423,25 +374,20 @@ lemma normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
      List.append_nil, Algebra.smul_mul_assoc]
    rw [← annihilateFilter_append]
  conv_lhs =>
-    lhs
-    lhs
+    lhs; lhs
    simp
  conv_lhs =>
-    rhs
-    rhs
-    lhs
+    rhs; rhs; lhs
    simp
  rw [normalOrderSign_swap_create_create φc φc' hφc hφc']
  rw [smul_smul, mul_comm, ← smul_smul]
  rw [← smul_sub, ofCrAnList_append, ofCrAnList_append, ofCrAnList_append]
  conv_lhs =>
-    rhs
-    rhs
+    rhs; rhs
    rw [ofCrAnList_append, ofCrAnList_append, ofCrAnList_append]
    rw [← smul_mul_assoc, ← smul_mul_assoc, ← Algebra.mul_smul_comm]
-  rw [← sub_mul, ← sub_mul, ← mul_sub]
-  congr
-  rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton]
+  rw [← sub_mul, ← sub_mul, ← mul_sub, ofCrAnList_append, ofCrAnList_singleton,
+    ofCrAnList_singleton]
  rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton, smul_mul_assoc]

 lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
@ -455,17 +401,14 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
    (ofCrAnList (createFilter (φs ++ φs'))
      * ofCrAnList (annihilateFilter φs) * superCommute (ofCrAnState φa) (ofCrAnState φa')
      * ofCrAnList (annihilateFilter φs')) := by
-  rw [superCommute_ofCrAnState_ofCrAnState]
-  rw [mul_sub, sub_mul, map_sub]
+  rw [superCommute_ofCrAnState_ofCrAnState, mul_sub, sub_mul, map_sub]
  conv_lhs =>
-    lhs
-    rhs
+    lhs; rhs
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, ← ofCrAnList_append, ← ofCrAnList_append,
      ← ofCrAnList_append]
  conv_lhs =>
    lhs
-    rw [normalOrder_ofCrAnList]
-    rw [normalOrderList_eq_createFilter_append_annihilateFilter]
+    rw [normalOrder_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
    rw [createFilter_append, createFilter_append, createFilter_append,
      createFilter_singleton_annihilate _ hφa, createFilter_singleton_annihilate _ hφa']
    rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append,
@ -475,8 +418,7 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
      instCommGroup.eq_1, Algebra.smul_mul_assoc, Algebra.mul_smul_comm, map_smul]
    rw [← createFilter_append]
  conv_lhs =>
-    rhs
-    rhs
+    rhs; rhs
    rw [smul_mul_assoc]
    rw [Algebra.mul_smul_comm, smul_mul_assoc]
    rhs
@ -486,8 +428,7 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
    rhs
    rw [map_smul]
    rhs
-    rw [normalOrder_ofCrAnList]
-    rw [normalOrderList_eq_createFilter_append_annihilateFilter]
+    rw [normalOrder_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
    rw [createFilter_append, createFilter_append, createFilter_append,
      createFilter_singleton_annihilate _ hφa, createFilter_singleton_annihilate _ hφa']
    rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append,
@ -497,20 +438,16 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
      List.append_nil, Algebra.smul_mul_assoc]
    rw [← createFilter_append]
  conv_lhs =>
-    lhs
-    lhs
+    lhs; lhs
    simp
  conv_lhs =>
-    rhs
-    rhs
-    lhs
+    rhs; rhs; lhs
    simp
  rw [normalOrderSign_swap_annihilate_annihilate φa φa' hφa hφa']
  rw [smul_smul, mul_comm, ← smul_smul]
  rw [← smul_sub, ofCrAnList_append, ofCrAnList_append, ofCrAnList_append]
  conv_lhs =>
-    rhs
-    rhs
+    rhs; rhs
    rw [ofCrAnList_append, ofCrAnList_append, ofCrAnList_append]
    rw [← Algebra.mul_smul_comm, ← smul_mul_assoc, ← Algebra.mul_smul_comm]
  rw [← mul_sub, ← sub_mul, ← mul_sub]
@ -519,7 +456,6 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
  apply congrArg
  rw [mul_assoc]
  apply congrArg
-  congr
  rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton]
  rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton, smul_mul_assoc]

@ -558,16 +494,14 @@ lemma ofCrAnList_mul_normalOrder_ofStateList_eq_superCommute (φs : List 𝓕.Cr
    ofCrAnList φs * normalOrder (ofStateList φs') =
    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • normalOrder (ofStateList φs') * ofCrAnList φs
    + ⟨ofCrAnList φs, normalOrder (ofStateList φs')⟩ₛca := by
-  rw [ofCrAnList_superCommute_normalOrder_ofStateList]
-  simp
+  simp [ofCrAnList_superCommute_normalOrder_ofStateList]

 lemma ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute (φ : 𝓕.CrAnStates)
    (φs' : List 𝓕.States) :
    ofCrAnState φ * normalOrder (ofStateList φs') =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • normalOrder (ofStateList φs') * ofCrAnState φ
    + ⟨ofCrAnState φ, normalOrder (ofStateList φs')⟩ₛca := by
-  rw [← ofCrAnList_singleton, ofCrAnList_mul_normalOrder_ofStateList_eq_superCommute]
-  simp [ofCrAnList_singleton]
+  simp [← ofCrAnList_singleton, ofCrAnList_mul_normalOrder_ofStateList_eq_superCommute]

 lemma anPart_mul_normalOrder_ofStateList_eq_superCommute (φ : 𝓕.States)
    (φs' : List 𝓕.States) :
@ -576,16 +510,9 @@ lemma anPart_mul_normalOrder_ofStateList_eq_superCommute (φ : 𝓕.States)
    + ⟨anPart (StateAlgebra.ofState φ), normalOrder (ofStateList φs')⟩ₛca := by
  rw [normalOrder_mul_anPart]
  match φ with
-  | .negAsymp φ =>
-    simp
-  | .position φ =>
-    simp only [anPart_position, instCommGroup.eq_1]
-    rw [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute]
-    simp [crAnStatistics]
-  | .posAsymp φ =>
-    simp only [anPart_posAsymp, instCommGroup.eq_1]
-    rw [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute]
-    simp [crAnStatistics]
+  | .negAsymp φ => simp
+  | .position φ => simp [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute, crAnStatistics]
+  | .posAsymp φ => simp [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute, crAnStatistics]

 end

--- a/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
@ -69,19 +69,14 @@ lemma koszulSignInsert_create (φ : 𝓕.CrAnStates)
 lemma normalOrderSign_cons_create (φ : 𝓕.CrAnStates)
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnStates) :
    normalOrderSign (φ :: φs) = normalOrderSign φs := by
-  dsimp only [normalOrderSign, Wick.koszulSign]
-  rw [koszulSignInsert_create φ hφ φs]
-  simp
+  simp [normalOrderSign, Wick.koszulSign, koszulSignInsert_create φ hφ φs]

@[simp]
-lemma normalOrderSign_singleton (φ : 𝓕.CrAnStates) :
-    normalOrderSign [φ] = 1 := by
+lemma normalOrderSign_singleton (φ : 𝓕.CrAnStates) : normalOrderSign [φ] = 1 := by
  simp [normalOrderSign]

@[simp]
-lemma normalOrderSign_nil :
-    normalOrderSign (𝓕 := 𝓕) [] = 1 := by
-  simp [normalOrderSign, Wick.koszulSign]
+lemma normalOrderSign_nil : normalOrderSign (𝓕 := 𝓕) [] = 1 := rfl

 lemma koszulSignInsert_append_annihilate (φ' φ : 𝓕.CrAnStates)
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) :
@ -139,10 +134,8 @@ lemma normalOrderSign_swap_create_annihlate_fst (φc φa : 𝓕.CrAnStates)

 lemma koszulSignInsert_swap (φ φc φa : 𝓕.CrAnStates) (φs φs' : List 𝓕.CrAnStates) :
    Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φa :: φc :: φs')
-    = Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φc :: φa :: φs') := by
-  apply Wick.koszulSignInsert_eq_perm
-  refine List.Perm.append_left φs ?h.a
-  exact List.Perm.swap φc φa φs'
+    = Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φc :: φa :: φs') :=
+  Wick.koszulSignInsert_eq_perm _ _ _ _ _ (List.Perm.append_left φs (List.Perm.swap φc φa φs'))

 lemma normalOrderSign_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate) :
@ -157,12 +150,9 @@ lemma normalOrderSign_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
    rw [← mul_assoc, mul_comm _ (FieldStatistic.exchangeSign _ _), mul_assoc]
    simp only [FieldStatistic.instCommGroup.eq_1, mul_eq_mul_left_iff]
    apply Or.inl
-    conv_rhs =>
-      rw [normalOrderSign]
-      dsimp [Wick.koszulSign]
-      rw [← normalOrderSign]
+    conv_rhs => rw [normalOrderSign, Wick.koszulSign, ← normalOrderSign]
    simp only [mul_eq_mul_right_iff]
-    apply Or.inl
+    left
    rw [koszulSignInsert_swap]

 lemma normalOrderSign_swap_create_create_fst (φc φc' : 𝓕.CrAnStates)
--- a/HepLean/PerturbationTheory/WickContraction/Insert.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Insert.lean
@ -200,7 +200,7 @@ lemma mem_uncontracted_insert_none_iff (c : WickContraction n) (i : Fin n.succ)
  · simp only [Nat.succ_eq_add_one, ← Fin.exists_succAbove_eq_iff] at hi
    obtain ⟨z, hk⟩ := hi
    subst hk
-    have hn : ¬ i.succAbove z = i := by exact Fin.succAbove_ne i z
+    have hn : ¬ i.succAbove z = i := Fin.succAbove_ne i z
    simp only [Nat.succ_eq_add_one, insert_succAbove_mem_uncontracted_iff, hn, false_or]
    apply Iff.intro
    · intro h
--- a/HepLean/PerturbationTheory/WickContraction/InsertList.lean
+++ b/HepLean/PerturbationTheory/WickContraction/InsertList.lean
@ -77,7 +77,7 @@ lemma insertList_fstFieldOfContract_some_incl (φ : 𝓕.States) (φs : List
    · simp [congrLift]
    · rw [Fin.lt_def] at h ⊢
      simp_all only [Nat.succ_eq_add_one, Fin.val_fin_lt, not_lt, finCongr_apply, Fin.coe_cast]
-      have hi : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
+      have hi : i.succAbove j ≠ i := Fin.succAbove_ne i j
      omega

 /-!
@ -188,7 +188,7 @@ lemma insertList_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : List
    · simp [congrLift]
    · rw [Fin.lt_def] at h ⊢
      simp_all only [Nat.succ_eq_add_one, Fin.val_fin_lt, not_lt, finCongr_apply, Fin.coe_cast]
-      have hi : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
+      have hi : i.succAbove j ≠ i := Fin.succAbove_ne i j
      omega

 lemma insertList_none_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.States)
--- a/HepLean/PerturbationTheory/WickContraction/Sign.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Sign.lean
@ -240,7 +240,7 @@ lemma signFinset_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States)
        simp_all only [and_true, Finset.mem_insert]
        rw [succAbove_mem_insertListLiftFinset]
        simp only [Fin.ext_iff, Fin.coe_cast]
-        have h1 : ¬ (i.succAbove ↑j) = i := by exact Fin.succAbove_ne i ↑j
+        have h1 : ¬ (i.succAbove ↑j) = i := Fin.succAbove_ne i ↑j
        simp only [Fin.val_eq_val, h1, signFinset, Finset.mem_filter, Finset.mem_univ, true_and,
          false_or]
        rw [Fin.succAbove_lt_succAbove_iff, Fin.succAbove_lt_succAbove_iff]
@ -284,7 +284,7 @@ lemma signFinset_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States)
          intro h
          simp only [Fin.ext_iff, Fin.coe_cast] at h
          simp only [Fin.val_eq_val] at h
-          have hn : ¬ i.succAbove k = i := by exact Fin.succAbove_ne i k
+          have hn : ¬ i.succAbove k = i := Fin.succAbove_ne i k
          exact False.elim (hn h)
        · split
          simp only [Nat.succ_eq_add_one, finCongr_apply, Finset.mem_erase, ne_eq,
@ -807,7 +807,7 @@ lemma stat_signFinset_insert_some_self_fst
        obtain ⟨y, hy1, hy2⟩ := h
        simp only [Fin.ext_iff, Fin.coe_cast] at hy2
        simp only [Fin.val_eq_val] at hy2
-        rw [Function.Injective.eq_iff (by exact Fin.succAbove_right_injective)] at hy2
+        rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at hy2
        subst hy2
        simp only [hy1, true_and]
        apply And.intro
@ -885,7 +885,7 @@ lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.S
        obtain ⟨y, hy1, hy2⟩ := h
        simp only [Fin.ext_iff, Fin.coe_cast] at hy2
        simp only [Fin.val_eq_val] at hy2
-        rw [Function.Injective.eq_iff (by exact Fin.succAbove_right_injective)] at hy2
+        rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at hy2
        subst hy2
        simp only [hy1, true_and]
        apply And.intro
@ -965,13 +965,13 @@ lemma signInsertSome_mul_filter_contracted_of_lt (φ : 𝓕.States) (φs : List
        · exact h1'
  · /- The `(c.getDual? i).isSome` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
    intro j hj
-    have hn : ¬ c.getDual? j = none := by exact Option.isSome_iff_ne_none.mp hj
+    have hn : ¬ c.getDual? j = none := Option.isSome_iff_ne_none.mp hj
    simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,
      hn, hj, forall_true_left, false_or, true_and, and_false, false_and, Finset.mem_inter,
      not_false_eq_true, and_true, not_and, not_lt, getDual?_getDual?_get_get, reduceCtorEq,
      Option.isSome_some, Option.get_some, forall_const, and_imp]
    intro h1 h2
-    have hijsucc' : i.succAbove ((c.getDual? j).get hj) ≠ i := by exact Fin.succAbove_ne i _
+    have hijsucc' : i.succAbove ((c.getDual? j).get hj) ≠ i := Fin.succAbove_ne i _
    have hkneqj : ↑k ≠ j := by
      by_contra hkj
      have hk := k.prop
@ -1025,7 +1025,7 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.States) (φs : L
    signInsertSome φ φs c i k *
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, c.uncontracted.filter (fun x => x < ↑k)⟩)
    = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, Finset.univ.filter (fun x => i.succAbove x < i)⟩) := by
-  have hik : i.succAbove ↑k ≠ i := by exact Fin.succAbove_ne i ↑k
+  have hik : i.succAbove ↑k ≠ i := Fin.succAbove_ne i ↑k
  rw [signInsertSome, signInsertSomeProd_eq_finset (hφj := hg.2) (hg := hg.1),
    signInsertSomeCoef_eq_finset (hφj := hg.2), if_pos (by omega), ← map_mul, ← map_mul]
  congr 1
@ -1036,7 +1036,7 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.States) (φs : L
  apply stat_ofFinset_eq_one_of_gradingCompliant _ _ _ hg.1
  · /- The `c.getDual? i = none` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
    intro j hj
-    have hijsucc : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
+    have hijsucc : i.succAbove j ≠ i := Fin.succAbove_ne i j
    simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,
      hj, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, and_true, true_and,
      and_false, or_false, Finset.mem_inter, not_false_eq_true, and_self, not_and, not_lt,
@ -1055,8 +1055,8 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.States) (φs : L
    omega
  · /- The `(c.getDual? i).isSome` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
    intro j hj
-    have hn : ¬ c.getDual? j = none := by exact Option.isSome_iff_ne_none.mp hj
-    have hijSuc : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
+    have hn : ¬ c.getDual? j = none := Option.isSome_iff_ne_none.mp hj
+    have hijSuc : i.succAbove j ≠ i := Fin.succAbove_ne i j
    have hkneqj : ↑k ≠ j := by
      by_contra hkj
      have hk := k.prop
--- a/HepLean/PerturbationTheory/WicksTheorem.lean
+++ b/HepLean/PerturbationTheory/WicksTheorem.lean
@ -173,7 +173,7 @@ lemma sign_timeContract_normalOrder_insertList_some (φ : 𝓕.States) (φs : Li
      congr 1
      exact signInsertSome_mul_filter_contracted_of_lt φ φs c i k hk hg
      · omega
-    · have hik : i.succAbove ↑k ≠ i := by exact Fin.succAbove_ne i ↑k
+    · have hik : i.succAbove ↑k ≠ i := Fin.succAbove_ne i ↑k
      rw [WickContraction.timeConract_insertList_some_eq_mul_contractStateAtIndex_lt]
      swap
      · exact hlt _