diff --git a/HepLean/SpaceTime/WeylFermion/Contraction.lean b/HepLean/SpaceTime/WeylFermion/Contraction.lean
index 38968f6..1ac898b 100644
--- a/HepLean/SpaceTime/WeylFermion/Contraction.lean
+++ b/HepLean/SpaceTime/WeylFermion/Contraction.lean
@@ -203,7 +203,8 @@ lemma rightAltContraction_hom_tmul (ψ : rightHanded) (φ : altRightHanded) :
   rfl
 
 lemma rightAltContraction_basis (i j : Fin 2) :
-    rightAltContraction.hom (rightBasis i ⊗ₜ altRightBasis j) = if i.1 = j.1 then (1 : ℂ) else 0 := by
+    rightAltContraction.hom (rightBasis i ⊗ₜ altRightBasis j) =
+    if i.1 = j.1 then (1 : ℂ) else 0 := by
   rw [rightAltContraction_hom_tmul]
   simp only [Action.instMonoidalCategory_tensorUnit_V, rightBasis_toFin2ℂ, altRightBasis_toFin2ℂ,
     dotProduct_single, mul_one]
@@ -242,7 +243,8 @@ lemma altRightContraction_hom_tmul (φ : altRightHanded) (ψ : rightHanded) :
   rfl
 
 lemma altRightContraction_basis (i j : Fin 2) :
-    altRightContraction.hom (altRightBasis i ⊗ₜ rightBasis j) = if i.1 = j.1 then (1 : ℂ) else 0 := by
+    altRightContraction.hom (altRightBasis i ⊗ₜ rightBasis j) =
+    if i.1 = j.1 then (1 : ℂ) else 0 := by
   rw [altRightContraction_hom_tmul]
   simp only [Action.instMonoidalCategory_tensorUnit_V, rightBasis_toFin2ℂ, altRightBasis_toFin2ℂ,
     dotProduct_single, mul_one]
diff --git a/HepLean/SpaceTime/WeylFermion/Two.lean b/HepLean/SpaceTime/WeylFermion/Two.lean
index fa1a046..4bfebaf 100644
--- a/HepLean/SpaceTime/WeylFermion/Two.lean
+++ b/HepLean/SpaceTime/WeylFermion/Two.lean
@@ -125,7 +125,8 @@ def altRightAltRightToMatrix : (altRightHanded ⊗ altRightHanded).V ≃ₗ[ℂ]
 
 /-- Expanding `altRightAltRightToMatrix` in terms of the standard basis. -/
 lemma altRightAltRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
-    altRightAltRightToMatrix.symm M = ∑ i, ∑ j, M i j • (altRightBasis i ⊗ₜ[ℂ] altRightBasis j) := by
+    altRightAltRightToMatrix.symm M =
+    ∑ i, ∑ j, M i j • (altRightBasis i ⊗ₜ[ℂ] altRightBasis j) := by
   simp only [Action.instMonoidalCategory_tensorObj_V, altRightAltRightToMatrix,
     LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
diff --git a/HepLean/Tensors/ComplexLorentz/Lemmas.lean b/HepLean/Tensors/ComplexLorentz/Lemmas.lean
index 772ad51..1567bba 100644
--- a/HepLean/Tensors/ComplexLorentz/Lemmas.lean
+++ b/HepLean/Tensors/ComplexLorentz/Lemmas.lean
@@ -119,7 +119,8 @@ 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)
@@ -141,7 +142,7 @@ lemma leftMetric_mul_rightMetric : {Fermion.leftMetric | α α' ⊗ Fermion.righ
   rw [add_tensor_eq_snd <| add_tensor_eq_snd <| prod_basisVector_tree _ _]
   rw [← add_assoc]
   simp only [add_tensor, smul_tensor, tensorNode_tensor]
-  change _ =  basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
+  change _ = basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
     +- basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0)
     +- basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)
     + basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0)
@@ -153,10 +154,11 @@ 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)
+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)
+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) :
@@ -164,12 +166,12 @@ lemma prod_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentz
       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
+      (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
+      (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
+    ((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
@@ -180,7 +182,7 @@ lemma prod_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentz
         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 <| 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 <|
@@ -188,39 +190,41 @@ lemma prod_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentz
   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 _ _ _]
+    <| 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
+  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 <| 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
+    (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
+      (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
+    ((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
+      (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]
@@ -244,12 +248,15 @@ lemma contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorent
 
 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))) :
+    (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
+      ((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
@@ -276,31 +283,41 @@ lemma basis_contr_pauliMatrix_basis_tree_expand' {n : ℕ} {c : Fin n → comple
   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
+  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))) :
+    (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))
+        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 (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']
@@ -319,8 +336,8 @@ lemma basis_contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complex
   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 _]
+    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
@@ -344,7 +361,7 @@ lemma pauliMatrix_contr_down_0 :
     fin_cases k <;> rfl
 
 lemma pauliMatrix_contr_down_0_tree :
-     (contr 0 1 rfl (((tensorNode (basisVector ![Color.down, Color.down] fun x => 0)).prod
+    (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
@@ -352,10 +369,9 @@ lemma pauliMatrix_contr_down_0_tree :
     (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
+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]
@@ -373,20 +389,19 @@ lemma pauliMatrix_contr_down_1 : (contr 0 1 rfl
     funext k
     fin_cases k <;> rfl
 
-lemma pauliMatrix_contr_down_1_tree : (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
-    = (TensorTree.add (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)))
+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 : (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
+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
+    + (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,
@@ -403,21 +418,19 @@ 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 =
+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 : (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)
+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,
@@ -435,27 +448,23 @@ 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 =
+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
+      (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)
+  ((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 :  (contr 0 2 rfl
-    (((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 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)
+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,
@@ -473,10 +482,10 @@ 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
-    (((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)
+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,
@@ -494,10 +503,10 @@ 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
-    (((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)
+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,
@@ -515,10 +524,10 @@ 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
-    (((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)
+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,
@@ -536,12 +545,12 @@ 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
-    (((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1))).prod
-    (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
-    PauliMatrix.asConsTensor)))).tensor =
+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
+    + (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,
@@ -558,12 +567,12 @@ 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
-    (((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0))).prod
-    (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
-    PauliMatrix.asConsTensor)))).tensor =
+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
+    + (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,
@@ -580,13 +589,12 @@ 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
-    (((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
+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,
@@ -603,12 +611,12 @@ 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
-    (((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)
-    + (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by
+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,
@@ -656,8 +664,10 @@ lemma pauliMatrix_lower : {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor
   /- 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]
+  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,
@@ -686,7 +696,8 @@ lemma pauliMatrix_lower_tree : {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsT
   rfl
 
 lemma pauliMatrix_contract_pauliMatrix_aux :
-  {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗ PauliMatrix.asConsTensor | ν α' β'}ᵀ.tensor
+  {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
@@ -701,57 +712,89 @@ lemma pauliMatrix_contract_pauliMatrix_aux :
       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
+        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
+        (-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
+        (-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 _ _ _]
+  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 _ _ _]
+  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 _ _]
+  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 _ _]
+  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]
+  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 =
+  {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)
@@ -762,7 +805,7 @@ lemma pauliMatrix_contract_pauliMatrix :
     neg_mul, _root_.neg_neg]
   ring_nf
   rw [Complex.I_sq]
-  simp only [ neg_smul, one_smul, _root_.neg_neg]
+  simp only [neg_smul, one_smul, _root_.neg_neg]
   abel
 
 end Fermion
diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean
index de66c36..50e78ec 100644
--- a/HepLean/Tensors/OverColor/Lift.lean
+++ b/HepLean/Tensors/OverColor/Lift.lean
@@ -207,6 +207,8 @@ def discreteSumEquiv {X Y : OverColor C} (i : X.left ⊕ Y.left) :
   | Sum.inl _ => LinearEquiv.refl _ _
   | 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`.  -/
 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)) :=
@@ -271,7 +273,8 @@ lemma μ_tmul_tprod {X Y : OverColor C} (p : (i : X.left) → F.obj (Discrete.mk
 lemma μ_tmul_tprod_mk {X Y : Type} {cX : X → C} {cY : Y → C}
     (p : (i : X) → F.obj (Discrete.mk <| cX i))
     (q : (i : Y) → (F.obj <| Discrete.mk (cY i))) :
-    (μ F (OverColor.mk cX) (OverColor.mk cY)).hom.hom (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q)
+    (μ F (OverColor.mk cX) (OverColor.mk cY)).hom.hom
+    (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q)
     = (PiTensorProduct.tprod k) fun i =>
     discreteSumEquiv' F i (HepLean.PiTensorProduct.elimPureTensor p q i) := by
   let q' : (i : (OverColor.mk cY).left) → (F.obj <| Discrete.mk ((OverColor.mk cY).hom i)) := q
diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean
index 885302c..51e8ad5 100644
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@@ -152,8 +152,11 @@ def getNoIndicesExact (stx : Syntax) : TermElabM ℕ := do
     | Expr.app _ (Expr.app _ (Expr.app _ c)) =>
       let typeC ← inferType c
       match typeC with
-      | Expr.forallE _ (Expr.app _ (Expr.app (Expr.app _ (Expr.lit (Literal.natVal n))) _)) _ _ =>
-        return n
+      | Expr.forallE _ (Expr.app _ a) _ _ =>
+        let a' ← whnf a
+        match a' with
+        | Expr.lit (Literal.natVal n) => return n
+        |_ => throwError "Could not extract number of indices from tensor (getNoIndicesExact). "
       | _ => throwError "Could not extract number of indices from tensor (getNoIndicesExact). "
     | _ => return 1
   | k => return k
@@ -248,11 +251,7 @@ def termNodeSyntax (T : Term) : TermElabM Term := do
   | _ =>
   match type with
   | Expr.app _ (Expr.app _ (Expr.app _ c)) =>
-    let typeC ← inferType c
-    match typeC with
-    | Expr.forallE _ (Expr.app _ (Expr.app (Expr.app _ (Expr.lit (Literal.natVal _))) _)) _ _ =>
       return Syntax.mkApp (mkIdent ``TensorTree.tensorNode) #[T]
-    | _ => throwError "Could not create terminal node syntax (termNodeSyntax). "
   | _ => return Syntax.mkApp (mkIdent ``TensorTree.vecNode) #[T]
 
 /-- Adjusts a list `List ℕ` by subtracting from each natrual number the number
@@ -547,5 +546,14 @@ elab_rules (kind:=tensorExprSyntax) : term
   | `(term| {$e:tensorExpr}ᵀ) => do
     let tensorTree ← elaborateTensorNode e
     return tensorTree
+/-!
 
+## Test cases
+
+-/
+
+variable {S : TensorSpecies} {c : Fin (Nat.succ (Nat.succ 0)) → S.C} {t : S.F.obj (OverColor.mk c)}
+/-
+#check {t | α β}ᵀ
+-/
 end TensorTree
diff --git a/scripts/hepLean_style_lint.lean b/scripts/hepLean_style_lint.lean
index 3dc6587..a708881 100644
--- a/scripts/hepLean_style_lint.lean
+++ b/scripts/hepLean_style_lint.lean
@@ -52,6 +52,14 @@ def doubleSpaceLinter : HepLeanTextLinter := fun lines ↦ Id.run do
     else none)
   errors.toArray
 
+def longLineLinter : HepLeanTextLinter := fun lines ↦ Id.run do
+  let enumLines := (lines.toList.enumFrom 1)
+  let errors := enumLines.filterMap (fun (lno, l) ↦
+    if l.length > 100 ∧ ¬ String.containsSubstr l "http" then
+      some (s!" Line is too long.", lno, 100)
+    else none)
+  errors.toArray
+
 /-- Substring linter. -/
 def substringLinter (s : String) : HepLeanTextLinter := fun lines ↦ Id.run do
   let enumLines := (lines.toList.enumFrom 1)
@@ -93,7 +101,7 @@ def hepLeanLintFile (path : FilePath) : IO (Array HepLeanErrorContext) := do
   let lines ← IO.FS.lines path
   let allOutput := (Array.map (fun lint ↦
     (Array.map (fun (e, n, c) ↦ HepLeanErrorContext.mk e n c path)) (lint lines)))
-    #[doubleEmptyLineLinter, doubleSpaceLinter, numInitialSpacesEven,
+    #[doubleEmptyLineLinter, doubleSpaceLinter, numInitialSpacesEven, longLineLinter,
     substringLinter ".-/", substringLinter " )",
     substringLinter "( ", substringLinter "=by", substringLinter "  def ",
     substringLinter "/-- We ", substringLinter "[ ", substringLinter " ]", substringLinter " ,"