From 95857993b5c9fa329adc546dbd30ae8ae3d4ae76 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 24 Oct 2024 06:10:08 +0000
Subject: [PATCH] refactor: Simplify proofs

---
 .../LorentzVector/Complex/Basic.lean          |   1 -
 HepLean/Tensors/ComplexLorentz/Basic.lean     |   1 -
 HepLean/Tensors/ComplexLorentz/Basis.lean     |  33 +-
 HepLean/Tensors/ComplexLorentz/Lemmas.lean    | 824 +++++++-----------
 HepLean/Tensors/OverColor/Lift.lean           |   1 -
 HepLean/Tensors/Tree/Basic.lean               |   2 +-
 6 files changed, 366 insertions(+), 496 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean b/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
index 20cf861..b59a393 100644
--- a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
+++ b/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
@@ -88,7 +88,6 @@ lemma complexCoBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 1 ⊕ Fin 3) :
 def complexCoBasisFin4 : Basis (Fin 4) ℂ complexCo :=
   Basis.reindex complexCoBasis finSumFinEquiv
 
-
 /-!
 
 ## Relation to real
diff --git a/HepLean/Tensors/ComplexLorentz/Basic.lean b/HepLean/Tensors/ComplexLorentz/Basic.lean
index 067b2b9..8c4a0a0 100644
--- a/HepLean/Tensors/ComplexLorentz/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basic.lean
@@ -184,6 +184,5 @@ lemma basis_contr (c : complexLorentzTensor.C) (i : Fin (complexLorentzTensor.re
   | Color.up => Lorentz.contrCoContraction_basis _ _
   | Color.down => Lorentz.coContrContraction_basis _ _
 
-
 end
 end Fermion
diff --git a/HepLean/Tensors/ComplexLorentz/Basis.lean b/HepLean/Tensors/ComplexLorentz/Basis.lean
index ec707a7..54ab11f 100644
--- a/HepLean/Tensors/ComplexLorentz/Basis.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basis.lean
@@ -79,11 +79,32 @@ lemma perm_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, LinearEquiv.ofLinear_apply]
   rw [basis_eq_FDiscrete]
 
+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))) : ℂ :=
+  (if (b i).val = (b (i.succAbove j)).val then (1 : ℂ) else 0)
+
+lemma contrBasisVectorMul_neg {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
+    {i : Fin n.succ.succ} {j : Fin n.succ} {b : Π k, Fin (complexLorentzTensor.repDim (c k))}
+    (h : ¬ (b i).val = (b (i.succAbove j)).val := by decide) :
+    contrBasisVectorMul i j b = 0 := by
+  rw [contrBasisVectorMul]
+  simp
+  exact h
+
+lemma contrBasisVectorMul_pos {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
+    {i : Fin n.succ.succ} {j : Fin n.succ} {b : Π k, Fin (complexLorentzTensor.repDim (c k))}
+    (h : (b i).val = (b (i.succAbove j)).val := by decide) :
+    contrBasisVectorMul i j b = 1 := by
+  rw [contrBasisVectorMul]
+  simp
+  exact h
+
 lemma contr_basisVector {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 = (if (b i).val = (b (i.succAbove j)).val
-    then (1 : ℂ) else 0) • basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
+    (contr i j h (tensorNode (basisVector c b))).tensor = (contrBasisVectorMul i j b) •
+    basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
     (fun k => b (i.succAbove (j.succAbove k))) := by
   rw [contr_tensor]
   simp only [Nat.succ_eq_add_one, tensorNode_tensor]
@@ -102,8 +123,7 @@ lemma contr_basisVector_tree  {n : ℕ} {c : Fin n.succ.succ → complexLorentzT
     {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 ((if (b i).val = (b (i.succAbove j)).val
-    then (1 : ℂ) else 0)) (tensorNode ( basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
+    (smul (contrBasisVectorMul i j b) (tensorNode ( basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
     (fun k => b (i.succAbove (j.succAbove k)))) )).tensor := by
   exact contr_basisVector _
 
@@ -113,7 +133,7 @@ lemma contr_basisVector_tree_pos  {n : ℕ} {c : Fin n.succ.succ → complexLore
     (contr i j h (tensorNode (basisVector c b))).tensor =
     ((tensorNode ( basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
     (fun k => b (i.succAbove (j.succAbove k)))))).tensor := by
-  rw [contr_basisVector_tree]
+  rw [contr_basisVector_tree, contrBasisVectorMul]
   rw [if_pos hn]
   simp [smul_tensor]
 
@@ -122,10 +142,11 @@ lemma contr_basisVector_tree_neg  {n : ℕ} {c : Fin n.succ.succ → complexLore
     (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]
+  rw [contr_basisVector_tree, contrBasisVectorMul]
   rw [if_neg hn]
   simp [smul_tensor]
 
+
 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)))
diff --git a/HepLean/Tensors/ComplexLorentz/Lemmas.lean b/HepLean/Tensors/ComplexLorentz/Lemmas.lean
index c8378f6..772ad51 100644
--- a/HepLean/Tensors/ComplexLorentz/Lemmas.lean
+++ b/HepLean/Tensors/ComplexLorentz/Lemmas.lean
@@ -119,7 +119,7 @@ And related results.
 -/
 open complexLorentzTensor
 
-def leftMetricMulRightMap := (Sum.elim ![Color.upL, Color.upL]  ![Color.upR, Color.upR]) ∘ finSumFinEquiv.symm
+def leftMetricMulRightMap := (Sum.elim ![Color.upL, Color.upL] ![Color.upR, Color.upR]) ∘ finSumFinEquiv.symm
 
 lemma leftMetric_mul_rightMetric : {Fermion.leftMetric | α α' ⊗ Fermion.rightMetric | β β'}ᵀ.tensor
     = basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
@@ -153,23 +153,64 @@ 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] ∘ ⇑finSumFinEquiv.symm) ∘
     Fin.succAbove 0 ∘ Fin.succAbove 1)
 
 abbrev pauliMatrixContrMap {n : ℕ} (c : Fin n → complexLorentzTensor.C) := (Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm)
 
-lemma pauliMatrix_contr_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C}
+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
+      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
+       (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
@@ -180,26 +221,7 @@ lemma pauliMatrix_contr_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C}
       (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_tensor_eq_snd <| pauliMatrix_basis_expand_tree]
-  rw [contr_tensor_eq <| prod_add _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <|  prod_add _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| prod_add _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| prod_add _ _ _]
-  rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _]
-  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  <| prod_add _ _ _]
-  /- Moving smuls. -/
-  rw [contr_tensor_eq  <| add_tensor_eq_snd  <| add_tensor_eq_snd  <| add_tensor_eq_snd
-    <| add_tensor_eq_snd <| add_tensor_eq_fst <| prod_smul _ _ _]
-  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 <| prod_smul _ _ _]
-  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_snd <| prod_smul _ _ _]
+  rw [contr_tensor_eq <| prod_pauliMatrix_basis_tree_expand _]
   /- Moving contr over add. -/
   rw [contr_add]
   rw [add_tensor_eq_snd <| contr_add _ _]
@@ -213,21 +235,32 @@ lemma pauliMatrix_contr_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C}
     <| 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 _ _]
+    <| 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 _ _]
+    <| 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 <|
+    add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
     contr_smul _ _]
-  rfl
 
-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 [pauliMatrix_contr_expand]
+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 _ _]
@@ -240,32 +273,68 @@ lemma pauliMatrix_contr_down_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_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
+  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_pos _ rfl]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_pos _ rfl]
+  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_neg _ ]
+    <| contr_basisVector_tree _]
   rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
+    <| 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_neg _]
+    <| 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_neg _]
+    <| 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_neg _]
+    <| 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_neg _]
-  /- Simplifying. -/
+     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 [smul_zero, add_zero]
+  simp only [one_smul, zero_smul, smul_zero, add_zero]
   congr 1
   · congr 1
     funext k
@@ -274,51 +343,28 @@ lemma pauliMatrix_contr_down_0 :
     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 : (contr 0 1 rfl
     (((tensorNode (basisVector ![Color.down, Color.down] fun x => 1)).prod
     (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
       PauliMatrix.asConsTensor)))).tensor
     = basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)
     + basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0) := by
-  rw [pauliMatrix_contr_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 _ _]
-  /- Contracting basis vectors. -/
-  rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| contr_basisVector_tree_pos _ rfl]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| contr_basisVector_tree_pos _ rfl]
-  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_neg _]
-  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_neg _]
-  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_neg _]
-  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_neg _]
-  /- Simplifying. -/
+  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 [smul_zero, add_zero, zero_add]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
   congr 1
   · congr 1
     funext k
@@ -341,45 +387,14 @@ lemma pauliMatrix_contr_down_2 : (contr 0 1 rfl
       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 [pauliMatrix_contr_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 _ _]
-  /- Contracting basis vectors. -/
-  rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  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_pos _]
-  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_pos _]
-  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_neg _]
-  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_neg _]
+  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 [smul_zero, add_zero, zero_add]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
   congr 1
   · congr 2
     funext k
@@ -388,51 +403,30 @@ lemma pauliMatrix_contr_down_2 : (contr 0 1 rfl
     funext k
     fin_cases k <;> rfl
 
+lemma pauliMatrix_contr_down_2_tree : (contr 0 1 rfl
+    (((tensorNode (basisVector ![Color.down, Color.down] fun x => 2)).prod
+    (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
+      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 : (contr 0 1 rfl
     (((tensorNode (basisVector ![Color.down, Color.down] fun x => 3)).prod
     (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
       PauliMatrix.asConsTensor)))).tensor
     =  basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)
     + (- 1 : ℂ) • basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by
-  rw [pauliMatrix_contr_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 _ _]
-  /- Contracting basis vectors. -/
-  rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  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_neg _]
-  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_neg _]
-  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_pos _]
-  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_pos _]
+  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 [smul_zero, add_zero, zero_add]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
   congr 1
   · congr 2
     funext k
@@ -441,6 +435,16 @@ lemma pauliMatrix_contr_down_3 : (contr 0 1 rfl
     funext k
     fin_cases k <;> rfl
 
+lemma pauliMatrix_contr_down_3_tree : (contr 0 1 rfl
+    (((tensorNode (basisVector ![Color.down, Color.down] fun x => 3)).prod
+    (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
+      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)
@@ -453,45 +457,14 @@ lemma pauliMatrix_contr_lower_0_0_0 :  (contr 0 2 rfl
     (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
     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 [pauliMatrix_contr_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 _ _]
-  /- Contracting basis vectors. -/
-  rw [add_tensor_eq_fst <| contr_basisVector_tree_pos _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_pos _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  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_neg _]
-  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_neg _]
-  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_neg _]
-  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_neg _]
+  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 [smul_zero, add_zero, zero_add]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
   congr 1
   · congr 1
     funext k
@@ -500,50 +473,19 @@ lemma pauliMatrix_contr_lower_0_0_0 :  (contr 0 2 rfl
     funext k
     fin_cases k <;> rfl
 
-lemma pauliMatrix_contr_lower_0_1_1 :  (contr 0 2 rfl
+lemma pauliMatrix_contr_lower_0_1_1 : (contr 0 2 rfl
     (((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1))).prod
     (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
     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 [pauliMatrix_contr_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 _ _]
-  /- Contracting basis vectors. -/
-  rw [add_tensor_eq_fst <| contr_basisVector_tree_pos _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_pos _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  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_neg _]
-  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_neg _]
-  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_neg _]
-  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_neg _]
+  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 [smul_zero, add_zero, zero_add]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
   congr 1
   · congr 1
     funext k
@@ -552,51 +494,19 @@ lemma pauliMatrix_contr_lower_0_1_1 :  (contr 0 2 rfl
     funext k
     fin_cases k <;> rfl
 
-
-lemma pauliMatrix_contr_lower_1_0_1 :  (contr 0 2 rfl
+lemma pauliMatrix_contr_lower_1_0_1 : (contr 0 2 rfl
     (((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1))).prod
     (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
     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 [pauliMatrix_contr_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 _ _]
-  /- Contracting basis vectors. -/
-  rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| contr_basisVector_tree_pos _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| contr_basisVector_tree_pos _]
-  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_neg _]
-  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_neg _]
-  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_neg _]
-  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_neg _]
+  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 [smul_zero, add_zero, zero_add]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
   congr 1
   · congr 1
     funext k
@@ -605,50 +515,19 @@ lemma pauliMatrix_contr_lower_1_0_1 :  (contr 0 2 rfl
     funext k
     fin_cases k <;> rfl
 
-lemma pauliMatrix_contr_lower_1_1_0 :  (contr 0 2 rfl
+lemma pauliMatrix_contr_lower_1_1_0 : (contr 0 2 rfl
     (((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0))).prod
     (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
     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 [pauliMatrix_contr_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 _ _]
-  /- Contracting basis vectors. -/
-  rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| contr_basisVector_tree_pos _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| contr_basisVector_tree_pos _]
-  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_neg _]
-  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_neg _]
-  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_neg _]
-  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_neg _]
+  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 [smul_zero, add_zero, zero_add]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
   congr 1
   · congr 1
     funext k
@@ -657,51 +536,20 @@ lemma pauliMatrix_contr_lower_1_1_0 :  (contr 0 2 rfl
     funext k
     fin_cases k <;> rfl
 
-lemma pauliMatrix_contr_lower_2_0_1 :  (contr 0 2 rfl
+lemma pauliMatrix_contr_lower_2_0_1 : (contr 0 2 rfl
     (((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1))).prod
     (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
     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 [pauliMatrix_contr_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 _ _]
-  /- Contracting basis vectors. -/
-  rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  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_pos _]
-  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_pos _]
-  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_neg _]
-  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_neg _]
+  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 [smul_zero, add_zero, zero_add]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
   congr 1
   · congr 2
     funext k
@@ -710,51 +558,20 @@ lemma pauliMatrix_contr_lower_2_0_1 :  (contr 0 2 rfl
     funext k
     fin_cases k <;> rfl
 
-lemma pauliMatrix_contr_lower_2_1_0 :  (contr 0 2 rfl
+lemma pauliMatrix_contr_lower_2_1_0 : (contr 0 2 rfl
     (((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0))).prod
     (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
     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 [pauliMatrix_contr_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 _ _]
-  /- Contracting basis vectors. -/
-  rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  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_pos _]
-  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_pos _]
-  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_neg _]
-  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_neg _]
+  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 [smul_zero, add_zero, zero_add]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
   congr 1
   · congr 2
     funext k
@@ -763,52 +580,21 @@ lemma pauliMatrix_contr_lower_2_1_0 :  (contr 0 2 rfl
     funext k
     fin_cases k <;> rfl
 
-
-lemma pauliMatrix_contr_lower_3_0_0 :  (contr 0 2 rfl
+lemma pauliMatrix_contr_lower_3_0_0 : (contr 0 2 rfl
     (((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0))).prod
     (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
     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 [pauliMatrix_contr_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 _ _]
-  /- Contracting basis vectors. -/
-  rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  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_neg _]
-  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_neg _]
-  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_pos _]
-  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_pos _]
+      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 [smul_zero, add_zero, zero_add]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
   congr 1
   · congr 2
     funext k
@@ -817,52 +603,20 @@ lemma pauliMatrix_contr_lower_3_0_0 :  (contr 0 2 rfl
     funext k
     fin_cases k <;> rfl
 
-
-lemma pauliMatrix_contr_lower_3_1_1 :  (contr 0 2 rfl
+lemma pauliMatrix_contr_lower_3_1_1 : (contr 0 2 rfl
     (((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1))).prod
     (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
     PauliMatrix.asConsTensor)))).tensor =
-       basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0)
+     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 [pauliMatrix_contr_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 _ _]
-  /- Contracting basis vectors. -/
-  rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
-    <| contr_basisVector_tree_neg _ ]
-  rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
-    <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
-  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_neg _]
-  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_neg _]
-  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_pos _]
-  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_pos _]
+  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 [smul_zero, add_zero, zero_add]
+  simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add]
   congr 1
   · congr 2
     funext k
@@ -871,18 +625,15 @@ lemma pauliMatrix_contr_lower_3_1_1 :  (contr 0 2 rfl
     funext k
     fin_cases k <;> rfl
 
-
-
-lemma pauliMatrix_lower :
-    {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
+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
+    - 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 _ _ _]
@@ -903,16 +654,117 @@ lemma pauliMatrix_lower :
   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. -/
-  sorry
+  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) +
+        (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1))))))))).tensor := by
+  rw [contr_tensor_eq <| prod_tensor_eq_fst <| pauliMatrix_lower_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 _ _ _]
+  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
-  = basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
-    - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0)
-    - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)
-    + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0)  := by
-  sorry
+  {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
 
 end
diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean
index bbb08ec..de66c36 100644
--- a/HepLean/Tensors/OverColor/Lift.lean
+++ b/HepLean/Tensors/OverColor/Lift.lean
@@ -286,7 +286,6 @@ lemma μ_tmul_tprod_mk {X Y : Type} {cX : X → C} {cY : Y → C}
   | Sum.inl i => rfl
   | Sum.inr i => rfl
 
-
 lemma μ_natural_left {X Y : OverColor C} (f : X ⟶ Y) (Z : OverColor C) :
     MonoidalCategory.whiskerRight (objMap' F f) (objObj' F Z) ≫ (μ F Y Z).hom =
     (μ F X Z).hom ≫ objMap' F (MonoidalCategory.whiskerRight f Z) := by
diff --git a/HepLean/Tensors/Tree/Basic.lean b/HepLean/Tensors/Tree/Basic.lean
index 42e19dd..63fcab3 100644
--- a/HepLean/Tensors/Tree/Basic.lean
+++ b/HepLean/Tensors/Tree/Basic.lean
@@ -680,7 +680,7 @@ lemma eval_tensor {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : ℕ)
     (eval i e t).tensor = (S.evalMap i (Fin.ofNat' e Fin.size_pos')) t.tensor := rfl
 
 lemma smul_tensor {c : Fin n → S.C} (a : S.k) (T : TensorTree S c) :
-    (smul a  T).tensor = a • T.tensor:= rfl
+    (smul a T).tensor = a • T.tensor:= rfl
 /-!
 
 ## Equality of tensors and rewrites.