From f7499f8d867d1caf2b8fb8778a23e2d01542217a Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 29 Oct 2024 11:32:04 +0000
Subject: [PATCH] refactor: Linting

---
 HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean     | 2 +-
 HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean | 2 +-
 HepLean/Tensors/OverColor/Iso.lean                      | 2 +-
 HepLean/Tensors/Tree/NodeIdentities/Basic.lean          | 2 +-
 HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean     | 3 +++
 5 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
index 395cda4..e731941 100644
--- a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
@@ -149,7 +149,7 @@ lemma contrBispinorDown_eq_pauliCoDown_contr (p : complexContr) :
 
 set_option maxRecDepth 5000 in
 lemma coBispinorDown_eq_pauliContrDown_contr (p : complexCo) :
-    {coBispinorDown p | α β = pauliContrDown | μ α β ⊗ p | μ}ᵀs := by
+    {coBispinorDown p | α β = pauliContrDown | μ α β ⊗ p | μ}ᵀ := by
   conv =>
     rhs
     rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_fst <|
diff --git a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean
index bc48973..021150b 100644
--- a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean
@@ -37,7 +37,7 @@ open Fermion
 
 -/
 
-/- The Pauli matrices as the complex Lorentz tensor `σ^μ^α^{dot β}`. -/
+/-- The Pauli matrices as the complex Lorentz tensor `σ^μ^α^{dot β}`. -/
 def pauliContr := {PauliMatrix.asConsTensor | ν α β}ᵀ.tensor
 
 /-- The Pauli matrices as the complex Lorentz tensor `σ_μ^α^{dot β}`. -/
diff --git a/HepLean/Tensors/OverColor/Iso.lean b/HepLean/Tensors/OverColor/Iso.lean
index fcb83cd..13520b5 100644
--- a/HepLean/Tensors/OverColor/Iso.lean
+++ b/HepLean/Tensors/OverColor/Iso.lean
@@ -62,7 +62,7 @@ def mkIso {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2 :=
     rfl))
 
 lemma mkIso_refl_hom {c : X → C} : (mkIso (by rfl : c =c)).hom = 𝟙 _ := by
-  simp [mkIso]
+  rw [mkIso]
   rfl
 
 @[simp]
diff --git a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
index ea19d5f..ed1f0f6 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
@@ -121,7 +121,7 @@ lemma perm_eq_iff_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
     (perm σ t).tensor = t2.tensor ↔ t.tensor =
     (perm (equivToHomEq (Hom.toEquiv σ).symm (fun x => Hom.toEquiv_comp_apply σ x)) t2).tensor := by
   refine Iff.intro (fun h => ?_) (fun h => ?_)
-  · simp [perm_tensor, ← h]
+  · simp only [mk_hom, perm_tensor, ← h]
     change _ = (S.F.map _ ≫ S.F.map _).hom _
     rw [← S.F.map_comp]
     have h1 : (σ ≫ equivToHomEq (Hom.toEquiv σ).symm
diff --git a/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean b/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean
index acd10cf..1ade571 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean
@@ -281,6 +281,9 @@ lemma contr_contr (t : TensorTree S c) :
 end
 end ContrQuartet
 
+/-- The homomorphism one must apply on swapping the order of contractions.
+  This is identical to `ContrQuartet.contrSwapHom` except manifestly between the correct
+  types. -/
 def contrContrPerm {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n.succ.succ.succ.succ}
     {j : Fin n.succ.succ.succ} {k : Fin n.succ.succ} {l : Fin n.succ}
     (hij : c (i.succAbove j) = S.τ (c i)) (hkl : (c ∘ i.succAbove ∘ j.succAbove) (k.succAbove l) =