diff --git a/HepLean/Tensors/ComplexLorentz/Basis.lean b/HepLean/Tensors/ComplexLorentz/Basis.lean
index a3ff81c..3acf860 100644
--- a/HepLean/Tensors/ComplexLorentz/Basis.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basis.lean
@@ -38,7 +38,7 @@ namespace complexLorentzTensor
 
 /-- Basis vectors for complex Lorentz tensors. -/
 def basisVector {n : ℕ} (c : Fin n → complexLorentzTensor.C)
-  (b : Π j, Fin (complexLorentzTensor.repDim (c j))) :
+    (b : Π j, Fin (complexLorentzTensor.repDim (c j))) :
     complexLorentzTensor.F.obj (OverColor.mk c) :=
   PiTensorProduct.tprod ℂ (fun i => complexLorentzTensor.basis (c i) (b i))
 
diff --git a/HepLean/Tensors/ComplexLorentz/PauliContr.lean b/HepLean/Tensors/ComplexLorentz/PauliContr.lean
index 4424299..d65380d 100644
--- a/HepLean/Tensors/ComplexLorentz/PauliContr.lean
+++ b/HepLean/Tensors/ComplexLorentz/PauliContr.lean
@@ -237,9 +237,9 @@ private lemma pauliMatrix_lower_basis_expand_prod' {n : ℕ} {c : Fin n → comp
     exact pauliMatrix_lower_basis_expand_prod _
 
 lemma pauliMatrix_contract_pauliMatrix_aux :
-  {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗
+    {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗
     PauliMatrix.asConsTensor | ν α' β'}ᵀ.tensor
-  = ((tensorNode
+    = ((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
@@ -310,8 +310,8 @@ lemma pauliMatrix_contract_pauliMatrix_aux :
     pauliMatrix_contr_lower_3_1_1]
 
 lemma pauliMatrix_contract_pauliMatrix_expand :
-  {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)
diff --git a/HepLean/Tensors/ComplexLorentz/PauliLower.lean b/HepLean/Tensors/ComplexLorentz/PauliLower.lean
index f801f10..d84422e 100644
--- a/HepLean/Tensors/ComplexLorentz/PauliLower.lean
+++ b/HepLean/Tensors/ComplexLorentz/PauliLower.lean
@@ -139,7 +139,7 @@ lemma pauliMatrix_contr_down_3 :
     fin_cases k <;> rfl
 
 lemma pauliMatrix_contr_down_3_tree : {(basisVector ![Color.down, Color.down] fun x => 3) | μ ν ⊗
-      PauliMatrix.asConsTensor | μ α β}ᵀ.tensor =
+    PauliMatrix.asConsTensor | μ α β}ᵀ.tensor =
     (TensorTree.add
       ((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0))))
       (smul (-1) (tensorNode (basisVector pauliMatrixLowerMap
diff --git a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
index dbe3ec7..2553c16 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
@@ -203,7 +203,7 @@ lemma smul_prod {n m: ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
   simp [prod_tensor, smul_tensor, tmul_smul, smul_tmul, map_smul]
 
 lemma prod_smul {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
-  (a : S.k) (t1 : TensorTree S c) (t2 : TensorTree S c1) :
+    (a : S.k) (t1 : TensorTree S c) (t2 : TensorTree S c1) :
     (prod t1 (smul a t2)).tensor = (smul a (prod t1 t2)).tensor := by
   simp [prod_tensor, smul_tensor, tmul_smul, smul_tmul, map_smul]