refactor: Lint

HepLean.lean

@@ -109,7 +109,10 @@ import HepLean.StandardModel.HiggsBoson.Potential
 import HepLean.StandardModel.Representations
 import HepLean.Tensors.ComplexLorentz.Basic
 import HepLean.Tensors.ComplexLorentz.Basis
+import HepLean.Tensors.ComplexLorentz.BasisTrees
 import HepLean.Tensors.ComplexLorentz.Lemmas
+import HepLean.Tensors.ComplexLorentz.PauliContr
+import HepLean.Tensors.ComplexLorentz.PauliLower
 import HepLean.Tensors.OverColor.Basic
 import HepLean.Tensors.OverColor.Discrete
 import HepLean.Tensors.OverColor.Functors

HepLean/Tensors/ComplexLorentz/Basis.lean

@@ -79,6 +79,15 @@ lemma perm_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, LinearEquiv.ofLinear_apply]
   rw [basis_eq_FDiscrete]
 
+lemma perm_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
+    {c1 : Fin m → complexLorentzTensor.C} (σ : OverColor.mk c ⟶ OverColor.mk c1)
+    (b : Π j, Fin (complexLorentzTensor.repDim (c j))) :
+    (perm σ (tensorNode (basisVector c b))).tensor =
+    (tensorNode (basisVector c1 (fun i => Fin.cast (perm_basisVector_cast σ i)
+    (b ((OverColor.Hom.toEquiv σ).symm i))))).tensor := by
+  exact perm_basisVector _ _
+
+/-- The scalar determining if contracting two basis vectors together gives zero or not. -/
 def contrBasisVectorMul {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
     (i : Fin n.succ.succ) (j : Fin n.succ)
     (b : Π k, Fin (complexLorentzTensor.repDim (c k))) : ℂ :=
@@ -89,7 +98,7 @@ lemma contrBasisVectorMul_neg {n : ℕ} {c : Fin n.succ.succ → complexLorentzT
     (h : ¬ (b i).val = (b (i.succAbove j)).val := by decide) :
     contrBasisVectorMul i j b = 0 := by
   rw [contrBasisVectorMul]
-  simp
+  simp only [ite_eq_else, one_ne_zero, imp_false]
   exact h
 
 lemma contrBasisVectorMul_pos {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
@@ -97,7 +106,7 @@ lemma contrBasisVectorMul_pos {n : ℕ} {c : Fin n.succ.succ → complexLorentzT
     (h : (b i).val = (b (i.succAbove j)).val := by decide) :
     contrBasisVectorMul i j b = 1 := by
   rw [contrBasisVectorMul]
-  simp
+  simp only [ite_eq_then, zero_ne_one, imp_false, Decidable.not_not]
   exact h
 
 lemma contr_basisVector {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
@@ -119,37 +128,41 @@ lemma contr_basisVector {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.
   erw [basis_contr]
   rfl
 
-lemma contr_basisVector_tree  {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
+lemma contr_basisVector_tree {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
     {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)}
     (b : Π k, Fin (complexLorentzTensor.repDim (c k))) :
     (contr i j h (tensorNode (basisVector c b))).tensor =
-    (smul (contrBasisVectorMul i j b) (tensorNode ( basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
+    (smul (contrBasisVectorMul i j b) (tensorNode
-    (fun k => b (i.succAbove (j.succAbove k)))) )).tensor := by
+    (basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
+    (fun k => b (i.succAbove (j.succAbove k)))))).tensor := by
   exact contr_basisVector _
 
-lemma contr_basisVector_tree_pos  {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
+lemma contr_basisVector_tree_pos {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
     {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)}
-    (b : Π k, Fin (complexLorentzTensor.repDim (c k))) (hn : (b i).val = (b (i.succAbove j)).val := by decide) :
+    (b : Π k, Fin (complexLorentzTensor.repDim (c k)))
+    (hn : (b i).val = (b (i.succAbove j)).val := by decide) :
     (contr i j h (tensorNode (basisVector c b))).tensor =
-    ((tensorNode ( basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
+    ((tensorNode (basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
     (fun k => b (i.succAbove (j.succAbove k)))))).tensor := by
   rw [contr_basisVector_tree, contrBasisVectorMul]
   rw [if_pos hn]
   simp [smul_tensor]
 
-lemma contr_basisVector_tree_neg  {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
+lemma contr_basisVector_tree_neg {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
     {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)}
-    (b : Π k, Fin (complexLorentzTensor.repDim (c k))) (hn : ¬ (b i).val = (b (i.succAbove j)).val := by decide) :
+    (b : Π k, Fin (complexLorentzTensor.repDim (c k)))
+    (hn : ¬ (b i).val = (b (i.succAbove j)).val := by decide) :
     (contr i j h (tensorNode (basisVector c b))).tensor =
     (tensorNode 0).tensor := by
   rw [contr_basisVector_tree, contrBasisVectorMul]
   rw [if_neg hn]
-  simp [smul_tensor]
+  simp only [Nat.succ_eq_add_one, smul_tensor, tensorNode_tensor, zero_smul]
-
 
+/-- Equivalence of Fin types appearing in the product of two basis vectors. -/
 def prodBasisVecEquiv {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     {c1 : Fin m → complexLorentzTensor.C} (i : Fin n ⊕ Fin m) :
-    Sum.elim (fun i => Fin (complexLorentzTensor.repDim (c i))) (fun i => Fin (complexLorentzTensor.repDim (c1 i)))
+    Sum.elim (fun i => Fin (complexLorentzTensor.repDim (c i))) (fun i =>
+      Fin (complexLorentzTensor.repDim (c1 i)))
     i ≃ Fin (complexLorentzTensor.repDim ((Sum.elim c c1 i))) :=
   match i with
   | Sum.inl _ => Equiv.refl _
@@ -184,17 +197,17 @@ lemma prod_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
   | Sum.inl k => rfl
   | Sum.inr k => rfl
 
-lemma prod_basisVector_tree  {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
+lemma prod_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     {c1 : Fin m → complexLorentzTensor.C}
     (b : Π k, Fin (complexLorentzTensor.repDim (c k)))
     (b1 : Π k, Fin (complexLorentzTensor.repDim (c1 k))) :
-   (prod (tensorNode (basisVector c b)) (tensorNode (basisVector c1 b1))).tensor =
+    (prod (tensorNode (basisVector c b)) (tensorNode (basisVector c1 b1))).tensor =
     (tensorNode (basisVector (Sum.elim c c1 ∘ finSumFinEquiv.symm) (fun i =>
     prodBasisVecEquiv (finSumFinEquiv.symm i)
     ((HepLean.PiTensorProduct.elimPureTensor b b1) (finSumFinEquiv.symm i))))).tensor := by
   exact prod_basisVector _ _
 
-lemma eval_basisVector  {n : ℕ} {c : Fin n.succ → complexLorentzTensor.C}
+lemma eval_basisVector {n : ℕ} {c : Fin n.succ → complexLorentzTensor.C}
     {i : Fin n.succ} (j : Fin (complexLorentzTensor.repDim (c i)))
     (b : Π k, Fin (complexLorentzTensor.repDim (c k))) :
     (eval i j (tensorNode (basisVector c b))).tensor = (if j = b i then (1 : ℂ) else 0) •
@@ -282,7 +295,7 @@ lemma contrMatrix_basis_expand_tree : {Lorentz.contrMetric | μ ν}ᵀ.tensor =
   contrMatrix_basis_expand
 
 lemma leftMetric_expand : {Fermion.leftMetric | α β}ᵀ.tensor =
-   - basisVector ![Color.upL, Color.upL] (fun | 0 => 0 | 1 => 1)
+    - basisVector ![Color.upL, Color.upL] (fun | 0 => 0 | 1 => 1)
     + basisVector ![Color.upL, Color.upL] (fun | 0 => 1 | 1 => 0) := by
   simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
     Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue]
@@ -299,7 +312,8 @@ lemma leftMetric_expand : {Fermion.leftMetric | α β}ᵀ.tensor =
     · rfl
 
 lemma leftMetric_expand_tree : {Fermion.leftMetric | α β}ᵀ.tensor =
-    (TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.upL, Color.upL] (fun | 0 => 0 | 1 => 1)))) <|
+    (TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.upL, Color.upL]
+    (fun | 0 => 0 | 1 => 1)))) <|
     (tensorNode (basisVector ![Color.upL, Color.upL] (fun | 0 => 1 | 1 => 0)))).tensor :=
   leftMetric_expand
 
@@ -320,8 +334,10 @@ lemma altLeftMetric_expand : {Fermion.altLeftMetric | α β}ᵀ.tensor =
     · rfl
 
 lemma altLeftMetric_expand_tree : {Fermion.altLeftMetric | α β}ᵀ.tensor =
-    (TensorTree.add (tensorNode (basisVector ![Color.downL, Color.downL] (fun | 0 => 0 | 1 => 1))) <|
+    (TensorTree.add (tensorNode (basisVector ![Color.downL, Color.downL]
-    (smul (-1) (tensorNode (basisVector ![Color.downL, Color.downL] (fun | 0 => 1 | 1 => 0))))).tensor :=
+    (fun | 0 => 0 | 1 => 1))) <|
+    (smul (-1) (tensorNode (basisVector ![Color.downL, Color.downL]
+    (fun | 0 => 1 | 1 => 0))))).tensor :=
   altLeftMetric_expand
 
 lemma rightMetric_expand : {Fermion.rightMetric | α β}ᵀ.tensor =
@@ -342,7 +358,8 @@ lemma rightMetric_expand : {Fermion.rightMetric | α β}ᵀ.tensor =
     · rfl
 
 lemma rightMetric_expand_tree : {Fermion.rightMetric | α β}ᵀ.tensor =
-    (TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.upR, Color.upR] (fun | 0 => 0 | 1 => 1)))) <|
+    (TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.upR, Color.upR]
+    (fun | 0 => 0 | 1 => 1)))) <|
     (tensorNode (basisVector ![Color.upR, Color.upR] (fun | 0 => 1 | 1 => 0)))).tensor :=
   rightMetric_expand
 
@@ -363,8 +380,10 @@ lemma altRightMetric_expand : {Fermion.altRightMetric | α β}ᵀ.tensor =
     · rfl
 
 lemma altRightMetric_expand_tree : {Fermion.altRightMetric | α β}ᵀ.tensor =
-    (TensorTree.add (tensorNode (basisVector ![Color.downR, Color.downR] (fun | 0 => 0 | 1 => 1))) <|
+    (TensorTree.add (tensorNode (basisVector
-    (smul (-1) (tensorNode (basisVector ![Color.downR, Color.downR] (fun | 0 => 1 | 1 => 0))))).tensor :=
+    ![Color.downR, Color.downR] (fun | 0 => 0 | 1 => 1))) <|
+    (smul (-1) (tensorNode (basisVector ![Color.downR, Color.downR]
+    (fun | 0 => 1 | 1 => 0))))).tensor :=
   altRightMetric_expand
 
 /-- The expansion of the Pauli matrices `σ^μ^a^{dot a}` in terms of basis vectors. -/
@@ -406,13 +425,13 @@ lemma pauliMatrix_basis_expand : {PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
     | (2 : Fin 3) => rfl
 
 lemma pauliMatrix_basis_expand_tree : {PauliMatrix.asConsTensor | μ α β}ᵀ.tensor =
-   (TensorTree.add (tensorNode
+    (TensorTree.add (tensorNode
       (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 0 | 1 => 0 | 2 => 0))) <|
     TensorTree.add (tensorNode
       (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 0 | 1 => 1 | 2 => 1))) <|
     TensorTree.add (tensorNode
       (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 1 | 1 => 0 | 2 => 1))) <|
-   TensorTree.add (tensorNode
+    TensorTree.add (tensorNode
       (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 1 | 1 => 1 | 2 => 0))) <|
     TensorTree.add (smul (-I) (tensorNode
       (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 2 | 1 => 0 | 2 => 1)))) <|
@@ -421,7 +440,8 @@ lemma pauliMatrix_basis_expand_tree : {PauliMatrix.asConsTensor | μ α β}ᵀ.t
     TensorTree.add (tensorNode
       (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 3 | 1 => 0 | 2 => 0))) <|
     (smul (-1) (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 3 | 1 => 1 | 2 => 1))))).tensor := by
+      (basisVector ![Color.up, Color.upL, Color.upR]
+        (fun | 0 => 3 | 1 => 1 | 2 => 1))))).tensor := by
   rw [pauliMatrix_basis_expand]
   simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, add_tensor, tensorNode_tensor,
     smul_tensor, neg_smul, one_smul]

HepLean/Tensors/ComplexLorentz/BasisTrees.lean

@@ -0,0 +1,233 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Tensors.Tree.Elab
+import HepLean.Tensors.ComplexLorentz.Basic
+import Mathlib.LinearAlgebra.TensorProduct.Basis
+import HepLean.Tensors.Tree.NodeIdentities.Basic
+import HepLean.Tensors.Tree.NodeIdentities.PermProd
+import HepLean.Tensors.Tree.NodeIdentities.PermContr
+import HepLean.Tensors.Tree.NodeIdentities.ProdComm
+import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
+import HepLean.Tensors.Tree.NodeIdentities.ContrContr
+import HepLean.Tensors.ComplexLorentz.Basis
+/-!
+
+## Basis trees
+
+When contracting e.g. Pauli matrices with other tensors, it is sometimes convienent
+to rewrite the contraction in terms of a basis.
+
+The lemmas in this file allow us to do this.
+-/
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open IndexNotation
+open CategoryTheory
+open TensorTree
+open OverColor.Discrete
+
+noncomputable section
+
+namespace Fermion
+open complexLorentzTensor
+
+/-!
+
+## Tree expansions for Pauli matrices.
+
+-/
+
+/-- The map to colors one gets when contracting with Pauli matrices on the right. -/
+abbrev pauliMatrixContrMap {n : ℕ} (c : Fin n → complexLorentzTensor.C) :=
+  (Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm)
+
+lemma prod_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C}
+    (t : TensorTree complexLorentzTensor c) :
+    (TensorTree.prod t (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
+      PauliMatrix.asConsTensor)).tensor = (((t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 0 | 2 => 0)))).add
+    (((t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 1 | 2 => 1)))).add
+    (((t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 0 | 2 => 1)))).add
+    (((t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 1 | 2 => 0)))).add
+    ((TensorTree.smul (-I) ((t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 0 | 2 => 1))))).add
+    ((TensorTree.smul I ((t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 1 | 2 => 0))))).add
+    ((t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 3 | 1 => 0 | 2 => 0))).add
+    (TensorTree.smul (-1) (t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR]
+        fun | 0 => 3 | 1 => 1 | 2 => 1))))))))))).tensor := by
+  rw [prod_tensor_eq_snd <| pauliMatrix_basis_expand_tree]
+  rw [prod_add _ _ _]
+  rw [add_tensor_eq_snd <| prod_add _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    prod_add _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _]
+  /- Moving smuls. -/
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_fst <| prod_smul _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| prod_smul _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_snd<| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| prod_smul _ _ _]
+  rfl
+
+lemma contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C}
+    (t : TensorTree complexLorentzTensor c) (i : Fin (n + 3)) (j : Fin (n +2))
+    (h : (pauliMatrixContrMap c) (i.succAbove j) =
+      complexLorentzTensor.τ ((pauliMatrixContrMap c) i)) :
+    (contr i j h (TensorTree.prod t
+    (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
+      PauliMatrix.asConsTensor))).tensor =
+    ((contr i j h (t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 0 | 2 => 0)))).add
+    ((contr i j h (t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 1 | 2 => 1)))).add
+    ((contr i j h (t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 0 | 2 => 1)))).add
+    ((contr i j h (t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 1 | 2 => 0)))).add
+    ((TensorTree.smul (-I) (contr i j h (t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 0 | 2 => 1))))).add
+    ((TensorTree.smul I (contr i j h (t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 1 | 2 => 0))))).add
+    ((contr i j h (t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 3 | 1 => 0 | 2 => 0)))).add
+    (TensorTree.smul (-1) (contr i j h (t.prod (tensorNode
+      (basisVector ![Color.up, Color.upL, Color.upR]
+        fun | 0 => 3 | 1 => 1 | 2 => 1)))))))))))).tensor := by
+  rw [contr_tensor_eq <| prod_pauliMatrix_basis_tree_expand _]
+  /- Moving contr over add. -/
+  rw [contr_add]
+  rw [add_tensor_eq_snd <| contr_add _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| contr_add _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
+  /- Moving contr over smul. -/
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    contr_smul _ _]
+
+lemma basis_contr_pauliMatrix_basis_tree_expand' {n : ℕ} {c : Fin n → complexLorentzTensor.C}
+    (i : Fin (n + 3)) (j : Fin (n +2))
+    (h : (pauliMatrixContrMap c) (i.succAbove j) = complexLorentzTensor.τ
+      ((pauliMatrixContrMap c) i))
+    (b : Π k, Fin (complexLorentzTensor.repDim (c k))) :
+    let c' := Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ finSumFinEquiv.symm
+    let b' (i1 i2 i3 : Fin 4) := fun i => prodBasisVecEquiv (finSumFinEquiv.symm i)
+      ((HepLean.PiTensorProduct.elimPureTensor b (fun | 0 => i1 | 1 => i2 | 2 => i3))
+      (finSumFinEquiv.symm i))
+    (contr i j h (TensorTree.prod (tensorNode (basisVector c b))
+      (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
+    PauliMatrix.asConsTensor))).tensor = ((contr i j h ((tensorNode
+    (basisVector c' (b' 0 0 0))))).add
+    ((contr i j h ((tensorNode (basisVector c' (b' 0 1 1))))).add
+    ((contr i j h ((tensorNode (basisVector c' (b' 1 0 1))))).add
+    ((contr i j h ((tensorNode (basisVector c' (b' 1 1 0))))).add
+    ((TensorTree.smul (-I) (contr i j h ((tensorNode (basisVector c' (b' 2 0 1)))))).add
+    ((TensorTree.smul I (contr i j h ((tensorNode (basisVector c' (b' 2 1 0)))))).add
+    ((contr i j h ((tensorNode (basisVector c' (b' 3 0 0))))).add
+    (TensorTree.smul (-1) (contr i j h ((tensorNode
+      (basisVector c' (b' 3 1 1))))))))))))).tensor := by
+  rw [contr_pauliMatrix_basis_tree_expand]
+  /- Product of basis vectors . -/
+  rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
+    <| prod_basisVector_tree _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
+    <| contr_tensor_eq <| prod_basisVector_tree _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
+      <| prod_basisVector_tree _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
+    <| prod_basisVector_tree _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
+    <| contr_tensor_eq <| prod_basisVector_tree _ _]
+  rfl
+
+lemma basis_contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C}
+    (i : Fin (n + 3)) (j : Fin (n +2))
+    (h : (pauliMatrixContrMap c) (i.succAbove j) = complexLorentzTensor.τ
+      ((pauliMatrixContrMap c) i))
+    (b : Π k, Fin (complexLorentzTensor.repDim (c k))) :
+    let c' := (Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ finSumFinEquiv.symm)
+      ∘ Fin.succAbove i ∘ Fin.succAbove j
+    let b'' (i1 i2 i3 : Fin 4) : (i : Fin (n + (Nat.succ 0).succ.succ)) →
+        Fin (complexLorentzTensor.repDim (Sum.elim c ![Color.up, Color.upL, Color.upR]
+          (finSumFinEquiv.symm i))) := fun i => prodBasisVecEquiv (finSumFinEquiv.symm i)
+      ((HepLean.PiTensorProduct.elimPureTensor b (fun | (0 : Fin 3) => i1 | 1 => i2 | 2 => i3))
+      (finSumFinEquiv.symm i))
+    let b' (i1 i2 i3 : Fin 4) := fun k => (b'' i1 i2 i3) (i.succAbove (j.succAbove k))
+    (contr i j h (TensorTree.prod (tensorNode (basisVector c b))
+    (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
+    PauliMatrix.asConsTensor))).tensor = (((
+    TensorTree.smul (contrBasisVectorMul i j (b'' 0 0 0))
+      (tensorNode (basisVector c' (b' 0 0 0))))).add
+    (((TensorTree.smul (contrBasisVectorMul i j (b'' 0 1 1))
+      (tensorNode (basisVector c' (b' 0 1 1))))).add
+    (((TensorTree.smul (contrBasisVectorMul i j (b'' 1 0 1))
+      (tensorNode (basisVector c' (b' 1 0 1))))).add
+    (((TensorTree.smul (contrBasisVectorMul i j (b'' 1 1 0))
+      (tensorNode (basisVector c' (b' 1 1 0))))).add
+    ((TensorTree.smul (-I) ((TensorTree.smul (contrBasisVectorMul i j (b'' 2 0 1))
+      (tensorNode (basisVector c' (b' 2 0 1)))))).add
+    ((TensorTree.smul I ((TensorTree.smul (contrBasisVectorMul i j (b'' 2 1 0))
+      (tensorNode (basisVector c' (b' 2 1 0)))))).add
+    (((TensorTree.smul (contrBasisVectorMul i j (b'' 3 0 0))
+      (tensorNode (basisVector c' (b' 3 0 0))))).add
+    (TensorTree.smul (-1) ((TensorTree.smul (contrBasisVectorMul i j (b'' 3 1 1)) (tensorNode
+      (basisVector c' (b' 3 1 1))))))))))))).tensor := by
+  rw [basis_contr_pauliMatrix_basis_tree_expand']
+  /- Contracting basis vectors. -/
+  rw [add_tensor_eq_fst <| contr_basisVector_tree _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
+    <| contr_basisVector_tree _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_fst <| contr_basisVector_tree _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
+    <| contr_basisVector_tree _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    smul_tensor_eq <| contr_basisVector_tree _]
+
+end Fermion
+
+end

HepLean/Tensors/ComplexLorentz/Lemmas.lean

@@ -3,17 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.Tensors.Tree.Elab
+import HepLean.Tensors.ComplexLorentz.BasisTrees
-import HepLean.Tensors.ComplexLorentz.Basic
-import Mathlib.LinearAlgebra.TensorProduct.Basis
-import HepLean.Tensors.Tree.NodeIdentities.Basic
-import HepLean.Tensors.Tree.NodeIdentities.PermProd
-import HepLean.Tensors.Tree.NodeIdentities.PermContr
-import HepLean.Tensors.Tree.NodeIdentities.ProdComm
-import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
-import HepLean.Tensors.Tree.NodeIdentities.ContrContr
-import HepLean.Tensors.ComplexLorentz.Basis
-import LLMLean
 /-!
 
 ## Lemmas related to complex Lorentz tensors.
@@ -33,7 +23,7 @@ open OverColor.Discrete
 noncomputable section
 
 namespace Fermion
-
+open complexLorentzTensor
 set_option maxRecDepth 20000 in
 lemma contr_rank_2_symm {T1 : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
     {T2 : (Lorentz.complexCo ⊗ Lorentz.complexCo).V} :
@@ -117,8 +107,8 @@ lemma antiSymm_add_self {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
 And related results.
 
 -/
-open complexLorentzTensor
 
+/-- The map to color one gets when multiplying left and right metrics. -/
 def leftMetricMulRightMap := (Sum.elim ![Color.upL, Color.upL] ![Color.upR, Color.upR]) ∘
   finSumFinEquiv.symm
 
@@ -154,659 +144,20 @@ lemma leftMetric_mul_rightMetric : {Fermion.leftMetric | α α' ⊗ Fermion.righ
     funext x
     fin_cases x <;> rfl
 
-def pauliMatrixLowerMap := ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘
+lemma leftMetric_mul_rightMetric_tree :
-  ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 0 ∘ Fin.succAbove 1)
+    {Fermion.leftMetric | α α' ⊗ Fermion.rightMetric | β β'}ᵀ.tensor
-
-abbrev pauliMatrixContrMap {n : ℕ} (c : Fin n → complexLorentzTensor.C) :=
-  (Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm)
-
-lemma prod_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C}
-    (t : TensorTree complexLorentzTensor c) :
-    (TensorTree.prod t (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
-      PauliMatrix.asConsTensor)).tensor = (((t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 0 | 2 => 0)))).add
-    (((t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 1 | 2 => 1)))).add
-    (((t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 0 | 2 => 1)))).add
-    (((t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 1 | 2 => 0)))).add
-    ((TensorTree.smul (-I) ((t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 0 | 2 => 1))))).add
-    ((TensorTree.smul I ((t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 1 | 2 => 0))))).add
-    ((t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 3 | 1 => 0 | 2 => 0))).add
-    (TensorTree.smul (-1) (t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR]
-        fun | 0 => 3 | 1 => 1 | 2 => 1))))))))))).tensor := by
-  rw [prod_tensor_eq_snd <| pauliMatrix_basis_expand_tree]
-  rw [prod_add _ _ _]
-  rw [add_tensor_eq_snd <| prod_add _ _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    prod_add _ _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _]
-  /- Moving smuls. -/
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_fst <| prod_smul _ _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| prod_smul _ _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_snd<| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| prod_smul _ _ _]
-  rfl
-
-lemma contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C}
-    (t : TensorTree complexLorentzTensor c) (i : Fin (n + 3)) (j : Fin (n +2))
-    (h : (pauliMatrixContrMap c) (i.succAbove j) =
-      complexLorentzTensor.τ ((pauliMatrixContrMap c) i)) :
-    (contr i j h (TensorTree.prod t
-    (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
-      PauliMatrix.asConsTensor))).tensor =
-    ((contr i j h (t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 0 | 2 => 0)))).add
-    ((contr i j h (t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 1 | 2 => 1)))).add
-    ((contr i j h (t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 0 | 2 => 1)))).add
-    ((contr i j h (t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 1 | 2 => 0)))).add
-    ((TensorTree.smul (-I) (contr i j h (t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 0 | 2 => 1))))).add
-    ((TensorTree.smul I (contr i j h (t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 1 | 2 => 0))))).add
-    ((contr i j h (t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 3 | 1 => 0 | 2 => 0)))).add
-    (TensorTree.smul (-1) (contr i j h (t.prod (tensorNode
-      (basisVector ![Color.up, Color.upL, Color.upR]
-        fun | 0 => 3 | 1 => 1 | 2 => 1)))))))))))).tensor := by
-  rw [contr_tensor_eq <| prod_pauliMatrix_basis_tree_expand _]
-  /- Moving contr over add. -/
-  rw [contr_add]
-  rw [add_tensor_eq_snd <| contr_add _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| contr_add _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
-  /- Moving contr over smul. -/
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    contr_smul _ _]
-
-lemma basis_contr_pauliMatrix_basis_tree_expand' {n : ℕ} {c : Fin n → complexLorentzTensor.C}
-    (i : Fin (n + 3)) (j : Fin (n +2))
-    (h : (pauliMatrixContrMap c) (i.succAbove j) = complexLorentzTensor.τ
-      ((pauliMatrixContrMap c) i))
-    (b : Π k, Fin (complexLorentzTensor.repDim (c k))) :
-    let c' := Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ finSumFinEquiv.symm
-    let b' (i1 i2 i3 : Fin 4) := fun i => prodBasisVecEquiv (finSumFinEquiv.symm i)
-      ((HepLean.PiTensorProduct.elimPureTensor b (fun | 0 => i1 | 1 => i2 | 2 => i3))
-      (finSumFinEquiv.symm i))
-    (contr i j h (TensorTree.prod (tensorNode (basisVector c b))
-      (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
-    PauliMatrix.asConsTensor))).tensor = ((contr i j h ((tensorNode
-    (basisVector c' (b' 0 0 0))))).add
-    ((contr i j h ((tensorNode (basisVector c' (b' 0 1 1))))).add
-    ((contr i j h ((tensorNode (basisVector c' (b' 1 0 1))))).add
-    ((contr i j h ((tensorNode (basisVector c' (b' 1 1 0))))).add
-    ((TensorTree.smul (-I) (contr i j h ((tensorNode (basisVector c' (b' 2 0 1)))))).add
-    ((TensorTree.smul I (contr i j h ((tensorNode (basisVector c' (b' 2 1 0)))))).add
-    ((contr i j h ((tensorNode (basisVector c' (b' 3 0 0))))).add
-    (TensorTree.smul (-1) (contr i j h ((tensorNode
-      (basisVector c' (b' 3 1 1))))))))))))).tensor := by
-  rw [contr_pauliMatrix_basis_tree_expand]
-  /- Product of basis vectors . -/
-  rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
-    <| prod_basisVector_tree _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| contr_tensor_eq <| prod_basisVector_tree _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
-      <| prod_basisVector_tree _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
-    <| prod_basisVector_tree _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
-    <| contr_tensor_eq <| prod_basisVector_tree _ _]
-  rfl
-
-lemma basis_contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C}
-    (i : Fin (n + 3)) (j : Fin (n +2))
-    (h : (pauliMatrixContrMap c) (i.succAbove j) = complexLorentzTensor.τ
-      ((pauliMatrixContrMap c) i))
-    (b : Π k, Fin (complexLorentzTensor.repDim (c k))) :
-    let c' := (Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ finSumFinEquiv.symm)
-      ∘ Fin.succAbove i ∘ Fin.succAbove j
-    let b'' (i1 i2 i3 : Fin 4) : (i : Fin (n + (Nat.succ 0).succ.succ)) →
-        Fin (complexLorentzTensor.repDim (Sum.elim c ![Color.up, Color.upL, Color.upR]
-          (finSumFinEquiv.symm i))) := fun i => prodBasisVecEquiv (finSumFinEquiv.symm i)
-      ((HepLean.PiTensorProduct.elimPureTensor b (fun | (0 : Fin 3) => i1 | 1 => i2 | 2 => i3))
-      (finSumFinEquiv.symm i))
-    let b' (i1 i2 i3 : Fin 4) := fun k => (b'' i1 i2 i3) (i.succAbove (j.succAbove k))
-    (contr i j h (TensorTree.prod (tensorNode (basisVector c b))
-    (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
-    PauliMatrix.asConsTensor))).tensor = (((
-    TensorTree.smul (contrBasisVectorMul i j (b'' 0 0 0))
-      (tensorNode (basisVector c' (b' 0 0 0))))).add
-    (((TensorTree.smul (contrBasisVectorMul i j (b'' 0 1 1))
-      (tensorNode (basisVector c' (b' 0 1 1))))).add
-    (((TensorTree.smul (contrBasisVectorMul i j (b'' 1 0 1))
-      (tensorNode (basisVector c' (b' 1 0 1))))).add
-    (((TensorTree.smul (contrBasisVectorMul i j (b'' 1 1 0))
-      (tensorNode (basisVector c' (b' 1 1 0))))).add
-    ((TensorTree.smul (-I) ((TensorTree.smul (contrBasisVectorMul i j (b'' 2 0 1))
-      (tensorNode (basisVector c' (b' 2 0 1)))))).add
-    ((TensorTree.smul I ((TensorTree.smul (contrBasisVectorMul i j (b'' 2 1 0))
-      (tensorNode (basisVector c' (b' 2 1 0)))))).add
-    (((TensorTree.smul (contrBasisVectorMul i j (b'' 3 0 0))
-      (tensorNode (basisVector c' (b' 3 0 0))))).add
-    (TensorTree.smul (-1) ((TensorTree.smul (contrBasisVectorMul i j (b'' 3 1 1)) (tensorNode
-      (basisVector c' (b' 3 1 1))))))))))))).tensor := by
-  rw [basis_contr_pauliMatrix_basis_tree_expand']
-  /- Contracting basis vectors. -/
-  rw [add_tensor_eq_fst <| contr_basisVector_tree _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| contr_basisVector_tree _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| contr_basisVector_tree _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
-    <| contr_basisVector_tree _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    smul_tensor_eq <| contr_basisVector_tree _]
-
-lemma pauliMatrix_contr_down_0 :
-    (contr 0 1 rfl (((tensorNode (basisVector ![Color.down, Color.down] fun x => 0)).prod
-    (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
-      PauliMatrix.asConsTensor)))).tensor
-    = basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0)
-    + basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1) := by
-  rw [basis_contr_pauliMatrix_basis_tree_expand]
-  rw [contrBasisVectorMul_pos, contrBasisVectorMul_pos,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
-  simp only [smul_tensor, add_tensor, tensorNode_tensor]
-  simp only [one_smul, zero_smul, smul_zero, add_zero]
-  congr 1
-  · congr 1
-    funext k
-    fin_cases k <;> rfl
-  · congr 1
-    funext k
-    fin_cases k <;> rfl
-
-lemma pauliMatrix_contr_down_0_tree :
-    (contr 0 1 rfl (((tensorNode (basisVector ![Color.down, Color.down] fun x => 0)).prod
-    (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
-      PauliMatrix.asConsTensor)))).tensor
     = (TensorTree.add (tensorNode
-      (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0)))
+        (basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1))) <|
-    (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1)))).tensor := by
+      TensorTree.add (TensorTree.smul (-1 : ℂ) (tensorNode
-  exact pauliMatrix_contr_down_0
+        (basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0)))) <|
-
+      TensorTree.add (TensorTree.smul (-1 : ℂ) (tensorNode
-lemma pauliMatrix_contr_down_1 :
+        (basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)))) <|
-    {(basisVector ![Color.down, Color.down] fun x => 1) | μ ν ⊗
-      PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
-    = basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)
-    + basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0) := by
-  rw [basis_contr_pauliMatrix_basis_tree_expand]
-  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_pos, contrBasisVectorMul_pos,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
-  simp only [smul_tensor, add_tensor, tensorNode_tensor]
-  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
-  congr 1
-  · congr 1
-    funext k
-    fin_cases k <;> rfl
-  · congr 1
-    funext k
-    fin_cases k <;> rfl
-
-lemma pauliMatrix_contr_down_1_tree :
-    {(basisVector ![Color.down, Color.down] fun x => 1) | μ ν ⊗
-      PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
-    = (TensorTree.add (tensorNode
-      (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)))
-    (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)))).tensor := by
-  exact pauliMatrix_contr_down_1
-
-lemma pauliMatrix_contr_down_2 :
-    {(basisVector ![Color.down, Color.down] fun x => 2) | μ ν ⊗
-      PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
-    = (- I) • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)
-    + (I) • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0) := by
-  rw [basis_contr_pauliMatrix_basis_tree_expand]
-  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_pos, contrBasisVectorMul_pos,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
-  /- Simplifying. -/
-  simp only [smul_tensor, add_tensor, tensorNode_tensor]
-  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
-  congr 1
-  · congr 2
-    funext k
-    fin_cases k <;> rfl
-  · congr 2
-    funext k
-    fin_cases k <;> rfl
-
-lemma pauliMatrix_contr_down_2_tree :
-    {(basisVector ![Color.down, Color.down] fun x => 2) | μ ν ⊗
-      PauliMatrix.asConsTensor | μ α β}ᵀ.tensor =
-    (TensorTree.add
-    (smul (- I) (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1))))
-    (smul I (tensorNode (basisVector
-      pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0))))).tensor := by
-  exact pauliMatrix_contr_down_2
-
-lemma pauliMatrix_contr_down_3 :
-    {(basisVector ![Color.down, Color.down] fun x => 3) | μ ν ⊗
-    PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
-    = basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)
-    + (- 1 : ℂ) • basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by
-  rw [basis_contr_pauliMatrix_basis_tree_expand]
-  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_pos, contrBasisVectorMul_pos]
-  /- Simplifying. -/
-  simp only [smul_tensor, add_tensor, tensorNode_tensor]
-  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
-  congr 1
-  · congr 2
-    funext k
-    fin_cases k <;> rfl
-  · congr 2
-    funext k
-    fin_cases k <;> rfl
-
-lemma pauliMatrix_contr_down_3_tree : {(basisVector ![Color.down, Color.down] fun x => 3) | μ ν ⊗
-      PauliMatrix.asConsTensor | μ α β}ᵀ.tensor =
-    (TensorTree.add
-      ((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0))))
-      (smul (-1) (tensorNode (basisVector pauliMatrixLowerMap
-      (fun | 0 => 3 | 1 => 1 | 2 => 1))))).tensor := by
-  exact pauliMatrix_contr_down_3
-
-def pauliMatrixContrPauliMatrixMap := ((Sum.elim
-  ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘
-  Fin.succAbove 0 ∘ Fin.succAbove 1) ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘
-  Fin.succAbove 0 ∘ Fin.succAbove 2)
-
-lemma pauliMatrix_contr_lower_0_0_0 :
-    {(basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0)) | μ α β ⊗
-    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
-    basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0)
-    + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) := by
-  rw [basis_contr_pauliMatrix_basis_tree_expand]
-  rw [contrBasisVectorMul_pos, contrBasisVectorMul_pos,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
-  /- Simplifying. -/
-  simp only [smul_tensor, add_tensor, tensorNode_tensor]
-  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
-  congr 1
-  · congr 1
-    funext k
-    fin_cases k <;> rfl
-  · congr 1
-    funext k
-    fin_cases k <;> rfl
-
-lemma pauliMatrix_contr_lower_0_1_1 :
-    {(basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1)) | μ α β ⊗
-    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
-    basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0)
-    + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by
-  rw [basis_contr_pauliMatrix_basis_tree_expand]
-  rw [contrBasisVectorMul_pos, contrBasisVectorMul_pos,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
-  /- Simplifying. -/
-  simp only [smul_tensor, add_tensor, tensorNode_tensor]
-  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
-  congr 1
-  · congr 1
-    funext k
-    fin_cases k <;> rfl
-  · congr 1
-    funext k
-    fin_cases k <;> rfl
-
-lemma pauliMatrix_contr_lower_1_0_1 :
-    {(basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)) | μ α β ⊗
-    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
-    basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
-    + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) := by
-  rw [basis_contr_pauliMatrix_basis_tree_expand]
-  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_pos, contrBasisVectorMul_pos,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
-  /- Simplifying. -/
-  simp only [smul_tensor, add_tensor, tensorNode_tensor]
-  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
-  congr 1
-  · congr 1
-    funext k
-    fin_cases k <;> rfl
-  · congr 1
-    funext k
-    fin_cases k <;> rfl
-
-lemma pauliMatrix_contr_lower_1_1_0 :
-    {(basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)) | μ α β ⊗
-    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
-    basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)
-    + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by
-  rw [basis_contr_pauliMatrix_basis_tree_expand]
-  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_pos, contrBasisVectorMul_pos,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
-  /- Simplifying. -/
-  simp only [smul_tensor, add_tensor, tensorNode_tensor]
-  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
-  congr 1
-  · congr 1
-    funext k
-    fin_cases k <;> rfl
-  · congr 1
-    funext k
-    fin_cases k <;> rfl
-
-lemma pauliMatrix_contr_lower_2_0_1 :
-    {(basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)) | μ α β ⊗
-    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
-      (-I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
-    + (I) •
-      basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) := by
-  rw [basis_contr_pauliMatrix_basis_tree_expand]
-  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_pos, contrBasisVectorMul_pos,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
-  /- Simplifying. -/
-  simp only [smul_tensor, add_tensor, tensorNode_tensor]
-  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
-  congr 1
-  · congr 2
-    funext k
-    fin_cases k <;> rfl
-  · congr 2
-    funext k
-    fin_cases k <;> rfl
-
-lemma pauliMatrix_contr_lower_2_1_0 :
-    {(basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0)) | μ α β ⊗
-    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
-      (-I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)
-    + (I) •
-      basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by
-  rw [basis_contr_pauliMatrix_basis_tree_expand]
-  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_pos, contrBasisVectorMul_pos,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
-  /- Simplifying. -/
-  simp only [smul_tensor, add_tensor, tensorNode_tensor]
-  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
-  congr 1
-  · congr 2
-    funext k
-    fin_cases k <;> rfl
-  · congr 2
-    funext k
-    fin_cases k <;> rfl
-
-lemma pauliMatrix_contr_lower_3_0_0 :
-    {(basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)) | μ α β ⊗
-    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
-    basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0)
-    + (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap
-    (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) := by
-  rw [basis_contr_pauliMatrix_basis_tree_expand]
-  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_pos, contrBasisVectorMul_pos]
-  /- Simplifying. -/
-  simp only [smul_tensor, add_tensor, tensorNode_tensor]
-  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
-  congr 1
-  · congr 2
-    funext k
-    fin_cases k <;> rfl
-  · congr 2
-    funext k
-    fin_cases k <;> rfl
-
-lemma pauliMatrix_contr_lower_3_1_1 :
-    {(basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1)) | μ α β ⊗
-    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
-    basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0)
-    + (-1 : ℂ) •
-      basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by
-  rw [basis_contr_pauliMatrix_basis_tree_expand]
-  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
-      contrBasisVectorMul_pos, contrBasisVectorMul_pos]
-  /- Simplifying. -/
-  simp only [smul_tensor, add_tensor, tensorNode_tensor]
-  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
-  congr 1
-  · congr 2
-    funext k
-    fin_cases k <;> rfl
-  · congr 2
-    funext k
-    fin_cases k <;> rfl
-
-lemma pauliMatrix_lower : {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
-    = basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0)
-    + basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1)
-    - basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)
-    - basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)
-    + I • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)
-    - I • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0)
-    - basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)
-    + basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by
-  rw [contr_tensor_eq <| prod_tensor_eq_fst <| coMetric_basis_expand_tree]
-  /- Moving the prod through additions. -/
-  rw [contr_tensor_eq <| add_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _]
-  /- Moving the prod through smuls. -/
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| smul_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| smul_prod _ _ _]
-  /- Moving contraction through addition. -/
-  rw [contr_add]
-  rw [add_tensor_eq_snd <| contr_add _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
-  /- Moving contraction through smul. -/
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_smul _ _]
-  /- Replacing the contractions. -/
-  rw [add_tensor_eq_fst <| pauliMatrix_contr_down_0_tree]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| pauliMatrix_contr_down_1_tree]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <|
-    pauliMatrix_contr_down_2_tree]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq <|
-    pauliMatrix_contr_down_3_tree]
-  /- Simplifying -/
-  simp only [add_tensor, smul_tensor, tensorNode_tensor, smul_add,_root_.smul_smul]
-  simp only [Nat.reduceAdd, Fin.isValue, neg_smul, one_smul, mul_neg, neg_mul, one_mul,
-    _root_.neg_neg, mul_one]
-  rfl
-
-lemma pauliMatrix_lower_tree : {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
-    = (TensorTree.add (tensorNode
-      (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0))) <|
-    TensorTree.add (tensorNode
-      (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1))) <|
-    TensorTree.add (TensorTree.smul (-1) (tensorNode
-      (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)))) <|
-    TensorTree.add (TensorTree.smul (-1) (tensorNode
-      (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)))) <|
-    TensorTree.add (TensorTree.smul I (tensorNode
-      (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)))) <|
-    TensorTree.add (TensorTree.smul (-I) (tensorNode
-      (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0)))) <|
-    TensorTree.add (TensorTree.smul (-1) (tensorNode
-      (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)))) <|
-      (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1)))).tensor := by
-  rw [pauliMatrix_lower]
-  simp only [Nat.reduceAdd, Fin.isValue, add_tensor,
-    tensorNode_tensor, smul_tensor, neg_smul, one_smul]
-  rfl
-
-lemma pauliMatrix_contract_pauliMatrix_aux :
-  {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗
-    PauliMatrix.asConsTensor | ν α' β'}ᵀ.tensor
-  = ((tensorNode
-      ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) +
-        basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1)).add
-    ((tensorNode
-      ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) +
-      basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1)).add
-    ((TensorTree.smul (-1) (tensorNode
-      ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) +
-      basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0))).add
-    ((TensorTree.smul (-1) (tensorNode
-      ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) +
-      basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0))).add
-    ((TensorTree.smul I (tensorNode
-      ((-I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) +
-        I •
-        basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0))).add
-    ((TensorTree.smul (-I) (tensorNode
-      ((-I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) +
-      I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0))).add
-      ((TensorTree.smul (-1) (tensorNode
-        ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) +
-        (-1 : ℂ) •
-        basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1))).add
       (tensorNode
-        ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) +
+        (basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0)))).tensor := by
-        (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap
+  rw [leftMetric_mul_rightMetric]
-          fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1))))))))).tensor := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, add_tensor, tensorNode_tensor,
-  rw [contr_tensor_eq <| prod_tensor_eq_fst <| pauliMatrix_lower_tree]
+    smul_tensor, neg_smul, one_smul]
-  /- Moving the prod through additions. -/
+  rfl
-  rw [contr_tensor_eq <| add_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _]
-  /- Moving the prod through smuls. -/
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <|
-    smul_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_fst <| smul_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_tensor_eq_fst <| smul_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_prod _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <|
-    smul_prod _ _ _]
-  /- Moving contraction through addition. -/
-  rw [contr_add]
-  rw [add_tensor_eq_snd <| contr_add _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    contr_add _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| contr_add _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
-  /- Moving contraction through smul. -/
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <|
-    contr_smul _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_fst <| contr_smul _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
-  /- Replacing the contractions. -/
-  rw [add_tensor_eq_fst <| eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_0_0_0]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| eq_tensorNode_of_eq_tensor <|
-    pauliMatrix_contr_lower_0_1_1]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <|
-    eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_1_0_1]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <|
-    smul_tensor_eq <| eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_1_1_0]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_fst <| smul_tensor_eq <| eq_tensorNode_of_eq_tensor <|
-    pauliMatrix_contr_lower_2_0_1]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| eq_tensorNode_of_eq_tensor
-    <| pauliMatrix_contr_lower_2_1_0]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <|
-    eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_3_0_0]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
-    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| eq_tensorNode_of_eq_tensor <|
-    pauliMatrix_contr_lower_3_1_1]
-
-lemma pauliMatrix_contract_pauliMatrix :
-  {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗
-  PauliMatrix.asConsTensor | ν α' β'}ᵀ.tensor =
-  2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1)
-    + 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0)
-    - 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0)
-    - 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) := by
-  rw [pauliMatrix_contract_pauliMatrix_aux]
-  simp only [Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero, neg_smul,
-    one_smul, add_tensor, tensorNode_tensor, smul_tensor, smul_add, smul_neg, _root_.smul_smul,
-    neg_mul, _root_.neg_neg]
-  ring_nf
-  rw [Complex.I_sq]
-  simp only [neg_smul, one_smul, _root_.neg_neg]
-  abel
 
 end Fermion
 

HepLean/Tensors/ComplexLorentz/PauliContr.lean

@@ -0,0 +1,373 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Tensors.ComplexLorentz.PauliLower
+import HepLean.Tensors.ComplexLorentz.Lemmas
+/-!
+
+## Contractiong of indices of Pauli matrix.
+
+The main result of this file is `pauliMatrix_contract_pauliMatrix` which states that
+`η_{μν} σ^{μ α dot β} σ^{ν α' dot β'} = 2 ε^{αα'} ε^{dot β dot β'}`.
+
+The current way this result is proved is by using tensor tree manipulations.
+There is likely a more direct path to this result.
+
+-/
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open IndexNotation
+open CategoryTheory
+open TensorTree
+open OverColor.Discrete
+noncomputable section
+
+namespace Fermion
+open complexLorentzTensor
+
+/-- The map to colors one gets when contracting the 4-vector indices pauli matrices. -/
+def pauliMatrixContrPauliMatrixMap := ((Sum.elim
+  ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘
+  Fin.succAbove 0 ∘ Fin.succAbove 1) ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘
+  Fin.succAbove 0 ∘ Fin.succAbove 2)
+
+lemma pauliMatrix_contr_lower_0_0_0 :
+    {(basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0)) | μ α β ⊗
+    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
+    basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0)
+    + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) := by
+  rw [basis_contr_pauliMatrix_basis_tree_expand]
+  rw [contrBasisVectorMul_pos, contrBasisVectorMul_pos,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
+  /- Simplifying. -/
+  simp only [smul_tensor, add_tensor, tensorNode_tensor]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
+  congr 1
+  · congr 1
+    funext k
+    fin_cases k <;> rfl
+  · congr 1
+    funext k
+    fin_cases k <;> rfl
+
+lemma pauliMatrix_contr_lower_0_1_1 :
+    {(basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1)) | μ α β ⊗
+    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
+    basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0)
+    + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by
+  rw [basis_contr_pauliMatrix_basis_tree_expand]
+  rw [contrBasisVectorMul_pos, contrBasisVectorMul_pos,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
+  /- Simplifying. -/
+  simp only [smul_tensor, add_tensor, tensorNode_tensor]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
+  congr 1
+  · congr 1
+    funext k
+    fin_cases k <;> rfl
+  · congr 1
+    funext k
+    fin_cases k <;> rfl
+
+lemma pauliMatrix_contr_lower_1_0_1 :
+    {(basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)) | μ α β ⊗
+    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
+    basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
+    + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) := by
+  rw [basis_contr_pauliMatrix_basis_tree_expand]
+  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_pos, contrBasisVectorMul_pos,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
+  /- Simplifying. -/
+  simp only [smul_tensor, add_tensor, tensorNode_tensor]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
+  congr 1
+  · congr 1
+    funext k
+    fin_cases k <;> rfl
+  · congr 1
+    funext k
+    fin_cases k <;> rfl
+
+lemma pauliMatrix_contr_lower_1_1_0 :
+    {(basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)) | μ α β ⊗
+    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
+    basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)
+    + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by
+  rw [basis_contr_pauliMatrix_basis_tree_expand]
+  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_pos, contrBasisVectorMul_pos,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
+  /- Simplifying. -/
+  simp only [smul_tensor, add_tensor, tensorNode_tensor]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
+  congr 1
+  · congr 1
+    funext k
+    fin_cases k <;> rfl
+  · congr 1
+    funext k
+    fin_cases k <;> rfl
+
+lemma pauliMatrix_contr_lower_2_0_1 :
+    {(basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)) | μ α β ⊗
+    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
+      (-I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
+    + (I) •
+      basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) := by
+  rw [basis_contr_pauliMatrix_basis_tree_expand]
+  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_pos, contrBasisVectorMul_pos,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
+  /- Simplifying. -/
+  simp only [smul_tensor, add_tensor, tensorNode_tensor]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
+  congr 1
+  · congr 2
+    funext k
+    fin_cases k <;> rfl
+  · congr 2
+    funext k
+    fin_cases k <;> rfl
+
+lemma pauliMatrix_contr_lower_2_1_0 :
+    {(basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0)) | μ α β ⊗
+    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
+      (-I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)
+    + (I) •
+      basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by
+  rw [basis_contr_pauliMatrix_basis_tree_expand]
+  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_pos, contrBasisVectorMul_pos,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
+  /- Simplifying. -/
+  simp only [smul_tensor, add_tensor, tensorNode_tensor]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
+  congr 1
+  · congr 2
+    funext k
+    fin_cases k <;> rfl
+  · congr 2
+    funext k
+    fin_cases k <;> rfl
+
+lemma pauliMatrix_contr_lower_3_0_0 :
+    {(basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)) | μ α β ⊗
+    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
+    basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0)
+    + (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap
+    (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) := by
+  rw [basis_contr_pauliMatrix_basis_tree_expand]
+  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_pos, contrBasisVectorMul_pos]
+  /- Simplifying. -/
+  simp only [smul_tensor, add_tensor, tensorNode_tensor]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
+  congr 1
+  · congr 2
+    funext k
+    fin_cases k <;> rfl
+  · congr 2
+    funext k
+    fin_cases k <;> rfl
+
+lemma pauliMatrix_contr_lower_3_1_1 :
+    {(basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1)) | μ α β ⊗
+    PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor =
+    basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0)
+    + (-1 : ℂ) •
+      basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by
+  rw [basis_contr_pauliMatrix_basis_tree_expand]
+  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_pos, contrBasisVectorMul_pos]
+  /- Simplifying. -/
+  simp only [smul_tensor, add_tensor, tensorNode_tensor]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
+  congr 1
+  · congr 2
+    funext k
+    fin_cases k <;> rfl
+  · congr 2
+    funext k
+    fin_cases k <;> rfl
+
+/-! TODO: Work out why `pauliMatrix_lower_basis_expand_prod'` is needed. -/
+/-- This lemma is exactly the same as `pauliMatrix_lower_basis_expand_prod'`.
+  It is needed here for `pauliMatrix_contract_pauliMatrix_aux`. It is unclear why
+  `pauliMatrix_lower_basis_expand_prod` does not work. -/
+private lemma pauliMatrix_lower_basis_expand_prod' {n : ℕ} {c : Fin n → complexLorentzTensor.C}
+    (t : TensorTree complexLorentzTensor c) :
+    (prod {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ t).tensor =
+    ((((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 0 | 1 => 0 | 2 => 0)).prod t).add
+    (((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 0 | 1 => 1 | 2 => 1)).prod t).add
+    ((TensorTree.smul (-1) ((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 1 | 1 => 0 | 2 => 1)).prod t)).add
+    ((TensorTree.smul (-1) ((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 1 | 1 => 1 | 2 => 0)).prod t)).add
+    ((TensorTree.smul I ((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 2 | 1 => 0 | 2 => 1)).prod t)).add
+    ((TensorTree.smul (-I) ((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 2 | 1 => 1 | 2 => 0)).prod t)).add
+    ((TensorTree.smul (-1) ((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 3 | 1 => 0 | 2 => 0)).prod t)).add
+    ((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 3 | 1 => 1 | 2 => 1)).prod
+      t))))))))).tensor := by
+    exact pauliMatrix_lower_basis_expand_prod _
+
+lemma pauliMatrix_contract_pauliMatrix_aux :
+  {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗
+    PauliMatrix.asConsTensor | ν α' β'}ᵀ.tensor
+  = ((tensorNode
+      ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) +
+        basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1)).add
+    ((tensorNode
+      ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) +
+      basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1)).add
+    ((TensorTree.smul (-1) (tensorNode
+      ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) +
+      basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0))).add
+    ((TensorTree.smul (-1) (tensorNode
+      ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) +
+      basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0))).add
+    ((TensorTree.smul I (tensorNode
+      ((-I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) +
+        I •
+        basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0))).add
+    ((TensorTree.smul (-I) (tensorNode
+      ((-I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) +
+      I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0))).add
+      ((TensorTree.smul (-1) (tensorNode
+        ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) +
+        (-1 : ℂ) •
+        basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1))).add
+      (tensorNode
+        ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) +
+        (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap
+          fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1))))))))).tensor := by
+  rw [contr_tensor_eq <| pauliMatrix_lower_basis_expand_prod' _]
+  /- Moving contraction through addition. -/
+  rw [contr_add]
+  rw [add_tensor_eq_snd <| contr_add _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    contr_add _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| contr_add _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
+  /- Moving contraction through smul. -/
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <|
+    contr_smul _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_fst <| contr_smul _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
+  /- Replacing the contractions. -/
+  rw [add_tensor_eq_fst <| eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_0_0_0]
+  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| eq_tensorNode_of_eq_tensor <|
+    pauliMatrix_contr_lower_0_1_1]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <|
+    eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_1_0_1]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <|
+    smul_tensor_eq <| eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_1_1_0]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_fst <| smul_tensor_eq <| eq_tensorNode_of_eq_tensor <|
+    pauliMatrix_contr_lower_2_0_1]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| eq_tensorNode_of_eq_tensor
+    <| pauliMatrix_contr_lower_2_1_0]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <|
+    eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_3_0_0]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| eq_tensorNode_of_eq_tensor <|
+    pauliMatrix_contr_lower_3_1_1]
+
+lemma pauliMatrix_contract_pauliMatrix_expand :
+  {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗
+  PauliMatrix.asConsTensor | ν α' β'}ᵀ.tensor =
+    2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1)
+    + 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0)
+    - 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0)
+    - 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) := by
+  rw [pauliMatrix_contract_pauliMatrix_aux]
+  simp only [Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero, neg_smul,
+    one_smul, add_tensor, tensorNode_tensor, smul_tensor, smul_add, smul_neg, _root_.smul_smul,
+    neg_mul, _root_.neg_neg]
+  ring_nf
+  rw [Complex.I_sq]
+  simp only [neg_smul, one_smul, _root_.neg_neg]
+  abel
+
+/-- The statement that `η_{μν} σ^{μ α dot β} σ^{ν α' dot β'} = 2 ε^{αα'} ε^{dot β dot β'}`. -/
+theorem pauliMatrix_contract_pauliMatrix :
+    {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗
+    PauliMatrix.asConsTensor | ν α' β' =
+    2 •ₜ Fermion.leftMetric | α α' ⊗ Fermion.rightMetric | β β'}ᵀ := by
+  rw [pauliMatrix_contract_pauliMatrix_expand]
+  rw [perm_tensor_eq <| smul_tensor_eq <| leftMetric_mul_rightMetric_tree]
+  rw [perm_smul]
+  /- Moving perm through adds. -/
+  rw [smul_tensor_eq <| perm_add _ _ _]
+  rw [smul_tensor_eq <| add_tensor_eq_snd <| perm_add _ _ _]
+  rw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| perm_add _ _ _]
+  /- Moving perm through smul. -/
+  rw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_fst <| perm_smul _ _ _]
+  rw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| add_tensor_eq_fst <| perm_smul _ _ _]
+  /- Perm acting on basis. -/
+  erw [smul_tensor_eq <| add_tensor_eq_fst <| perm_basisVector_tree _ _]
+  erw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <|
+    perm_basisVector_tree _ _]
+  erw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <|
+    smul_tensor_eq <| perm_basisVector_tree _ _]
+  erw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    perm_basisVector_tree _ _]
+  /- Simplifying. -/
+  simp only [smul_tensor, add_tensor, tensorNode_tensor]
+  have h1 (b0011 b1100 b0110 b1001 : CoeSort.coe (complexLorentzTensor.F.obj
+      (OverColor.mk pauliMatrixContrPauliMatrixMap))) :
+      ((2 • b0011 + 2 • b1100) - 2 • b0110 - 2 • b1001) = (2 : ℂ) • ((b0011) +
+      (((-1 : ℂ)• b0110) + (((-1 : ℂ) •b1001) + b1100))) := by
+    trans (2 : ℂ) • b0011 + (2 : ℂ) • b1100 - ((2 : ℂ) • b0110) - ((2 : ℂ) • b1001)
+    · repeat rw [two_smul]
+    · simp only [neg_smul, one_smul, smul_add, smul_neg]
+      abel
+  rw [h1]
+  congr
+  · funext i
+    fin_cases i <;> rfl
+  · funext i
+    fin_cases i <;> rfl
+  · funext i
+    fin_cases i <;> rfl
+  · funext i
+    fin_cases i <;> rfl
+
+end Fermion

HepLean/Tensors/ComplexLorentz/PauliLower.lean

@@ -0,0 +1,257 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Tensors.ComplexLorentz.BasisTrees
+/-!
+
+## Lowering indices of Pauli matrices.
+
+-/
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open IndexNotation
+open CategoryTheory
+open TensorTree
+open OverColor.Discrete
+noncomputable section
+
+namespace Fermion
+open complexLorentzTensor
+
+/-- The map to color one gets when lowering the indices of pauli matrices. -/
+def pauliMatrixLowerMap := ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘
+  ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 0 ∘ Fin.succAbove 1)
+
+lemma pauliMatrix_contr_down_0 :
+    (contr 0 1 rfl (((tensorNode (basisVector ![Color.down, Color.down] fun x => 0)).prod
+    (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
+      PauliMatrix.asConsTensor)))).tensor
+    = basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0)
+    + basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1) := by
+  rw [basis_contr_pauliMatrix_basis_tree_expand]
+  rw [contrBasisVectorMul_pos, contrBasisVectorMul_pos,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
+  simp only [smul_tensor, add_tensor, tensorNode_tensor]
+  simp only [one_smul, zero_smul, smul_zero, add_zero]
+  congr 1
+  · congr 1
+    funext k
+    fin_cases k <;> rfl
+  · congr 1
+    funext k
+    fin_cases k <;> rfl
+
+lemma pauliMatrix_contr_down_0_tree :
+    (contr 0 1 rfl (((tensorNode (basisVector ![Color.down, Color.down] fun x => 0)).prod
+    (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
+      PauliMatrix.asConsTensor)))).tensor
+    = (TensorTree.add (tensorNode
+      (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0)))
+    (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1)))).tensor := by
+  exact pauliMatrix_contr_down_0
+
+lemma pauliMatrix_contr_down_1 :
+    {(basisVector ![Color.down, Color.down] fun x => 1) | μ ν ⊗
+      PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
+    = basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)
+    + basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0) := by
+  rw [basis_contr_pauliMatrix_basis_tree_expand]
+  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_pos, contrBasisVectorMul_pos,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
+  simp only [smul_tensor, add_tensor, tensorNode_tensor]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
+  congr 1
+  · congr 1
+    funext k
+    fin_cases k <;> rfl
+  · congr 1
+    funext k
+    fin_cases k <;> rfl
+
+lemma pauliMatrix_contr_down_1_tree :
+    {(basisVector ![Color.down, Color.down] fun x => 1) | μ ν ⊗
+      PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
+    = (TensorTree.add (tensorNode
+      (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)))
+    (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)))).tensor := by
+  exact pauliMatrix_contr_down_1
+
+lemma pauliMatrix_contr_down_2 :
+    {(basisVector ![Color.down, Color.down] fun x => 2) | μ ν ⊗
+      PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
+    = (- I) • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)
+    + (I) • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0) := by
+  rw [basis_contr_pauliMatrix_basis_tree_expand]
+  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_pos, contrBasisVectorMul_pos,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg]
+  /- Simplifying. -/
+  simp only [smul_tensor, add_tensor, tensorNode_tensor]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
+  congr 1
+  · congr 2
+    funext k
+    fin_cases k <;> rfl
+  · congr 2
+    funext k
+    fin_cases k <;> rfl
+
+lemma pauliMatrix_contr_down_2_tree :
+    {(basisVector ![Color.down, Color.down] fun x => 2) | μ ν ⊗
+      PauliMatrix.asConsTensor | μ α β}ᵀ.tensor =
+    (TensorTree.add
+    (smul (- I) (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1))))
+    (smul I (tensorNode (basisVector
+      pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0))))).tensor := by
+  exact pauliMatrix_contr_down_2
+
+lemma pauliMatrix_contr_down_3 :
+    {(basisVector ![Color.down, Color.down] fun x => 3) | μ ν ⊗
+    PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
+    = basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)
+    + (- 1 : ℂ) • basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by
+  rw [basis_contr_pauliMatrix_basis_tree_expand]
+  rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_neg, contrBasisVectorMul_neg,
+      contrBasisVectorMul_pos, contrBasisVectorMul_pos]
+  /- Simplifying. -/
+  simp only [smul_tensor, add_tensor, tensorNode_tensor]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
+  congr 1
+  · congr 2
+    funext k
+    fin_cases k <;> rfl
+  · congr 2
+    funext k
+    fin_cases k <;> rfl
+
+lemma pauliMatrix_contr_down_3_tree : {(basisVector ![Color.down, Color.down] fun x => 3) | μ ν ⊗
+      PauliMatrix.asConsTensor | μ α β}ᵀ.tensor =
+    (TensorTree.add
+      ((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0))))
+      (smul (-1) (tensorNode (basisVector pauliMatrixLowerMap
+      (fun | 0 => 3 | 1 => 1 | 2 => 1))))).tensor := by
+  exact pauliMatrix_contr_down_3
+
+lemma pauliMatrix_lower : {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
+    = basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0)
+    + basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1)
+    - basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)
+    - basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)
+    + I • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)
+    - I • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0)
+    - basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)
+    + basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by
+  rw [contr_tensor_eq <| prod_tensor_eq_fst <| coMetric_basis_expand_tree]
+  /- Moving the prod through additions. -/
+  rw [contr_tensor_eq <| add_prod _ _ _]
+  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_prod _ _ _]
+  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _]
+  /- Moving the prod through smuls. -/
+  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_prod _ _ _]
+  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
+    <| smul_prod _ _ _]
+  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
+    <| smul_prod _ _ _]
+  /- Moving contraction through addition. -/
+  rw [contr_add]
+  rw [add_tensor_eq_snd <| contr_add _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
+  /- Moving contraction through smul. -/
+  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_smul _ _]
+  /- Replacing the contractions. -/
+  rw [add_tensor_eq_fst <| pauliMatrix_contr_down_0_tree]
+  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| pauliMatrix_contr_down_1_tree]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <|
+    pauliMatrix_contr_down_2_tree]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq <|
+    pauliMatrix_contr_down_3_tree]
+  /- Simplifying -/
+  simp only [add_tensor, smul_tensor, tensorNode_tensor, smul_add,_root_.smul_smul]
+  simp only [Nat.reduceAdd, Fin.isValue, neg_smul, one_smul, mul_neg, neg_mul, one_mul,
+    _root_.neg_neg, mul_one]
+  rfl
+
+lemma pauliMatrix_lower_tree : {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
+    = (TensorTree.add (tensorNode
+      (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0))) <|
+    TensorTree.add (tensorNode
+      (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1))) <|
+    TensorTree.add (TensorTree.smul (-1) (tensorNode
+      (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)))) <|
+    TensorTree.add (TensorTree.smul (-1) (tensorNode
+      (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)))) <|
+    TensorTree.add (TensorTree.smul I (tensorNode
+      (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)))) <|
+    TensorTree.add (TensorTree.smul (-I) (tensorNode
+      (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0)))) <|
+    TensorTree.add (TensorTree.smul (-1) (tensorNode
+      (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)))) <|
+      (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1)))).tensor := by
+  rw [pauliMatrix_lower]
+  simp only [Nat.reduceAdd, Fin.isValue, add_tensor,
+    tensorNode_tensor, smul_tensor, neg_smul, one_smul]
+  rfl
+
+lemma pauliMatrix_lower_basis_expand_prod {n : ℕ} {c : Fin n → complexLorentzTensor.C}
+    (t : TensorTree complexLorentzTensor c) :
+    (prod {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ t).tensor =
+    (((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 0 | 1 => 0 | 2 => 0)).prod t).add
+    (((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 0 | 1 => 1 | 2 => 1)).prod t).add
+    ((TensorTree.smul (-1) ((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 1 | 1 => 0 | 2 => 1)).prod t)).add
+    ((TensorTree.smul (-1) ((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 1 | 1 => 1 | 2 => 0)).prod t)).add
+    ((TensorTree.smul I ((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 2 | 1 => 0 | 2 => 1)).prod t)).add
+    ((TensorTree.smul (-I) ((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 2 | 1 => 1 | 2 => 0)).prod t)).add
+    ((TensorTree.smul (-1) ((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 3 | 1 => 0 | 2 => 0)).prod t)).add
+    ((tensorNode
+      (basisVector pauliMatrixLowerMap fun | 0 => 3 | 1 => 1 | 2 => 1)).prod
+      t)))))))).tensor := by
+  rw [prod_tensor_eq_fst <| pauliMatrix_lower_tree]
+  /- Moving the prod through additions. -/
+  rw [add_prod _ _ _]
+  rw [add_tensor_eq_snd <| add_prod _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_prod _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_prod _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _]
+  /- Moving the prod through smuls. -/
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <|
+    smul_prod _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_fst <| smul_prod _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_tensor_eq_fst <| smul_prod _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_prod _ _ _]
+  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
+    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <|
+    smul_prod _ _ _]
+
+end Fermion

HepLean/Tensors/OverColor/Lift.lean

@@ -208,7 +208,7 @@ def discreteSumEquiv {X Y : OverColor C} (i : X.left ⊕ Y.left) :
   | Sum.inr _ => LinearEquiv.refl _ _
 
 /-- An equivalence used in the lemma of `μ_tmul_tprod_mk`. Identical to `μModEquiv`
-  except with arguments based on maps instead of elements of `OverColor C`.  -/
+  except with arguments based on maps instead of elements of `OverColor C`. -/
 def discreteSumEquiv' {X Y : Type} {cX : X → C} {cY : Y → C} (i : X ⊕ Y) :
     Sum.elim (fun i => F.obj (Discrete.mk (cX i)))
     (fun i => F.obj (Discrete.mk (cY i))) i ≃ₗ[k] F.obj (Discrete.mk ((Sum.elim cX cY) i)) :=
@@ -280,9 +280,12 @@ lemma μ_tmul_tprod_mk {X Y : Type} {cX : X → C} {cY : Y → C}
   let q' : (i : (OverColor.mk cY).left) → (F.obj <| Discrete.mk ((OverColor.mk cY).hom i)) := q
   let p' : (i : (OverColor.mk cX).left) → (F.obj <| Discrete.mk ((OverColor.mk cX).hom i)) := p
   have h1 := μModEquiv_tmul_tprod F p' q'
-  simp at h1
+  simp only [Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    objObj'_V_carrier, mk_hom, Functor.id_obj, instMonoidalCategoryStruct_tensorObj_hom] at h1
   erw [h1]
-  simp [p', q']
+  simp only [objObj'_V_carrier, instMonoidalCategoryStruct_tensorObj_left,
+    instMonoidalCategoryStruct_tensorObj_hom, mk_hom, p', q']
   apply congrArg
   funext i
   match i with

HepLean/Tensors/Tree/Elab.lean

@@ -250,7 +250,7 @@ def termNodeSyntax (T : Term) : TermElabM Term := do
     return f T
   | _ =>
   match type with
-  | Expr.app _ (Expr.app _ (Expr.app _ c)) =>
+  | Expr.app _ (Expr.app _ (Expr.app _ _)) =>
       return Syntax.mkApp (mkIdent ``TensorTree.tensorNode) #[T]
   | _ => return Syntax.mkApp (mkIdent ``TensorTree.vecNode) #[T]
 

HepLean/Tensors/Tree/NodeIdentities/Basic.lean

@@ -125,7 +125,7 @@ These identities are related to the fact that all the maps are linear.
 
 lemma smul_smul (t : TensorTree S c) (a b : S.k) :
     (smul a (smul b t)).tensor = (smul (a * b) t).tensor := by
-  simp [smul_tensor]
+  simp only [smul_tensor]
   exact _root_.smul_smul a b t.tensor
 
 lemma smul_one (t : TensorTree S c) :
@@ -150,11 +150,21 @@ lemma add_assoc (t1 t2 t3 : TensorTree S c) :
 
 /-- When the same permutation acts on both arguments of an addition, the permutation
   can be moved out of the addition. -/
-lemma add_perm {n : ℕ} {c : Fin n → S.C} {c1 : Fin n → S.C}
+lemma add_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
     (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t t1 : TensorTree S c) :
     (add (perm σ t) (perm σ t1)).tensor = (perm σ (add t t1)).tensor := by
   simp only [add_tensor, perm_tensor, map_add]
 
+lemma perm_add {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
+    (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t t1 : TensorTree S c) :
+    (perm σ (add t t1)).tensor = (add (perm σ t) (perm σ t1)).tensor := by
+  simp only [add_tensor, perm_tensor, map_add]
+
+lemma perm_smul {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
+    (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (a : S.k) (t : TensorTree S c) :
+    (perm σ (smul a t)).tensor = (smul a (perm σ t)).tensor := by
+  simp only [smul_tensor, perm_tensor, map_smul]
+
 /-- When the same evaluation acts on both arguments of an addition, the evaluation
   can be moved out of the addition. -/
 lemma add_eval {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : ℕ) (t t1 : TensorTree S c) :