refactor: simp with simp only

HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean

@@ -38,7 +38,8 @@ lemma toSelfAdjointMatrix_apply (x : LorentzVector 3) : toSelfAdjointMatrix x =
     Basis.coe_mk, Fin.isValue]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℝ (s := Finset.univ)]
   · change (∑ i : Fin 1 ⊕ Fin 3, x i • PauliMatrix.σSAL' i) = _
-    simp [Fin.sum_univ_three, PauliMatrix.σSAL']
+    simp only [PauliMatrix.σSAL', Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
+      Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three]
     apply Subtype.ext
     simp only [Fin.isValue, AddSubgroup.coe_add, selfAdjoint.val_smul, smul_neg,
       AddSubgroupClass.coe_sub]
@@ -58,23 +59,29 @@ lemma toSelfAdjointMatrix_stdBasis (i : Fin 1 ⊕ Fin 3) :
   rw [toSelfAdjointMatrix_apply]
   match i with
   | Sum.inl 0 =>
-    simp [LorentzVector.stdBasis]
+    simp only [LorentzVector.stdBasis, Fin.isValue]
     erw [Pi.basisFun_apply]
     simp [PauliMatrix.σSAL, PauliMatrix.σSAL']
   | Sum.inr 0 =>
-    simp [LorentzVector.stdBasis]
+    simp only [LorentzVector.stdBasis, Fin.isValue]
     erw [Pi.basisFun_apply]
-    simp [PauliMatrix.σSAL, PauliMatrix.σSAL']
+    simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul,
+      Pi.single_eq_same, one_smul, zero_sub, Sum.inr.injEq, one_ne_zero, sub_zero, Fin.reduceEq,
+      PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL']
     refine Eq.symm (PauliMatrix.selfAdjoint_ext rfl rfl rfl rfl)
   | Sum.inr 1 =>
-    simp [LorentzVector.stdBasis]
+    simp only [LorentzVector.stdBasis, Fin.isValue]
     erw [Pi.basisFun_apply]
-    simp [PauliMatrix.σSAL, PauliMatrix.σSAL']
+    simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul,
+      Sum.inr.injEq, zero_ne_one, sub_self, Pi.single_eq_same, one_smul, zero_sub, Fin.reduceEq,
+      sub_zero, PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL']
     refine Eq.symm (PauliMatrix.selfAdjoint_ext rfl rfl rfl rfl)
   | Sum.inr 2 =>
-    simp [LorentzVector.stdBasis]
+    simp only [LorentzVector.stdBasis, Fin.isValue]
     erw [Pi.basisFun_apply]
-    simp [PauliMatrix.σSAL, PauliMatrix.σSAL']
+    simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul,
+      Sum.inr.injEq, Fin.reduceEq, sub_self, Pi.single_eq_same, one_smul, zero_sub,
+      PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL']
     refine Eq.symm (PauliMatrix.selfAdjoint_ext rfl rfl rfl rfl)
 
 @[simp]

HepLean/SpaceTime/LorentzVector/Complex/Basic.lean

@@ -99,7 +99,8 @@ lemma inclCongrRealLorentz_val (v : LorentzVector 3) :
 lemma complexContrBasis_of_real (i : Fin 1 ⊕ Fin 3) :
     (complexContrBasis i) = inclCongrRealLorentz (LorentzVector.stdBasis i) := by
   apply Lorentz.ContrℂModule.ext
-  simp [complexContrBasis, inclCongrRealLorentz, LorentzVector.stdBasis]
+  simp only [complexContrBasis, Basis.coe_ofEquivFun, inclCongrRealLorentz, LorentzVector.stdBasis,
+    LinearMap.coe_mk, AddHom.coe_mk]
   ext j
   simp only [Function.comp_apply, ofReal_eq_coe]
   erw [Pi.basisFun_apply]

HepLean/SpaceTime/PauliMatrices/SelfAdjoint.lean

@@ -48,9 +48,10 @@ lemma selfAdjoint_trace_σ1_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))
   have hA : IsSelfAdjoint A.1 := A.2
   rw [isSelfAdjoint_iff, star_eq_conjTranspose] at hA
   rw [eta_fin_two (A.1)ᴴ] at hA
-  simp at hA
+  simp only [Fin.isValue, conjTranspose_apply, RCLike.star_def] at hA
   have h01 := congrArg (fun f => f 0 1) hA
-  simp at h01
+  simp only [Fin.isValue, of_apply, cons_val', cons_val_one, head_cons, empty_val',
+    cons_val_fin_one, cons_val_zero] at h01
   rw [← h01]
   simp only [Fin.isValue, Complex.conj_re]
   rw [Complex.add_conj]
@@ -88,7 +89,7 @@ lemma selfAdjoint_trace_σ3_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))
     Equiv.symm_apply_apply, trace_fin_two_of, Complex.add_re, Complex.ofReal_add]
   have hA : IsSelfAdjoint A.1 := A.2
   rw [isSelfAdjoint_iff, star_eq_conjTranspose, eta_fin_two (A.1)ᴴ] at hA
-  simp at hA
+  simp only [Fin.isValue, conjTranspose_apply, RCLike.star_def] at hA
   have h00 := congrArg (fun f => f 0 0) hA
   have h11 := congrArg (fun f => f 1 1) hA
   have hA00 : A.1 0 0 = (A.1 0 0).re := Eq.symm ((fun {z} => Complex.conj_eq_iff_re.mp) h00)
@@ -110,9 +111,15 @@ lemma selfAdjoint_ext_complex {A B : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)}
   simp only [PauliMatrix.σ0, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons,
     head_cons, one_smul, tail_cons, zero_smul, empty_vecMul, add_zero, zero_add, empty_mul,
     Equiv.symm_apply_apply, trace_fin_two_of] at h0
-  simp [PauliMatrix.σ1] at h1
+  simp only [σ1, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons,
-  simp [PauliMatrix.σ2] at h2
+    zero_smul, tail_cons, one_smul, empty_vecMul, add_zero, zero_add, empty_mul,
-  simp [PauliMatrix.σ3] at h3
+    Equiv.symm_apply_apply, trace_fin_two_of] at h1
+  simp only [σ2, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons,
+    zero_smul, tail_cons, neg_smul, smul_cons, smul_eq_mul, smul_empty, neg_cons, neg_empty,
+    empty_vecMul, add_zero, zero_add, empty_mul, Equiv.symm_apply_apply, trace_fin_two_of] at h2
+  simp only [σ3, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons,
+    one_smul, tail_cons, zero_smul, empty_vecMul, add_zero, neg_smul, neg_cons, neg_empty, zero_add,
+    empty_mul, Equiv.symm_apply_apply, trace_fin_two_of] at h3
   match i, j with
   | 0, 0 =>
     linear_combination (norm := ring_nf) (h0 + h3) / 2
@@ -156,9 +163,10 @@ def σSA' (i : Fin 1 ⊕ Fin 3) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) :=
 lemma σSA_linearly_independent : LinearIndependent ℝ σSA' := by
   apply Fintype.linearIndependent_iff.mpr
   intro g hg
-  simp at hg
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton] at hg
   rw [Fin.sum_univ_three] at hg
-  simp [σSA'] at hg
+  simp only [Fin.isValue, σSA'] at hg
   intro i
   match i with
   | Sum.inl 0 =>
@@ -180,15 +188,32 @@ lemma σSA_span : ⊤ ≤ Submodule.span ℝ (Set.range σSA') := by
     | Sum.inr 1 => 1/2 * (Matrix.trace (σ2 * A.1)).re
     | Sum.inr 2 => 1/2 * (Matrix.trace (σ3 * A.1)).re
   use c
-  simp [Fin.sum_univ_three, c]
+  simp only [one_div, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three, c]
   apply selfAdjoint_ext
-  · simp [mul_add, σSA']
+  · simp only [σSA', AddSubgroup.coe_add, selfAdjoint.val_smul, mul_add, Algebra.mul_smul_comm,
+    trace_add, trace_smul, σ0_σ0_trace, real_smul, ofReal_mul, ofReal_inv, ofReal_ofNat,
+    σ0_σ1_trace, smul_zero, σ0_σ2_trace, add_zero, σ0_σ3_trace, mul_re, inv_re, re_ofNat,
+    normSq_ofNat, div_self_mul_self', ofReal_re, inv_im, im_ofNat, neg_zero, zero_div, ofReal_im,
+    mul_zero, sub_zero, mul_im, zero_mul]
     ring
-  · simp [mul_add, σSA']
+  · simp only [σSA', AddSubgroup.coe_add, selfAdjoint.val_smul, mul_add, Algebra.mul_smul_comm,
+    trace_add, trace_smul, σ1_σ0_trace, smul_zero, σ1_σ1_trace, real_smul, ofReal_mul, ofReal_inv,
+    ofReal_ofNat, σ1_σ2_trace, add_zero, σ1_σ3_trace, zero_add, mul_re, inv_re, re_ofNat,
+    normSq_ofNat, div_self_mul_self', ofReal_re, inv_im, im_ofNat, neg_zero, zero_div, ofReal_im,
+    mul_zero, sub_zero, mul_im, zero_mul]
     ring
-  · simp [mul_add, σSA']
+  · simp only [σSA', AddSubgroup.coe_add, selfAdjoint.val_smul, mul_add, Algebra.mul_smul_comm,
+    trace_add, trace_smul, σ2_σ0_trace, smul_zero, σ2_σ1_trace, σ2_σ2_trace, real_smul, ofReal_mul,
+    ofReal_inv, ofReal_ofNat, zero_add, σ2_σ3_trace, add_zero, mul_re, inv_re, re_ofNat,
+    normSq_ofNat, div_self_mul_self', ofReal_re, inv_im, im_ofNat, neg_zero, zero_div, ofReal_im,
+    mul_zero, sub_zero, mul_im, zero_mul]
     ring
-  · simp [mul_add, σSA']
+  · simp only [σSA', AddSubgroup.coe_add, selfAdjoint.val_smul, mul_add, Algebra.mul_smul_comm,
+    trace_add, trace_smul, σ3_σ0_trace, smul_zero, σ3_σ1_trace, σ3_σ2_trace, add_zero, σ3_σ3_trace,
+    real_smul, ofReal_mul, ofReal_inv, ofReal_ofNat, zero_add, mul_re, inv_re, re_ofNat,
+    normSq_ofNat, div_self_mul_self', ofReal_re, inv_im, im_ofNat, neg_zero, zero_div, ofReal_im,
+    mul_zero, sub_zero, mul_im, zero_mul]
     ring
 
 /-- The basis of `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` formed by Pauli matrices. -/
@@ -207,9 +232,10 @@ def σSAL' (i : Fin 1 ⊕ Fin 3) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) :=
 lemma σSAL_linearly_independent : LinearIndependent ℝ σSAL' := by
   apply Fintype.linearIndependent_iff.mpr
   intro g hg
-  simp at hg
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton] at hg
   rw [Fin.sum_univ_three] at hg
-  simp [σSAL'] at hg
+  simp only [Fin.isValue, σSAL'] at hg
   intro i
   match i with
   | Sum.inl 0 =>
@@ -231,15 +257,35 @@ lemma σSAL_span : ⊤ ≤ Submodule.span ℝ (Set.range σSAL') := by
     | Sum.inr 1 => - 1/2 * (Matrix.trace (σ2 * A.1)).re
     | Sum.inr 2 => - 1/2 * (Matrix.trace (σ3 * A.1)).re
   use c
-  simp [Fin.sum_univ_three, c]
+  simp only [one_div, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three, c]
   apply selfAdjoint_ext
-  · simp [mul_add, σSAL']
+  · simp only [σSAL', AddSubgroup.coe_add, selfAdjoint.val_smul, smul_neg, mul_add,
+    Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul, σ0_σ0_trace, real_smul, ofReal_mul,
+    ofReal_inv, ofReal_ofNat, trace_neg, σ0_σ1_trace, smul_zero, neg_zero, σ0_σ2_trace, add_zero,
+    σ0_σ3_trace, mul_re, inv_re, re_ofNat, normSq_ofNat, div_self_mul_self', ofReal_re, inv_im,
+    im_ofNat, zero_div, ofReal_im, mul_zero, sub_zero, mul_im, zero_mul]
     ring
-  · simp [mul_add, σSAL']
+  · simp only [σSAL', AddSubgroup.coe_add, selfAdjoint.val_smul, smul_neg, mul_add,
+    Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul, σ1_σ0_trace, smul_zero, trace_neg,
+    σ1_σ1_trace, real_smul, ofReal_mul, ofReal_div, ofReal_neg, ofReal_one, ofReal_ofNat,
+    σ1_σ2_trace, neg_zero, add_zero, σ1_σ3_trace, zero_add, neg_re, mul_re, div_ofNat_re, one_re,
+    ofReal_re, div_ofNat_im, neg_im, one_im, zero_div, ofReal_im, mul_zero, sub_zero, re_ofNat,
+    mul_im, zero_mul, im_ofNat]
     ring
-  · simp [mul_add, σSAL']
+  · simp only [σSAL', AddSubgroup.coe_add, selfAdjoint.val_smul, smul_neg, mul_add,
+    Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul, σ2_σ0_trace, smul_zero, trace_neg,
+    σ2_σ1_trace, neg_zero, σ2_σ2_trace, real_smul, ofReal_mul, ofReal_div, ofReal_neg, ofReal_one,
+    ofReal_ofNat, zero_add, σ2_σ3_trace, add_zero, neg_re, mul_re, div_ofNat_re, one_re, ofReal_re,
+    div_ofNat_im, neg_im, one_im, zero_div, ofReal_im, mul_zero, sub_zero, re_ofNat, mul_im,
+    zero_mul, im_ofNat]
     ring
-  · simp [mul_add, σSAL']
+  · simp only [σSAL', AddSubgroup.coe_add, selfAdjoint.val_smul, smul_neg, mul_add,
+    Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul, σ3_σ0_trace, smul_zero, trace_neg,
+    σ3_σ1_trace, neg_zero, σ3_σ2_trace, add_zero, σ3_σ3_trace, real_smul, ofReal_mul, ofReal_div,
+    ofReal_neg, ofReal_one, ofReal_ofNat, zero_add, neg_re, mul_re, div_ofNat_re, one_re, ofReal_re,
+    div_ofNat_im, neg_im, one_im, zero_div, ofReal_im, mul_zero, sub_zero, re_ofNat, mul_im,
+    zero_mul, im_ofNat]
     ring
 
 /-- The basis of `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` formed by Pauli matrices
@@ -253,22 +299,47 @@ lemma σSAL_decomp (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
     + (-1/2 * (Matrix.trace (σ2 * M.1)).re) • σSAL (Sum.inr 1)
     + (-1/2 * (Matrix.trace (σ3 * M.1)).re) • σSAL (Sum.inr 2) := by
   apply selfAdjoint_ext
-  · simp [σSAL, mul_add, σSAL']
+  · simp only [one_div, σSAL, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ0_σ0_trace, real_smul, ofReal_mul, ofReal_inv, ofReal_ofNat, trace_neg, σ0_σ1_trace, smul_zero,
+    neg_zero, add_zero, σ0_σ2_trace, σ0_σ3_trace, mul_re, inv_re, re_ofNat, normSq_ofNat,
+    div_self_mul_self', ofReal_re, inv_im, im_ofNat, zero_div, ofReal_im, mul_zero, sub_zero,
+    mul_im, zero_mul]
     ring
-  · simp [σSAL, mul_add, σSAL']
+  · simp only [one_div, σSAL, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ1_σ0_trace, smul_zero, trace_neg, σ1_σ1_trace, real_smul, ofReal_mul, ofReal_div, ofReal_neg,
+    ofReal_one, ofReal_ofNat, zero_add, σ1_σ2_trace, neg_zero, add_zero, σ1_σ3_trace, neg_re,
+    mul_re, div_ofNat_re, one_re, ofReal_re, div_ofNat_im, neg_im, one_im, zero_div, ofReal_im,
+    mul_zero, sub_zero, re_ofNat, mul_im, zero_mul, im_ofNat]
     ring
-  · simp [σSAL, mul_add, σSAL']
+  · simp only [one_div, σSAL, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ2_σ0_trace, smul_zero, trace_neg, σ2_σ1_trace, neg_zero, add_zero, σ2_σ2_trace, real_smul,
+    ofReal_mul, ofReal_div, ofReal_neg, ofReal_one, ofReal_ofNat, zero_add, σ2_σ3_trace, neg_re,
+    mul_re, div_ofNat_re, one_re, ofReal_re, div_ofNat_im, neg_im, one_im, zero_div, ofReal_im,
+    mul_zero, sub_zero, re_ofNat, mul_im, zero_mul, im_ofNat]
     ring
-  · simp [σSAL, mul_add, σSAL']
+  · simp only [one_div, σSAL, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ3_σ0_trace, smul_zero, trace_neg, σ3_σ1_trace, neg_zero, add_zero, σ3_σ2_trace, σ3_σ3_trace,
+    real_smul, ofReal_mul, ofReal_div, ofReal_neg, ofReal_one, ofReal_ofNat, zero_add, neg_re,
+    mul_re, div_ofNat_re, one_re, ofReal_re, div_ofNat_im, neg_im, one_im, zero_div, ofReal_im,
+    mul_zero, sub_zero, re_ofNat, mul_im, zero_mul, im_ofNat]
     ring
 
 @[simp]
 lemma σSAL_repr_inl_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
     σSAL.repr M (Sum.inl 0) = 1 / 2 * Matrix.trace (σ0 * M.1) := by
   have hM : M = ∑ i, σSAL.repr M i • σSAL i := (Basis.sum_repr σSAL M).symm
-  simp [Fin.sum_univ_three] at hM
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three] at hM
   have h0 := congrArg (fun A => Matrix.trace (σ0 * A.1)/ 2) hM
-  simp [σSAL, σSAL', mul_add] at h0
+  simp only [σSAL, Basis.mk_repr, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ0_σ0_trace, real_smul, trace_neg, σ0_σ1_trace, smul_zero, neg_zero, σ0_σ2_trace, add_zero,
+    σ0_σ3_trace, isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
+    IsUnit.mul_div_cancel_right] at h0
   linear_combination (norm := ring_nf) -h0
   simp [σSAL]
 
@@ -276,9 +347,14 @@ lemma σSAL_repr_inl_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
 lemma σSAL_repr_inr_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
     σSAL.repr M (Sum.inr 0) = - 1 / 2 * Matrix.trace (σ1 * M.1) := by
   have hM : M = ∑ i, σSAL.repr M i • σSAL i := (Basis.sum_repr σSAL M).symm
-  simp [Fin.sum_univ_three] at hM
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three] at hM
   have h0 := congrArg (fun A => - Matrix.trace (σ1 * A.1)/ 2) hM
-  simp [σSAL, σSAL', mul_add] at h0
+  simp only [σSAL, Basis.mk_repr, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ1_σ0_trace, smul_zero, trace_neg, σ1_σ1_trace, real_smul, σ1_σ2_trace, neg_zero, add_zero,
+    σ1_σ3_trace, zero_add, neg_neg, isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero,
+    not_false_eq_true, IsUnit.mul_div_cancel_right] at h0
   linear_combination (norm := ring_nf) -h0
   simp [σSAL]
 
@@ -286,9 +362,14 @@ lemma σSAL_repr_inr_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
 lemma σSAL_repr_inr_1 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
     σSAL.repr M (Sum.inr 1) = - 1 / 2 * Matrix.trace (σ2 * M.1) := by
   have hM : M = ∑ i, σSAL.repr M i • σSAL i := (Basis.sum_repr σSAL M).symm
-  simp [Fin.sum_univ_three] at hM
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three] at hM
   have h0 := congrArg (fun A => - Matrix.trace (σ2 * A.1)/ 2) hM
-  simp [σSAL, σSAL', mul_add] at h0
+  simp only [σSAL, Basis.mk_repr, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ2_σ0_trace, smul_zero, trace_neg, σ2_σ1_trace, neg_zero, σ2_σ2_trace, real_smul, zero_add,
+    σ2_σ3_trace, add_zero, neg_neg, isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero,
+    not_false_eq_true, IsUnit.mul_div_cancel_right] at h0
   linear_combination (norm := ring_nf) -h0
   simp [σSAL]
 
@@ -296,7 +377,8 @@ lemma σSAL_repr_inr_1 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
 lemma σSAL_repr_inr_2 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
     σSAL.repr M (Sum.inr 2) = - 1 / 2 * Matrix.trace (σ3 * M.1) := by
   have hM : M = ∑ i, σSAL.repr M i • σSAL i := (Basis.sum_repr σSAL M).symm
-  simp [Fin.sum_univ_three] at hM
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three] at hM
   have h0 := congrArg (fun A => - Matrix.trace (σ3 * A.1)/ 2) hM
   simp [σSAL, σSAL', mul_add] at h0
   linear_combination (norm := ring_nf) -h0
@@ -308,7 +390,8 @@ lemma σSA_minkowskiMetric_σSAL (i : Fin 1 ⊕ Fin 3) :
   | Sum.inl 0 =>
     simp [σSA, σSAL, σSA', σSAL', minkowskiMatrix.inl_0_inl_0]
   | Sum.inr 0 =>
-    simp [σSA, σSAL, σSA', σSAL', minkowskiMatrix.inr_i_inr_i]
+    simp only [σSA, Fin.isValue, Basis.coe_mk, σSA', minkowskiMatrix.inr_i_inr_i, σSAL, σSAL',
+      neg_smul, one_smul]
     cases i with
     | inl val =>
       ext i j : 2
@@ -317,7 +400,8 @@ lemma σSA_minkowskiMetric_σSAL (i : Fin 1 ⊕ Fin 3) :
       ext i j : 2
       simp_all only [NegMemClass.coe_neg, neg_apply, neg_neg]
   | Sum.inr 1 =>
-    simp [σSA, σSAL, σSA', σSAL', minkowskiMatrix.inr_i_inr_i]
+    simp only [σSA, Fin.isValue, Basis.coe_mk, σSA', minkowskiMatrix.inr_i_inr_i, σSAL, σSAL',
+      neg_smul, one_smul]
     cases i with
     | inl val =>
       ext i j : 2
@@ -326,7 +410,8 @@ lemma σSA_minkowskiMetric_σSAL (i : Fin 1 ⊕ Fin 3) :
       ext i j : 2
       simp_all only [NegMemClass.coe_neg, neg_apply, neg_neg]
   | Sum.inr 2 =>
-    simp [σSA, σSAL, σSA', σSAL', minkowskiMatrix.inr_i_inr_i]
+    simp only [σSA, Fin.isValue, Basis.coe_mk, σSA', minkowskiMatrix.inr_i_inr_i, σSAL, σSAL',
+      neg_smul, one_smul]
     cases i with
     | inl val =>
       ext i j : 2

HepLean/SpaceTime/SL2C/Basic.lean

@@ -145,7 +145,7 @@ lemma toLorentzGroup_eq_stdBasis (M : SL(2, ℂ)) :
 
 lemma repLorentzVector_apply_eq_mulVec (v : LorentzVector 3) :
     SL2C.repLorentzVector M v = (SL2C.toLorentzGroup M).1 *ᵥ v := by
-  simp [toLorentzGroup]
+  simp only [toLorentzGroup, MonoidHom.coe_mk, OneHom.coe_mk, toLorentzGroupElem_coe]
   have hv : v = (Finsupp.linearEquivFunOnFinite ℝ ℝ (Fin 1 ⊕ Fin 3))
     (LorentzVector.stdBasis.repr v) := by rfl
   nth_rewrite 2 [hv]