From 9d4c21fd6da9cfedd0b0b7eb02a77c3e3f9a5229 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 10 Dec 2024 14:02:31 +0000
Subject: [PATCH] refactor: Lint

---
 HepLean/Tensors/OverColor/Functors.lean       | 50 +++++++++++--------
 HepLean/Tensors/OverColor/Lift.lean           | 27 +++++++---
 HepLean/Tensors/TensorSpecies/Basic.lean      | 10 ++--
 .../TensorSpecies/Contractions/ContrMap.lean  |  7 +--
 .../Tensors/Tree/NodeIdentities/Basic.lean    |  7 +--
 .../Tree/NodeIdentities/PermContr.lean        |  9 ++--
 .../Tensors/Tree/NodeIdentities/PermProd.lean |  6 ++-
 .../Tree/NodeIdentities/ProdAssoc.lean        | 17 ++++---
 .../Tensors/Tree/NodeIdentities/ProdComm.lean |  3 +-
 .../Tree/NodeIdentities/ProdContr.lean        | 12 +++--
 scripts/lint_all.lean                         |  6 +--
 11 files changed, 98 insertions(+), 56 deletions(-)

diff --git a/HepLean/Tensors/OverColor/Functors.lean b/HepLean/Tensors/OverColor/Functors.lean
index 8de5d4f..bd96061 100644
--- a/HepLean/Tensors/OverColor/Functors.lean
+++ b/HepLean/Tensors/OverColor/Functors.lean
@@ -19,20 +19,21 @@ open MonoidalCategory
 def map {C D : Type} (f : C → D) : Functor (OverColor C) (OverColor D) :=
   Core.functorToCore (Core.inclusion (Over C) ⋙ (Over.map f))
 
+/-- The functor `map f` is lax-monoidal. -/
 instance map_laxMonoidal {C D : Type} (f : C → D) : Functor.LaxMonoidal (map f) where
   ε' := Over.isoMk (Iso.refl _) (by
     ext x
     exact Empty.elim x)
-  μ'  := fun X Y => Over.isoMk (Iso.refl _) (by
+  μ' := fun X Y => Over.isoMk (Iso.refl _) (by
     ext x
     match x with
     | Sum.inl x => rfl
     | Sum.inr x => rfl)
-  μ'_natural_left :=  fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+  μ'_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
     rfl
-  μ'_natural_right := fun X Y =>  CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+  μ'_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
     rfl
-  associativity' := fun X Y Z =>  CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+  associativity' X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
     match x with
     | Sum.inl (Sum.inl x) => rfl
     | Sum.inl (Sum.inr x) => rfl
@@ -46,6 +47,7 @@ instance map_laxMonoidal {C D : Type} (f : C → D) : Functor.LaxMonoidal (map f
     | Sum.inl x => rfl
     | Sum.inr x => rfl
 
+/-- The functor `map f` is lax-monoidal. -/
 noncomputable instance map_monoidal {C D : Type} (f : C → D) : Functor.Monoidal (map f) :=
   Functor.Monoidal.ofLaxMonoidal _
 
@@ -53,6 +55,7 @@ noncomputable instance map_monoidal {C D : Type} (f : C → D) : Functor.Monoida
 def tensor (C : Type) : Functor (OverColor C × OverColor C) (OverColor C) :=
   MonoidalCategory.tensor (OverColor C)
 
+/-- The functor tensor is lax-monoidal. -/
 instance tensor_laxMonoidal (C : Type) : Functor.LaxMonoidal (tensor C) where
   ε' := Over.isoMk (Equiv.sumEmpty Empty Empty).symm.toIso rfl
   μ' := fun X Y => Over.isoMk (Equiv.sumSumSumComm X.1.left X.2.left Y.1.left Y.2.left).toIso (by
@@ -62,19 +65,19 @@ instance tensor_laxMonoidal (C : Type) : Functor.LaxMonoidal (tensor C) where
     | Sum.inl (Sum.inr x) => rfl
     | Sum.inr (Sum.inl x) => rfl
     | Sum.inr (Sum.inr x) => rfl)
-  μ'_natural_left := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+  μ'_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
     match x with
     | Sum.inl (Sum.inl x) => rfl
     | Sum.inl (Sum.inr x) => rfl
     | Sum.inr (Sum.inl x) => rfl
     | Sum.inr (Sum.inr x) => rfl
-  μ'_natural_right := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+  μ'_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
     match x with
     | Sum.inl (Sum.inl x) => rfl
     | Sum.inl (Sum.inr x) => rfl
     | Sum.inr (Sum.inl x) => rfl
     | Sum.inr (Sum.inr x) => rfl
-  associativity' := fun X Y Z => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+  associativity' X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
     match x with
     | Sum.inl (Sum.inl (Sum.inl x)) => rfl
     | Sum.inl (Sum.inl (Sum.inr x)) => rfl
@@ -82,60 +85,67 @@ instance tensor_laxMonoidal (C : Type) : Functor.LaxMonoidal (tensor C) where
     | Sum.inl (Sum.inr (Sum.inr x)) => rfl
     | Sum.inr (Sum.inl x) => rfl
     | Sum.inr (Sum.inr x) => rfl
-  left_unitality' :=  fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+  left_unitality' X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
     match x with
     | Sum.inl x => exact Empty.elim x
     | Sum.inr (Sum.inl x)=> rfl
     | Sum.inr (Sum.inr x)=> rfl
-  right_unitality'  := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
+  right_unitality' X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
     match x with
     | Sum.inl (Sum.inl x) => rfl
     | Sum.inl (Sum.inr x) => rfl
     | Sum.inr x => exact Empty.elim x
 
+/-- The functor tensor is monoidal. -/
 noncomputable instance tensor_monoidal (C : Type) : Functor.Monoidal (tensor C) :=
   Functor.Monoidal.ofLaxMonoidal _
 
 /-- The constant monoidal functor from `OverColor C` to itself landing on `𝟙_ (OverColor C)`. -/
 def const (C : Type) : Functor (OverColor C) (OverColor C) :=
-   (Functor.const (OverColor C)).obj (𝟙_ (OverColor C))
+  (Functor.const (OverColor C)).obj (𝟙_ (OverColor C))
 
+/-- The functor `const C` is lax monoidal. -/
 instance const_laxMonoidal (C : Type) : Functor.LaxMonoidal (const C) where
   ε' := 𝟙 (𝟙_ (OverColor C))
   μ' := fun _ _ => (λ_ (𝟙_ (OverColor C))).hom
-  μ'_natural_left :=  fun _ _ => by
+  μ'_natural_left := fun _ _ => by
     simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerRight_id,
       Category.id_comp, Iso.hom_inv_id, Category.comp_id, const]
   μ'_natural_right := fun _ _ => by
     simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerLeft_id,
       Category.id_comp, Category.comp_id, const]
-  associativity' := fun X Y Z  => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
+  associativity' X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i =>
     match i with
     | Sum.inl (Sum.inl i) => rfl
     | Sum.inl (Sum.inr i) => rfl
     | Sum.inr i => rfl
-  left_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
+  left_unitality' X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i =>
     match i with
-    | Sum.inl i => exact Empty.elim i
-    | Sum.inr i => exact Empty.elim i
-  right_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
+    | Sum.inl i => Empty.elim i
+    | Sum.inr i => Empty.elim i
+  right_unitality' X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i =>
     match i with
-    | Sum.inl i => exact Empty.elim i
-    | Sum.inr i => exact Empty.elim i
+    | Sum.inl i => Empty.elim i
+    | Sum.inr i => Empty.elim i
 
+/-- The functor `const C` is monoidal. -/
 noncomputable instance const_monoidal (C : Type) : Functor.Monoidal (const C) :=
   Functor.Monoidal.ofLaxMonoidal _
 
 /-- The monoidal functor from `OverColor C` to `OverColor C` taking `f` to `f ⊗ τ_* f`. -/
 def contrPair (C : Type) (τ : C → C) : Functor (OverColor C) (OverColor C) :=
- (Functor.diag (OverColor C))
+  (Functor.diag (OverColor C))
   ⋙ (Functor.prod (Functor.id (OverColor C)) (OverColor.map τ))
   ⋙ (OverColor.tensor C)
 
+/-- The functor `contrPair` is lax-monoidal. -/
 instance contrPair_laxMonoidal (C : Type) (τ : C → C) : Functor.LaxMonoidal (contrPair C τ) :=
   Functor.LaxMonoidal.comp (Functor.diag (OverColor C)) ((𝟭 (OverColor C)).prod (map τ) ⋙ tensor C)
 
-noncomputable instance contrPair_monoidal (C : Type) (τ : C → C) : Functor.Monoidal (contrPair C τ) :=
+/-- The functor `contrPair` is monoidal. -/
+noncomputable instance contrPair_monoidal (C : Type) (τ : C → C) :
+    Functor.Monoidal (contrPair C τ) :=
   Functor.Monoidal.ofLaxMonoidal _
+
 end OverColor
 end IndexNotation
diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean
index 599d8d0..7a314ff 100644
--- a/HepLean/Tensors/OverColor/Lift.lean
+++ b/HepLean/Tensors/OverColor/Lift.lean
@@ -551,13 +551,14 @@ lemma objMap'_comp {X Y Z : OverColor C} (f : X ⟶ Y) (g : Y ⟶ Z) :
   rw [discreteFun_hom_trans]
   rfl
 
-/-- The `BraidedFunctor (OverColor C) (Rep k G)` from a functor `Discrete C ⥤ Rep k G`. -/
+/-- The `Functor (OverColor C) (Rep k G)` from a functor `Discrete C ⥤ Rep k G`. -/
 def obj' : Functor (OverColor C) (Rep k G) where
   obj := objObj' F
   map := objMap' F
-  map_comp := fun  f g => objMap'_comp F f g
+  map_comp := fun f g => objMap'_comp F f g
   map_id := fun f => objMap'_id F f
 
+/-- The lift of a functor is lax braided. -/
 instance obj'_laxBraidedFunctor : Functor.LaxBraided (obj' F) where
   ε' := (ε F).hom
   μ' := fun X Y => (μ F X Y).hom
@@ -571,12 +572,17 @@ instance obj'_laxBraidedFunctor : Functor.LaxBraided (obj' F) where
     rw [braided F X Y]
     simp
 
+/-- The lift of a functor is monoidal. -/
 instance obj'_monoidalFunctor : Functor.Monoidal (obj' F) :=
   haveI : IsIso (Functor.LaxMonoidal.ε (obj' F)) := Action.isIso_of_hom_isIso (ε F).hom
   haveI : (∀ (X Y : OverColor C), IsIso (Functor.LaxMonoidal.μ (obj' F) X Y)) :=
     fun X Y => Action.isIso_of_hom_isIso ((μ F X Y).hom)
   Functor.Monoidal.ofLaxMonoidal _
 
+/-- The lift of a functor is braided. -/
+instance obj'_braided : Functor.Braided (obj' F) := Functor.Braided.mk (fun X Y =>
+  Functor.LaxBraided.braided X Y)
+
 variable {F F' : Discrete C ⥤ Rep k G} (η : F ⟶ F')
 
 /-- The maps for a natural transformation between `obj' F` and `obj' F'`. -/
@@ -680,10 +686,11 @@ lemma mapApp'_tensor (X Y : OverColor C) :
 
 /-- Given a natural transformation between `F F' : Discrete C ⥤ Rep k G` the
   monoidal natural transformation between `obj' F` and `obj' F'`. -/
-def map' :  (obj' F) ⟶  (obj' F') where
+def map' : (obj' F) ⟶ (obj' F') where
   app := mapApp' η
   naturality _ _ f := mapApp'_naturality η f
 
+/-- The lift of a natural transformation is monoidal. -/
 instance map'_isMonoidal : NatTrans.IsMonoidal (map' η) where
   unit := mapApp'_unit η
   tensor := mapApp'_tensor η
@@ -736,10 +743,13 @@ noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ LaxBraidedFunctor (OverCol
 namespace lift
 variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F')
 
+/-- The lift of a functor is monoidal. -/
 noncomputable instance : (lift.obj F).Monoidal := obj'_monoidalFunctor F
 
+/-- The lift of a functor is lax-braided. -/
 noncomputable instance : (lift.obj F).LaxBraided := obj'_laxBraidedFunctor F
 
+/-- The lift of a functor is braided. -/
 noncomputable instance : (lift.obj F).Braided := Functor.Braided.mk (fun X Y =>
   Functor.LaxBraided.braided X Y)
 
@@ -754,7 +764,8 @@ lemma map_tprod (F : Discrete C ⥤ Rep k G) {X Y : OverColor C} (f : X ⟶ Y)
 lemma obj_μ_tprod_tmul (F : Discrete C ⥤ Rep k G) (X Y : OverColor C)
     (p : (i : X.left) → (F.obj (Discrete.mk <| X.hom i)))
     (q : (i : Y.left) → F.obj (Discrete.mk <| Y.hom i)) :
-    (Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).hom (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q) =
+    (Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).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
   exact μ_tmul_tprod F p q
@@ -764,12 +775,14 @@ lemma μIso_inv_tprod (F : Discrete C ⥤ Rep k G) (X Y : OverColor C)
     (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y).inv.hom (PiTensorProduct.tprod k p) =
     (PiTensorProduct.tprod k (fun i => p (Sum.inl i))) ⊗ₜ[k]
     (PiTensorProduct.tprod k (fun i => p (Sum.inr i))) := by
-  change ((Action.forget _ _).mapIso (Functor.Monoidal.μIso (lift.obj F).toFunctor  X Y)).inv (PiTensorProduct.tprod k p) = _
-  trans ((Action.forget _ _).mapIso (Functor.Monoidal.μIso (lift.obj F).toFunctor  X Y)).toLinearEquiv.symm
+  change ((Action.forget _ _).mapIso (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y)).inv
+    (PiTensorProduct.tprod k p) = _
+  trans ((Action.forget _ _).mapIso
+    (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y)).toLinearEquiv.symm
     (PiTensorProduct.tprod k p)
   · rfl
   erw [← LinearEquiv.eq_symm_apply]
-  change _ = (Functor.LaxMonoidal.μ (lift.obj F).toFunctor  X Y).hom _
+  change _ = (Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).hom _
   erw [obj_μ_tprod_tmul]
   congr
   funext i
diff --git a/HepLean/Tensors/TensorSpecies/Basic.lean b/HepLean/Tensors/TensorSpecies/Basic.lean
index db1c058..29dd8b5 100644
--- a/HepLean/Tensors/TensorSpecies/Basic.lean
+++ b/HepLean/Tensors/TensorSpecies/Basic.lean
@@ -111,14 +111,18 @@ def F : Functor (OverColor S.C) (Rep S.k S.G) := ((OverColor.lift).obj S.FD).toF
 /- The definition of `F` as a lemma. -/
 lemma F_def : F S = ((OverColor.lift).obj S.FD).toFunctor := rfl
 
-instance F_monoidal : Functor.Monoidal S.F := lift.instMonoidalRepObjFunctorDiscreteLaxBraidedFunctor S.FD
+/-- The functor `F` is monoidal. -/
+instance F_monoidal : Functor.Monoidal S.F :=
+  lift.instMonoidalRepObjFunctorDiscreteLaxBraidedFunctor S.FD
 
-instance F_laxBraided : Functor.LaxBraided S.F := lift.instLaxBraidedRepObjFunctorDiscreteLaxBraidedFunctor S.FD
+/-- The functor `F` is lax-braided. -/
+instance F_laxBraided : Functor.LaxBraided S.F :=
+  lift.instLaxBraidedRepObjFunctorDiscreteLaxBraidedFunctor S.FD
 
+/-- The functor `F` is braided. -/
 instance F_braided : Functor.Braided S.F := Functor.Braided.mk
   (fun X Y => Functor.LaxBraided.braided X Y)
 
-
 lemma perm_contr_cond {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.succ → S.C}
     {i : Fin n.succ.succ} {j : Fin n.succ}
     (h : c1 (i.succAbove j) = S.τ (c1 i)) (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
diff --git a/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean b/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean
index 3b8065d..b1dc6c3 100644
--- a/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean
+++ b/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean
@@ -152,7 +152,8 @@ lemma contrIso_hom_hom {n : ℕ} {c1 : Fin n.succ.succ → S.C}
     (S.contrIso c1 i j h).hom.hom =
     (S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom ≫
     (S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom ≫
-    (Functor.Monoidal.μIso S.F (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
+    (Functor.Monoidal.μIso S.F
+    (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
     (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom ≫
     ((S.contrFin1Fin1 c1 i j h).hom.hom ⊗
     (S.F.map (mkIso (contrIso.proof_1 S c1 i j)).hom).hom) := by
@@ -192,8 +193,8 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
     (((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj
     (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
     (((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom)
-    ((Functor.Monoidal.μIso (lift.obj S.FD).toFunctor (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)
-    ∘ Sum.inl))
+    ((Functor.Monoidal.μIso (lift.obj S.FD).toFunctor
+    (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
     (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
     (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom
     (((lift.obj S.FD).map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom
diff --git a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
index 88358a7..6511800 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
@@ -312,14 +312,15 @@ lemma prod_action {n n1 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} (g : S.
   simp only [prod_tensor, action_tensor, map_tmul]
   change _ = ((S.F.map (equivToIso finSumFinEquiv).hom).hom ≫
     (S.F.obj (OverColor.mk (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm))).ρ g)
-    (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom (t.tensor ⊗ₜ[S.k] t1.tensor)))
+    (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom
+    (t.tensor ⊗ₜ[S.k] t1.tensor)))
   erw [← (S.F.map (equivToIso finSumFinEquiv).hom).comm g]
   simp only [Action.forget_obj, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
     Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
     Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply]
   change _ = (S.F.map (equivToIso finSumFinEquiv).hom).hom
-    (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom ≫ (S.F.obj (OverColor.mk (Sum.elim c c1))).ρ g)
-      (t.tensor ⊗ₜ[S.k] t1.tensor))
+    (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom ≫
+    (S.F.obj (OverColor.mk (Sum.elim c c1))).ρ g) (t.tensor ⊗ₜ[S.k] t1.tensor))
   erw [← (Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).comm g]
   rfl
 
diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
index 64e045a..efb0911 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
@@ -117,14 +117,17 @@ lemma contrIso_comm_aux_2 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
     {i : Fin n.succ.succ} {j : Fin n.succ}
     (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
     (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)).hom ≫
-    (Functor.Monoidal.μIso S.F (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
+    (Functor.Monoidal.μIso S.F
+    (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
     (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom =
     (Functor.Monoidal.μIso S.F _ _).inv.hom ≫
     (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)).hom := by
   have h1 : (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)) ≫
-    (Functor.Monoidal.μIso S.F (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
+    (Functor.Monoidal.μIso S.F
+    (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
     (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv =
-    (Functor.Monoidal.μIso S.F _ _).inv ≫ (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)) := by
+    (Functor.Monoidal.μIso S.F _ _).inv ≫
+    (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)) := by
     erw [CategoryTheory.IsIso.comp_inv_eq, CategoryTheory.Category.assoc]
     erw [CategoryTheory.IsIso.eq_inv_comp]
     exact (Functor.LaxMonoidal.μ_natural S.F (extractTwoAux' i j σ) (extractTwoAux i j σ)).symm
diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean b/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean
index bf355d2..1df572e 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean
@@ -54,7 +54,8 @@ theorem prod_perm_left (t : TensorTree S c) (t2 : TensorTree S c2) :
     Action.FunctorCategoryEquivalence.functor_obj_obj, perm_tensor]
   change (S.F.map (equivToIso finSumFinEquiv).hom).hom
     (((S.F.map (σ) ▷ S.F.obj (OverColor.mk c2)) ≫
-    Functor.LaxMonoidal.μ S.F (OverColor.mk c') (OverColor.mk c2)).hom (t.tensor ⊗ₜ[S.k] t2.tensor)) = _
+    Functor.LaxMonoidal.μ S.F (OverColor.mk c') (OverColor.mk c2)).hom
+    (t.tensor ⊗ₜ[S.k] t2.tensor)) = _
   rw [Functor.LaxMonoidal.μ_natural_left]
   simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom,
     Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
@@ -72,7 +73,8 @@ theorem prod_perm_right (t2 : TensorTree S c2) (t : TensorTree S c) :
     Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
     Action.FunctorCategoryEquivalence.functor_obj_obj, perm_tensor]
   change (S.F.map (equivToIso finSumFinEquiv).hom).hom
-    (((S.F.obj (OverColor.mk c2) ◁ S.F.map σ) ≫ Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c')).hom
+    (((S.F.obj (OverColor.mk c2) ◁ S.F.map σ) ≫
+    Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c')).hom
     (t2.tensor ⊗ₜ[S.k] t.tensor)) = _
   rw [Functor.LaxMonoidal.μ_natural_right]
   simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom,
diff --git a/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean b/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean
index 80e3a5e..1ee3281 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean
@@ -63,8 +63,8 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree
   rw [perm_tensor]
   nth_rewrite 2 [prod_tensor]
   change _ = ((S.F.map (equivToIso finSumFinEquiv).hom) ≫ S.F.map (assocPerm c c2 c3).hom).hom
-    (((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) (OverColor.mk c3)).hom
-        ((t.prod t2).tensor ⊗ₜ[S.k] t3.tensor)))
+    (((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm))
+    (OverColor.mk c3)).hom ((t.prod t2).tensor ⊗ₜ[S.k] t3.tensor)))
   rw [← S.F.map_comp, finSumFinEquiv_comp_assocPerm]
   simp only [Functor.id_obj, mk_hom, whiskerRightIso_hom, Iso.symm_hom, whiskerLeftIso_hom,
     Functor.map_comp, Action.comp_hom, Action.instMonoidalCategory_tensorObj_V,
@@ -74,7 +74,8 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree
   apply congrArg
   change _ = (S.F.map (OverColor.mk c ◁ (equivToIso finSumFinEquiv).hom)).hom
     ((S.F.map (α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).hom).hom
-    ((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) (OverColor.mk c3)
+    ((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm))
+    (OverColor.mk c3)
     ≫ S.F.map ((equivToIso finSumFinEquiv).inv ▷ OverColor.mk c3)).hom
     (((t.prod t2).tensor ⊗ₜ[S.k] t3.tensor))))
   rw [← Functor.LaxMonoidal.μ_natural_left]
@@ -91,8 +92,8 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree
     ((S.F.map (α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).hom).hom
     ((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2)) (OverColor.mk c3)).hom
     ((S.F.map (equivToIso finSumFinEquiv).hom ≫ S.F.map (equivToIso finSumFinEquiv).inv).hom
-    (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c2)).hom (t.tensor ⊗ₜ[S.k] t2.tensor))) ⊗ₜ[S.k]
-    t3.tensor)))
+    (((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c2)).hom
+    (t.tensor ⊗ₜ[S.k] t2.tensor))) ⊗ₜ[S.k] t3.tensor)))
   simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
     Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
     Action.FunctorCategoryEquivalence.functor_obj_obj, Iso.map_hom_inv_id, Action.id_hom,
@@ -110,9 +111,11 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree
     ModuleCat.MonoidalCategory.associator_hom_apply]
   rw [prod_tensor]
   change ((_ ◁ (S.F.map (equivToIso finSumFinEquiv).hom)) ≫
-    Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm))).hom
+    Functor.LaxMonoidal.μ S.F (OverColor.mk c)
+    (OverColor.mk (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm))).hom
     (t.tensor ⊗ₜ[S.k]
-    ((Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c3)).hom (t2.tensor ⊗ₜ[S.k] t3.tensor))) = _
+    ((Functor.LaxMonoidal.μ S.F
+    (OverColor.mk c2) (OverColor.mk c3)).hom (t2.tensor ⊗ₜ[S.k] t3.tensor))) = _
   rw [Functor.LaxMonoidal.μ_natural_right]
   simp only [Action.instMonoidalCategory_tensorObj_V, Action.comp_hom, Equivalence.symm_inverse,
     Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
diff --git a/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean b/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean
index ec68726..7526f17 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean
@@ -49,7 +49,8 @@ theorem prod_comm (t : TensorTree S c) (t2 : TensorTree S c2) :
   rw [perm_tensor]
   nth_rewrite 2 [prod_tensor]
   change _ = (S.F.map (equivToIso finSumFinEquiv).hom ≫ S.F.map (braidPerm c c2)).hom
-    ((Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c)).hom (t2.tensor ⊗ₜ[S.k] t.tensor))
+    ((Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c)).hom
+    (t2.tensor ⊗ₜ[S.k] t.tensor))
   rw [← S.F.map_comp]
   rw [finSumFinEquiv_comp_braidPerm]
   rw [S.F.map_comp]
diff --git a/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean b/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean
index 0e416d2..df7f736 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean
@@ -172,7 +172,8 @@ lemma contrMap_prod_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c).left) →
     (q' : (i : (𝟭 Type).obj (OverColor.mk c1).left) →
       CoeSort.coe (S.FD.obj { as := (OverColor.mk c1).hom i })) :
     (S.F.map (equivToIso finSumFinEquiv).hom).hom
-    ((Functor.LaxMonoidal.μ S.F (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)) (OverColor.mk c1)).hom
+    ((Functor.LaxMonoidal.μ S.F
+    (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)) (OverColor.mk c1)).hom
     ((q.contrMap.hom (PiTensorProduct.tprod S.k p)) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) q'))
     = (S.F.map (mkIso (by exact leftContr_map_eq q)).hom).hom
     (q.leftContr.contrMap.hom
@@ -288,7 +289,8 @@ lemma contr_prod
     q.leftContr.h
     (perm (OverColor.equivToIso ContrPair.leftContrEquivSuccSucc).hom (prod t t1)))).tensor) := by
   simp only [contr_tensor, perm_tensor, prod_tensor]
-  change ((q.contrMap ▷ S.F.obj (OverColor.mk c1)) ≫ (Functor.LaxMonoidal.μ S.F _ ((OverColor.mk c1))) ≫
+  change ((q.contrMap ▷ S.F.obj (OverColor.mk c1)) ≫
+    (Functor.LaxMonoidal.μ S.F _ ((OverColor.mk c1))) ≫
     S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom (t.tensor ⊗ₜ[S.k] t1.tensor) = _
   rw [contrMap_prod]
   simp only [Nat.succ_eq_add_one, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
@@ -405,7 +407,8 @@ lemma prod_contrMap_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c1).left) →
     (q' : (i : (𝟭 Type).obj (OverColor.mk c).left) →
       CoeSort.coe (S.FD.obj { as := (OverColor.mk c).hom i })) :
     (S.F.map (equivToIso finSumFinEquiv).hom).hom
-    ((Functor.LaxMonoidal.μ S.F (OverColor.mk c1) (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove))).hom
+    ((Functor.LaxMonoidal.μ S.F (OverColor.mk c1)
+    (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove))).hom
     ((PiTensorProduct.tprod S.k) p ⊗ₜ[S.k] (q.contrMap.hom (PiTensorProduct.tprod S.k q')))) =
     (S.F.map (mkIso (by exact (rightContr_map_eq q))).hom).hom
     (q.rightContr.contrMap.hom
@@ -530,7 +533,8 @@ lemma prod_contr (t1 : TensorTree S c1) (t : TensorTree S c) :
     (contr (q.rightContrI n1) (q.rightContrJ n1)
     q.rightContr.h (prod t1 t))).tensor) := by
   simp only [contr_tensor, perm_tensor, prod_tensor]
-  change ((S.F.obj (OverColor.mk c1) ◁ q.contrMap) ≫ (Functor.LaxMonoidal.μ S.F ((OverColor.mk c1)) _) ≫
+  change ((S.F.obj (OverColor.mk c1) ◁ q.contrMap) ≫
+    (Functor.LaxMonoidal.μ S.F ((OverColor.mk c1)) _) ≫
     S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom (t1.tensor ⊗ₜ[S.k] t.tensor) = _
   rw [prod_contrMap]
   simp only [Nat.succ_eq_add_one, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
diff --git a/scripts/lint_all.lean b/scripts/lint_all.lean
index 34e22ef..bd02b41 100644
--- a/scripts/lint_all.lean
+++ b/scripts/lint_all.lean
@@ -11,15 +11,15 @@ import HepLean.Meta.Informal.Post
 import ImportGraph.RequiredModules
 
 def main (_: List String) : IO UInt32 := do
+  println! "Style lint ... "
+  let styleLint ← IO.Process.output {cmd := "lake", args := #["exe", "hepLean_style_lint"]}
+  println! styleLint.stdout
   println! "Building ... "
   let build ← IO.Process.output {cmd := "lake", args := #["build"]}
   println! build.stdout
   println! "File imports ... "
   let importCheck ← IO.Process.output {cmd := "lake", args := #["exe", "check_file_imports"]}
   println! importCheck.stdout
-  println! "Style lint ... "
-  let styleLint ← IO.Process.output {cmd := "lake", args := #["exe", "hepLean_style_lint"]}
-  println! styleLint.stdout
   println! "Doc check ..."
   let docCheck ← IO.Process.output {cmd := "lake", args := #["exe", "no_docs"]}
   println! docCheck.stdout