refactor: Some proof clean up

HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean

@@ -85,7 +85,6 @@ lemma δa₂_δ₁ (j : Fin n) : δa₂ j = δ₁ j.succ := by
   exact Nat.add_comm 1 ↑j
 
 lemma δa₂_δ!₁ (j : Fin n) : δa₂ j = δ!₁ j.castSucc := by
-  rw [Fin.ext_iff]
   rfl
 
 lemma δa₃_δ₃ : @δa₃ n = δ₃ := by

HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean

@@ -36,9 +36,7 @@ lemma exists_plane_exists_basis {n : ℕ} (hE : ExistsPlane n) :
   have h1 : ∑ x : Fin n, -(g (Sum.inr x) • Y (Sum.inr x)) =
       ∑ x : Fin n, (-g (Sum.inr x)) • Y (Sum.inr x) := by
     apply Finset.sum_congr
-    simp only
-    intro i _
-    simp
+    rfl
   rw [h1] at hg
   have h2 : ∑ a₁ : Fin 11, g (Sum.inl a₁) • Y (Sum.inl a₁) = 0 := by
     apply hB2

HepLean/SpaceTime/LorentzVector/Modules.lean

@@ -55,7 +55,7 @@ lemma ext (ψ ψ' : ContrℂModule) (h : ψ.val = ψ'.val) : ψ = ψ' := by
   cases ψ
   cases ψ'
   subst h
-  simp_all only
+  rfl
 
 @[simp]
 lemma val_add (ψ ψ' : ContrℂModule) : (ψ + ψ').val = ψ.val + ψ'.val := rfl

HepLean/SpaceTime/MinkowskiMetric.lean

@@ -83,7 +83,6 @@ lemma off_diag_zero {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) : η μ ν = 0 :=
   exact diagonal_apply_ne _ h
 
 lemma inl_0_inl_0 : @minkowskiMatrix d (Sum.inl 0) (Sum.inl 0) = 1 := by
-  simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
   rfl
 
 lemma inr_i_inr_i (i : Fin d) : @minkowskiMatrix d (Sum.inr i) (Sum.inr i) = -1 := by