diff --git a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
index 38dd7a1..4f5e33a 100644
--- a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
@@ -3,8 +3,13 @@ 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.PauliMatrices.Basic
 import HepLean.Tensors.Tree.NodeIdentities.ProdContr
+import HepLean.Tensors.Tree.NodeIdentities.PermContr
+import HepLean.Tensors.Tree.NodeIdentities.PermProd
+import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
+import HepLean.Tensors.Tree.NodeIdentities.ContrContr
+import HepLean.Tensors.Tree.NodeIdentities.ProdComm
 import HepLean.Tensors.Tree.NodeIdentities.Congr
 import HepLean.Tensors.Tree.NodeIdentities.ProdAssoc
 /-!
@@ -28,145 +33,59 @@ noncomputable section
 namespace complexLorentzTensor
 open Lorentz
 
+/-!
+
+## Definitions
+
+-/
+
 /-- A bispinor `pᵃᵃ` created from a lorentz vector `p^μ`. -/
 def contrBispinorUp (p : complexContr) :=
-  {p | μ ⊗ pauliCo | μ α β}ᵀ.tensor
-
-lemma tensorNode_contrBispinorUp (p : complexContr) :
-    (tensorNode (contrBispinorUp p)).tensor = {p | μ ⊗ pauliCo | μ α β}ᵀ.tensor := by
-  rw [contrBispinorUp, tensorNode_tensor]
-
-/-- An up-bispinor is equal to `pauliCo | μ α β ⊗ p | μ`-/
-lemma contrBispinorUp_eq_pauliCo_self (p : complexContr) :
-    {contrBispinorUp p | α β = pauliCo | μ α β ⊗ p | μ}ᵀ := by
-  rw [tensorNode_contrBispinorUp]
-  conv_lhs =>
-    rw [contr_tensor_eq <| prod_comm _ _ _ _]
-    rw [perm_contr]
-    rw [perm_tensor_eq <| contr_swap _ _]
-    rw [perm_perm]
-  apply perm_congr
-  · apply OverColor.Hom.ext
-    ext x
-    match x with
-    | (0 : Fin 2) => rfl
-    | (1 : Fin 2)  => rfl
-  · rfl
-
-set_option maxRecDepth 2000 in
-lemma altRightMetric_contr_contrBispinorUp_assoc (p : complexContr) :
-    {Fermion.altRightMetric | β β' ⊗ contrBispinorUp p | α β =
-    Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β ⊗ p | μ}ᵀ := by
-  conv_lhs =>
-    rw [contr_tensor_eq <| prod_tensor_eq_snd <| contrBispinorUp_eq_pauliCo_self _]
-    rw [contr_tensor_eq <| prod_perm_right  _ _ _ _]
-    rw [perm_contr]
-    rw [perm_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _]
-    rw [perm_tensor_eq <| perm_contr _ _]
-    rw [perm_perm]
-    erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| prod_assoc _ _ _ _ _ _]
-    rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
-    rw [perm_tensor_eq <| perm_contr _ _]
-    rw [perm_perm]
-  conv_rhs =>
-    rw [perm_tensor_eq <| contr_tensor_eq <| contr_prod _ _ _]
-    rw [perm_tensor_eq <| perm_contr _ _]
-    rw [perm_perm]
-    erw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
-    rw [perm_tensor_eq <| perm_contr _ _]
-    rw [perm_perm]
-    rw [perm_tensor_eq <| contr_contr _ _ _]
-    rw [perm_perm]
-  apply perm_congr (_) rfl
-  · apply OverColor.Hom.fin_ext
-    intro i
-    fin_cases i
-    exact rfl
-    exact rfl
+  {pauliCo | μ α β ⊗ p | μ}ᵀ.tensor
 
 /-- A bispinor `pₐₐ` created from a lorentz vector `p^μ`. -/
 def contrBispinorDown (p : complexContr) :=
   {Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗
-    (contrBispinorUp p) | α β}ᵀ.tensor
+  contrBispinorUp p | α β}ᵀ.tensor
 
-/-- Expands the tensor node of `contrBispinorDown` into a tensor tree based on
-  `contrBispinorUp`. -/
+/-- A bispinor `pᵃᵃ` created from a lorentz vector `p_μ`. -/
+def coBispinorUp (p : complexCo) :=
+  {pauliContr | μ α β ⊗ p | μ}ᵀ.tensor
+
+/-- A bispinor `pₐₐ` created from a lorentz vector `p_μ`. -/
+def coBispinorDown (p : complexCo) :=
+  {Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗
+  coBispinorUp p | α β}ᵀ.tensor
+
+/-!
+
+## Tensor nodes
+
+-/
+
+/-- The definitional tensor node relation for `contrBispinorUp`. -/
+lemma tensorNode_contrBispinorUp (p : complexContr) :
+    {contrBispinorUp p | α β}ᵀ.tensor = {pauliCo | μ α β ⊗ p | μ}ᵀ.tensor := by
+  rw [contrBispinorUp, tensorNode_tensor]
+
+/-- The definitional tensor node relation for `contrBispinorDown`. -/
 lemma tensorNode_contrBispinorDown (p : complexContr) :
-    {contrBispinorDown p | α β}ᵀ.tensor = {Fermion.altLeftMetric | α α' ⊗
-    Fermion.altRightMetric | β β' ⊗ (contrBispinorUp p) | α β}ᵀ.tensor := by
+    {contrBispinorDown p | α β}ᵀ.tensor =
+    {Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β'
+    ⊗ contrBispinorUp p | α β}ᵀ.tensor := by
   rw [contrBispinorDown, tensorNode_tensor]
 
-set_option maxRecDepth 10000 in
-lemma contrBispinorDown_eq_metric_contr_contrBispinorUp  (p : complexContr) :
-    {contrBispinorDown p | α' β' = Fermion.altLeftMetric | α α' ⊗
-    (Fermion.altRightMetric | β β' ⊗ contrBispinorUp p | α β)}ᵀ := by
-  rw [tensorNode_contrBispinorDown]
-  conv_lhs =>
-    rw [contr_tensor_eq <| contr_tensor_eq <| prod_assoc' _ _ _ _ _ _]
-    rw [contr_tensor_eq <| perm_contr _ _]
-    rw [perm_contr]
-    rw [perm_tensor_eq <| contr_contr _ _ _]
-    rw [perm_perm]
-  conv_rhs =>
-    rw [perm_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _ ]
-    rw [perm_tensor_eq <| perm_contr _ _]
-    rw [perm_perm]
-  apply perm_congr
-  · apply OverColor.Hom.ext
-    ext x
-    match x with
-    | (0 : Fin 2) => rfl
-    | (1 : Fin 2) => rfl
-  · rfl
+/-- The definitional tensor node relation for `coBispinorUp`. -/
+lemma tensorNode_coBispinorUp  (p : complexCo) :
+    {coBispinorUp p | α β}ᵀ.tensor = {pauliContr | μ α β ⊗ p | μ}ᵀ.tensor := by
+  rw [coBispinorUp, tensorNode_tensor]
 
-/- TODO: Remove maxHeartbeats from this result. -/
-set_option maxHeartbeats 400000 in
-set_option maxRecDepth 2000 in
-lemma contrBispinorDown_eq_contr_with_self (p : complexContr) :
-    {contrBispinorDown p | α' β' = (Fermion.altLeftMetric | α α' ⊗
-    (Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β)) ⊗ p | μ}ᵀ := by
-  rw [contrBispinorDown_eq_metric_contr_contrBispinorUp]
-  conv_lhs =>
-    rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| altRightMetric_contr_contrBispinorUp_assoc _]
-    rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_right _ _ _ _]
-    rw [perm_tensor_eq <| perm_contr _ _ ]
-    rw [perm_perm]
-    rw [perm_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _]
-    rw [perm_tensor_eq <| perm_contr _ _]
-    rw [perm_perm]
-    erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <|
-        prod_assoc _ _ _ _ _ _]
-    rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
-    rw [perm_tensor_eq <| perm_contr _ _]
-    rw [perm_perm]
-  conv =>
-    rhs
-    rw [perm_tensor_eq <| contr_tensor_eq <| contr_prod _ _ _]
-    rw [perm_tensor_eq <| perm_contr _ _]
-    rw [perm_perm]
-    erw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
-    rw [perm_tensor_eq <| perm_contr _ _]
-    rw [perm_perm]
-    rw [perm_tensor_eq <| contr_contr _ _ _]
-    rw [perm_perm]
-  apply congrArg
-  apply congrFun
-  apply congrArg
-  apply OverColor.Hom.fin_ext
-  intro i
-  fin_cases i
-  · exact rfl
-  · exact rfl
-
-/-- Expansion of a `contrBispinorDown` into the original contravariant tensor nested
-  between pauli matrices and metrics. -/
-lemma contrBispinorDown_eq_metric_mul_self_mul_pauli (p : complexContr) :
-    {contrBispinorDown p | α β}ᵀ.tensor = {Fermion.altLeftMetric | α α' ⊗
-    Fermion.altRightMetric | β β' ⊗ (p | μ ⊗ pauliCo | μ α β)}ᵀ.tensor := by
-  conv =>
-    lhs
-    rw [tensorNode_contrBispinorDown]
-    rw [contr_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| tensorNode_contrBispinorUp p]
+/-- The definitional tensor node relation for `coBispinorDown`. -/
+lemma tensorNode_coBispinorDown (p : complexCo) :
+    {coBispinorDown p | α β}ᵀ.tensor =
+    {Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β'
+    ⊗ coBispinorUp p | α β}ᵀ.tensor := by
+  rw [coBispinorDown, tensorNode_tensor]
 
 end complexLorentzTensor
 end
diff --git a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean
index b5d2a9f..ed06882 100644
--- a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean
@@ -33,19 +33,19 @@ open Fermion
 
 -/
 
-/- The Pauli matrices as `σ^μ^α^{dot β}`. -/
+/- The Pauli matrices as the complex Lorentz tensor `σ^μ^α^{dot β}`. -/
 def pauliContr := {PauliMatrix.asConsTensor | ν α β}ᵀ.tensor
 
-/-- The Pauli matrices as `σ_μ^α^{dot β}`. -/
+/-- The Pauli matrices as the complex Lorentz tensor `σ_μ^α^{dot β}`. -/
 def pauliCo := {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | ν α β}ᵀ.tensor
 
-/-- The Pauli matrices as `σ_μ_α_{dot β}`. -/
-def pauliCoDown := {Fermion.altLeftMetric | α α' ⊗
-  Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β}ᵀ.tensor
+/-- The Pauli matrices as the complex Lorentz tensor `σ_μ_α_{dot β}`. -/
+def pauliCoDown := {pauliCo | μ α β ⊗ Fermion.altLeftMetric | α α' ⊗
+  Fermion.altRightMetric | β β'}ᵀ.tensor
 
-/-- The Pauli matrices as `σ^μ_α_{dot β}`. -/
-def pauliContrDown := {Fermion.altLeftMetric | α α' ⊗
-  Fermion.altRightMetric | β β' ⊗ pauliContr | μ α β}ᵀ.tensor
+/-- The Pauli matrices as the complex Lorentz tensor `σ^μ_α_{dot β}`. -/
+def pauliContrDown := {pauliContr | μ α β ⊗ Fermion.altLeftMetric | α α' ⊗
+  Fermion.altRightMetric | β β'}ᵀ.tensor
 
 /-!
 
@@ -65,14 +65,14 @@ lemma tensorNode_pauliCo : {pauliCo | μ α β}ᵀ.tensor  =
 
 /-- The definitional tensor node relation for `pauliCoDown`. -/
 lemma tensorNode_pauliCoDown : {pauliCoDown | μ α β}ᵀ.tensor =
-    {Fermion.altLeftMetric | α α' ⊗
-    Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β}ᵀ.tensor := by
+    {pauliCo | μ α β ⊗ Fermion.altLeftMetric | α α' ⊗
+    Fermion.altRightMetric | β β'}ᵀ.tensor := by
   rfl
 
 /-- The definitional tensor node relation for `pauliContrDown`. -/
 lemma tensorNode_pauliContrDown : {pauliContrDown | μ α β}ᵀ.tensor =
-    {Fermion.altLeftMetric | α α' ⊗
-    Fermion.altRightMetric | β β' ⊗ pauliContr | μ α β}ᵀ.tensor := by
+    {pauliContr | μ α β ⊗ Fermion.altLeftMetric | α α' ⊗
+    Fermion.altRightMetric | β β'}ᵀ.tensor := by
   rfl
 
 end complexLorentzTensor