diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
index 7b6987e4..da54c988 100644
--- 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
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
index ac9e7bda..99212110 100644
--- 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 ?_)
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
index e37adccf..266d0914 100644
--- 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 ?_)
diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
index c326d1d7..cc7d7921 100644
--- 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 `Φ₁`. -/
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
index 5bf79a20..ef7be79a 100644
--- 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]
diff --git a/HepLean/Lorentz/Group/Boosts.lean b/HepLean/Lorentz/Group/Boosts.lean
index 870ada66..29e2eab1 100644
--- 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
diff --git a/HepLean/Mathematics/Fin/Involutions.lean b/HepLean/Mathematics/Fin/Involutions.lean
index 82f7f5bd..84567176 100644
--- 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 }
 
 /-!
 
diff --git a/HepLean/Mathematics/List.lean b/HepLean/Mathematics/List.lean
index e14891bc..b4cd91c4 100644
--- 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
diff --git a/HepLean/Mathematics/List/InsertionSort.lean b/HepLean/Mathematics/List/InsertionSort.lean
index ad3da79b..471e6ba2 100644
--- 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
diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean
index 9922467d..588220cc 100644
--- 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
 
diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
index 3d85a377..ba4b1763 100644
--- 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
 
diff --git a/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean b/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
index 9bdacdf0..af4d0622 100644
--- 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)
diff --git a/HepLean/PerturbationTheory/WickContraction/Insert.lean b/HepLean/PerturbationTheory/WickContraction/Insert.lean
index f006b5f9..c4a9a267 100644
--- 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
diff --git a/HepLean/PerturbationTheory/WickContraction/InsertList.lean b/HepLean/PerturbationTheory/WickContraction/InsertList.lean
index 6cc7978e..4ffb7b4f 100644
--- 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)
diff --git a/HepLean/PerturbationTheory/WickContraction/Sign.lean b/HepLean/PerturbationTheory/WickContraction/Sign.lean
index 2c1091a8..6a49d39b 100644
--- 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
diff --git a/HepLean/PerturbationTheory/WicksTheorem.lean b/HepLean/PerturbationTheory/WicksTheorem.lean
index cdb4a119..0236ea23 100644
--- 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 _