From aea1e885617946f38ea4c5794f67c544263910de Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 16 Oct 2024 11:09:52 +0000 Subject: [PATCH] refactor: simp with simp only --- .../LorentzVector/AsSelfAdjointMatrix.lean | 23 ++- .../LorentzVector/Complex/Basic.lean | 3 +- .../SpaceTime/PauliMatrices/SelfAdjoint.lean | 153 ++++++++++++++---- HepLean/SpaceTime/SL2C/Basic.lean | 2 +- 4 files changed, 137 insertions(+), 44 deletions(-) diff --git a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean index c1b4405..82bec94 100644 --- a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean +++ b/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] diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean b/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean index 70185f6..46122d2 100644 --- a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean +++ b/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] diff --git a/HepLean/SpaceTime/PauliMatrices/SelfAdjoint.lean b/HepLean/SpaceTime/PauliMatrices/SelfAdjoint.lean index 82ba264..ce83562 100644 --- a/HepLean/SpaceTime/PauliMatrices/SelfAdjoint.lean +++ b/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 [PauliMatrix.σ2] at h2 - simp [PauliMatrix.σ3] at h3 + simp only [σ1, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons, + zero_smul, tail_cons, one_smul, empty_vecMul, add_zero, zero_add, empty_mul, + 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 diff --git a/HepLean/SpaceTime/SL2C/Basic.lean b/HepLean/SpaceTime/SL2C/Basic.lean index 7a95924..e7d2458 100644 --- a/HepLean/SpaceTime/SL2C/Basic.lean +++ b/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]