diff --git a/HepLean/Tensors/ComplexLorentz/BasisTrees.lean b/HepLean/Tensors/ComplexLorentz/BasisTrees.lean
index 542a127..1285c6d 100644
--- a/HepLean/Tensors/ComplexLorentz/BasisTrees.lean
+++ b/HepLean/Tensors/ComplexLorentz/BasisTrees.lean
@@ -177,6 +177,8 @@ lemma basis_contr_pauliMatrix_basis_tree_expand' {n : ℕ} {c : Fin n → comple
     <| contr_tensor_eq <| prod_basisVector_tree _ _]
   rfl
 
+/-- The map to color which appears when contracting a basis vector with
+  puali matrices. -/
 def pauliMatrixBasisProdMap
     {n : ℕ} {c : Fin n → complexLorentzTensor.C}
     (b : Π k, Fin (complexLorentzTensor.repDim (c k))) (i1 i2 i3 : Fin 4) :
@@ -186,6 +188,8 @@ def pauliMatrixBasisProdMap
       ((HepLean.PiTensorProduct.elimPureTensor b (fun | (0 : Fin 3) => i1 | 1 => i2 | 2 => i3))
       (finSumFinEquiv.symm i))
 
+/-- The new basis vectors which appear when contracting pauli matrices with
+  basis vectors. -/
 def basisVectorContrPauli {n : ℕ} {c : Fin n → complexLorentzTensor.C}
     (i : Fin (n + 3)) (j : Fin (n +2))
     (b : Π k, Fin (complexLorentzTensor.repDim (c k)))
diff --git a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
index a76bfac..035e527 100644
--- a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
@@ -25,7 +25,7 @@ noncomputable section
 namespace complexLorentzTensor
 open Lorentz
 
-/-- A bispinor `pᵃᵃ` created from a lorentz vector  `p^μ`. -/
+/-- A bispinor `pᵃᵃ` created from a lorentz vector `p^μ`. -/
 def contrBispinorUp (p : complexContr) :=
   {p | μ ⊗ pauliCo | μ α β}ᵀ.tensor
 
@@ -33,7 +33,7 @@ lemma tensorNode_contrBispinorUp (p : complexContr) :
     (tensorNode (contrBispinorUp p)).tensor = {p | μ ⊗ pauliCo | μ α β}ᵀ.tensor := by
   rw [contrBispinorUp, tensorNode_tensor]
 
-/-- A bispinor `pₐₐ` created from a lorentz vector  `p^μ`. -/
+/-- A bispinor `pₐₐ` created from a lorentz vector `p^μ`. -/
 def contrBispinorDown (p : complexContr) :=
   {Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗
     (contrBispinorUp p) | α β}ᵀ.tensor
diff --git a/HepLean/Tensors/ComplexLorentz/PauliContr.lean b/HepLean/Tensors/ComplexLorentz/PauliContr.lean
index fd091ee..79c8c5e 100644
--- a/HepLean/Tensors/ComplexLorentz/PauliContr.lean
+++ b/HepLean/Tensors/ComplexLorentz/PauliContr.lean
@@ -506,7 +506,7 @@ lemma pauliCo_contr_pauliContr_expand :
     + 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]
+  rw [pauliCo_contr_pauliContr_expand_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]
@@ -519,7 +519,7 @@ lemma pauliCo_contr_pauliContr_expand :
 theorem pauliCo_contr_pauliContr :
     {pauliCo | ν α β ⊗ PauliMatrix.asConsTensor | ν α' β' =
     2 •ₜ Fermion.leftMetric | α α' ⊗ Fermion.rightMetric | β β'}ᵀ := by
-  rw [pauliMatrix_contract_pauliMatrix_expand]
+  rw [pauliCo_contr_pauliContr_expand]
   rw [perm_tensor_eq <| smul_tensor_eq <| leftMetric_mul_rightMetric_tree]
   rw [perm_smul]
   /- Moving perm through adds. -/
diff --git a/HepLean/Tensors/ComplexLorentz/PauliLower.lean b/HepLean/Tensors/ComplexLorentz/PauliLower.lean
index ed5fcaf..e8ebeb8 100644
--- a/HepLean/Tensors/ComplexLorentz/PauliLower.lean
+++ b/HepLean/Tensors/ComplexLorentz/PauliLower.lean
@@ -25,6 +25,7 @@ noncomputable section
 namespace Fermion
 open complexLorentzTensor
 
+/-- The pauli matrices as `σ_μ^α^{dot β}`. -/
 def pauliCo := {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | ν α β}ᵀ.tensor
 
 lemma tensorNode_pauliCo : (tensorNode pauliCo).tensor =