From f2eaa2ee433fbd41988cf1ef523e07489d007ddb Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 25 Oct 2024 13:54:58 +0000
Subject: [PATCH] refactor: Lint

---
 HepLean/Tensors/ComplexLorentz/Basic.lean     |  1 -
 .../Tensors/ComplexLorentz/BasisTrees.lean    | 57 +++++++++----------
 .../Tensors/ComplexLorentz/PauliLower.lean    |  3 +-
 HepLean/Tensors/Tree/Basic.lean               | 10 ++--
 4 files changed, 33 insertions(+), 38 deletions(-)

diff --git a/HepLean/Tensors/ComplexLorentz/Basic.lean b/HepLean/Tensors/ComplexLorentz/Basic.lean
index 0cc1723..484bf44 100644
--- a/HepLean/Tensors/ComplexLorentz/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basic.lean
@@ -209,6 +209,5 @@ lemma basis_contr (c : complexLorentzTensor.C) (i : Fin (complexLorentzTensor.re
   | Color.up => Lorentz.contrCoContraction_basis _ _
   | Color.down => Lorentz.coContrContraction_basis _ _
 
-
 end complexLorentzTensor
 end
diff --git a/HepLean/Tensors/ComplexLorentz/BasisTrees.lean b/HepLean/Tensors/ComplexLorentz/BasisTrees.lean
index 9dd69eb..542a127 100644
--- a/HepLean/Tensors/ComplexLorentz/BasisTrees.lean
+++ b/HepLean/Tensors/ComplexLorentz/BasisTrees.lean
@@ -177,7 +177,6 @@ lemma basis_contr_pauliMatrix_basis_tree_expand' {n : ℕ} {c : Fin n → comple
     <| contr_tensor_eq <| prod_basisVector_tree _ _]
   rfl
 
-
 def pauliMatrixBasisProdMap
     {n : ℕ} {c : Fin n → complexLorentzTensor.C}
     (b : Π k, Fin (complexLorentzTensor.repDim (c k))) (i1 i2 i3 : Fin 4) :
@@ -190,10 +189,11 @@ def pauliMatrixBasisProdMap
 def basisVectorContrPauli {n : ℕ} {c : Fin n → complexLorentzTensor.C}
     (i : Fin (n + 3)) (j : Fin (n +2))
     (b : Π k, Fin (complexLorentzTensor.repDim (c k)))
-    (i1 i2 i3 : Fin 4)  :=
+    (i1 i2 i3 : Fin 4) :=
   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) := fun k => (pauliMatrixBasisProdMap b i1 i2 i3) (i.succAbove (j.succAbove k))
+  let b' (i1 i2 i3 : Fin 4) := fun k => (pauliMatrixBasisProdMap b i1 i2 i3)
+    (i.succAbove (j.succAbove k))
   basisVector c' (b' i1 i2 i3)
 
 lemma basis_contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C}
@@ -203,7 +203,8 @@ lemma basis_contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complex
     (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) := fun k => (pauliMatrixBasisProdMap b i1 i2 i3) (i.succAbove (j.succAbove k))
+    let b' (i1 i2 i3 : Fin 4) := fun k => (pauliMatrixBasisProdMap 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 = (((
@@ -215,13 +216,16 @@ lemma basis_contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complex
       (tensorNode (basisVector c' (b' 1 0 1))))).add
     (((TensorTree.smul (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 1 1 0))
       (tensorNode (basisVector c' (b' 1 1 0))))).add
-    ((TensorTree.smul (-I) ((TensorTree.smul (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 2 0 1))
+    ((TensorTree.smul (-I) ((TensorTree.smul
+      (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 2 0 1))
       (tensorNode (basisVector c' (b' 2 0 1)))))).add
-    ((TensorTree.smul I ((TensorTree.smul (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 2 1 0))
+    ((TensorTree.smul I ((TensorTree.smul
+      (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 2 1 0))
       (tensorNode (basisVector c' (b' 2 1 0)))))).add
     (((TensorTree.smul (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 3 0 0))
       (tensorNode (basisVector c' (b' 3 0 0))))).add
-    (TensorTree.smul (-1) ((TensorTree.smul (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 3 1 1)) (tensorNode
+    (TensorTree.smul (-1) ((TensorTree.smul
+      (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 3 1 1)) (tensorNode
       (basisVector c' (b' 3 1 1))))))))))))).tensor := by
   rw [basis_contr_pauliMatrix_basis_tree_expand']
   /- Contracting basis vectors. -/
@@ -243,35 +247,30 @@ lemma basis_contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complex
     smul_tensor_eq <| contr_basisVector_tree _]
   rfl
 
-def pauilMatrixBasisContrMap {n : ℕ} {c : Fin n → complexLorentzTensor.C}
-    (i : Fin (n + 3)) (j : Fin (n +2))
-    (b : Π k, Fin (complexLorentzTensor.repDim (c k))) (i1 i2 i3 : Fin 4)  :
-     (k : Fin (n + 1)) →
-        Fin
-          (complexLorentzTensor.repDim
-            (Sum.elim c ![Color.up, Color.upL, Color.upR] (finSumFinEquiv.symm (i.succAbove (j.succAbove k))))) :=
-    fun k => (pauliMatrixBasisProdMap b i1 i2 i3) (i.succAbove (j.succAbove k))
-
-
 lemma basis_contr_pauliMatrix_basis_tree_expand_tensor {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) := fun k => (pauliMatrixBasisProdMap 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 =
-    (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 0 0 0)) • (basisVectorContrPauli i j b 0 0 0)
-    + (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 0 1 1)) • (basisVectorContrPauli i j b 0 1 1)
-    + (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 1 0 1)) • (basisVectorContrPauli i j b 1 0 1)
-    + (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 1 1 0)) • (basisVectorContrPauli i j b 1 1 0)
-    + (-I) • (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 2 0 1)) • (basisVectorContrPauli i j b 2 0 1)
-    + I • (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 2 1 0)) • (basisVectorContrPauli i j b 2 1 0)
-    + (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 3 0 0)) • (basisVectorContrPauli i j b 3 0 0)
-    + (-1 : ℂ) • (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 3 1 1)) • (basisVectorContrPauli i j b 3 1 1) := by
+    (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 0 0 0)) •
+      (basisVectorContrPauli i j b 0 0 0)
+    + (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 0 1 1)) •
+      (basisVectorContrPauli i j b 0 1 1)
+    + (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 1 0 1)) •
+      (basisVectorContrPauli i j b 1 0 1)
+    + (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 1 1 0)) •
+      (basisVectorContrPauli i j b 1 1 0)
+    + (-I) • (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 2 0 1)) •
+      (basisVectorContrPauli i j b 2 0 1)
+    + I • (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 2 1 0)) •
+      (basisVectorContrPauli i j b 2 1 0)
+    + (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 3 0 0)) •
+      (basisVectorContrPauli i j b 3 0 0)
+    + (-1 : ℂ) • (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 3 1 1)) •
+      (basisVectorContrPauli i j b 3 1 1) := by
   rw [basis_contr_pauliMatrix_basis_tree_expand]
   simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, cons_val_one, head_cons, Fin.val_zero,
     Nat.cast_zero, cons_val_two, Fin.val_one, Nat.cast_one, add_tensor, smul_tensor,
@@ -279,8 +278,6 @@ lemma basis_contr_pauliMatrix_basis_tree_expand_tensor {n : ℕ} {c : Fin n →
   simp_all only [Function.comp_apply, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue]
   rfl
 
-
-
 end complexLorentzTensor
 
 end
diff --git a/HepLean/Tensors/ComplexLorentz/PauliLower.lean b/HepLean/Tensors/ComplexLorentz/PauliLower.lean
index a283de0..191b0e4 100644
--- a/HepLean/Tensors/ComplexLorentz/PauliLower.lean
+++ b/HepLean/Tensors/ComplexLorentz/PauliLower.lean
@@ -76,7 +76,7 @@ lemma pauliMatrix_contr_down_0 :
     fin_cases k <;> rfl
 
 lemma pauliMatrix_contr_down_1 :
-    {(basisVector ![Color.down, Color.down] fun x => 1) | ν μ  ⊗
+    {(basisVector ![Color.down, Color.down] fun x => 1) | ν μ ⊗
       PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
     = basisVector pauliCoMap (fun | 0 => 1 | 1 => 0 | 2 => 1)
     + basisVector pauliCoMap (fun | 0 => 1 | 1 => 1 | 2 => 0) := by
@@ -268,7 +268,6 @@ lemma pauliCo_basis_expand : pauliCo
   simp only [neg_smul, one_smul]
   abel
 
-
 lemma pauliCo_basis_expand_tree : pauliCo
     = (TensorTree.add (tensorNode
       (basisVector pauliCoMap (fun | 0 => 0 | 1 => 0 | 2 => 0))) <|
diff --git a/HepLean/Tensors/Tree/Basic.lean b/HepLean/Tensors/Tree/Basic.lean
index 013c1be..cee6bfe 100644
--- a/HepLean/Tensors/Tree/Basic.lean
+++ b/HepLean/Tensors/Tree/Basic.lean
@@ -791,11 +791,11 @@ def zeroTree {n : ℕ} {c : Fin n → S.C} : TensorTree S c := tensorNode 0
 lemma zeroTree_tensor {n : ℕ} {c : Fin n → S.C} : (zeroTree (c := c)).tensor = 0 := by
   rfl
 
-lemma zero_smul {T1  : TensorTree S c} :
+lemma zero_smul {T1 : TensorTree S c} :
     (smul 0 T1).tensor = zeroTree.tensor := by
   simp only [smul_tensor, _root_.zero_smul, zeroTree_tensor]
 
-lemma smul_zero {a : S.k} : (smul a (zeroTree (c :=c ))).tensor = zeroTree.tensor := by
+lemma smul_zero {a : S.k} : (smul a (zeroTree (c := c))).tensor = zeroTree.tensor := by
   simp only [smul_tensor, zeroTree_tensor, _root_.smul_zero]
 
 lemma zero_add {T1 : TensorTree S c} : (add zeroTree T1).tensor = T1.tensor := by
@@ -808,11 +808,11 @@ lemma perm_zero {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (σ : (Over
     (OverColor.mk c1)) : (perm σ zeroTree).tensor = zeroTree.tensor := by
   simp only [perm_tensor, zeroTree_tensor, map_zero]
 
-lemma neg_zero  : (neg (zeroTree (c := c))).tensor = zeroTree.tensor := by
+lemma neg_zero : (neg (zeroTree (c := c))).tensor = zeroTree.tensor := by
   simp only [neg_tensor, zeroTree_tensor, _root_.neg_zero]
 
-lemma contr_zero  {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ}
-    {h : c (i.succAbove j) = S.τ (c i)}  : (contr i j h zeroTree).tensor = zeroTree.tensor := by
+lemma contr_zero {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ}
+    {h : c (i.succAbove j) = S.τ (c i)} : (contr i j h zeroTree).tensor = zeroTree.tensor := by
   simp only [contr_tensor, zeroTree_tensor, map_zero]
 
 lemma zero_prod {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (t : TensorTree S c1) :