refactor: Lint

HepLean/Mathematics/Fin.lean

@@ -240,7 +240,7 @@ lemma finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) :
   rfl
 
 /-- Given an equivalence `Fin n.succ.succ ≃ Fin n.succ.succ`, and an `i : Fin n.succ.succ`,
-  the map  `Fin n.succ → Fin n.succ` obtained by dropping `i` and it's image. -/
+  the map `Fin n.succ → Fin n.succ` obtained by dropping `i` and it's image. -/
 def finExtractOnPermHom (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
     Fin n.succ → Fin n.succ := fun x => predAboveI (σ i) (σ ((finExtractOne i).symm (Sum.inr x)))
 
@@ -269,7 +269,7 @@ lemma finExtractOnPermHom_inv (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fi
   omega
 
 /-- Given an equivalence `Fin n.succ.succ ≃ Fin n.succ.succ`, and an `i : Fin n.succ.succ`,
-  the equivalence  `Fin n.succ ≃ Fin n.succ` obtained by dropping `i` and it's image. -/
+  the equivalence `Fin n.succ ≃ Fin n.succ` obtained by dropping `i` and it's image. -/
 def finExtractOnePerm (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
     Fin n.succ ≃ Fin n.succ where
   toFun x := finExtractOnPermHom i σ x

HepLean/Tensors/ComplexLorentz/Lemmas.lean

@@ -96,7 +96,7 @@ lemma symm_contract_antiSymm (A : (Lorentz.complexContr ⊗ Lorentz.complexContr
   rw [perm_contr]
   rw [perm_tensor_eq (contr_tensor_eq (contr_tensor_eq (prod_perm_right _ _ _ _)))]
   rw [perm_tensor_eq (contr_tensor_eq (perm_contr _ _))]
-  rw [perm_tensor_eq (perm_contr _  _)]
+  rw [perm_tensor_eq (perm_contr _ _)]
   rw [perm_perm]
   nth_rewrite 1 [perm_tensor_eq (contr_contr _ _ _)]
   rw [perm_perm]

HepLean/Tensors/OverColor/Discrete.lean

@@ -49,7 +49,7 @@ def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverCol
     rfl
 
 /-- The isomorphism between `F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2)` and
-  `(lift.obj F).obj (OverColor.mk ![c1,c2])` fored by the tensorate.  -/
+  `(lift.obj F).obj (OverColor.mk ![c1,c2])` fored by the tensorate. -/
 def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) ≅
     (lift.obj F).obj (OverColor.mk ![c1,c2]) := by
   symm

HepLean/Tensors/Tree/Elab.lean

@@ -183,7 +183,6 @@ def termNodeSyntax (T : Term) : TermElabM Term := do
   let strType := toString type
   let n := (String.splitOn strType "CategoryTheory.MonoidalCategoryStruct.tensorObj").length
   let const := (String.splitOn strType "Quiver.Hom").length
-  println! "n: {n}, const: {const}"
   match n, const with
   | 1, 1 =>
     match type with
@@ -266,7 +265,7 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
   let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x)
   return ind.filter (fun x => indFilt.count x ≤ 1)
 
-/-- Takes a list and puts conseutive  elements into pairs.
+/-- Takes a list and puts conseutive elements into pairs.
   e.g. [0, 1, 2, 3] becomes [(0, 1), (2, 3)]. -/
 def toPairs (l : List ℕ) : List (ℕ × ℕ) :=
   match l with
@@ -364,8 +363,6 @@ partial def syntaxFull (stx : Syntax) : TermElabM Term := do
   | `(tensorExpr| $_:term | $[$args]*) => TensorNode.syntaxFull stx
   | `(tensorExpr| $a:tensorExpr ⊗ $b:tensorExpr) => do
       let prodSyntax := prodSyntax (← syntaxFull a) (← syntaxFull b)
-      println! (← getContrPos stx)
-      println! TensorNode.contrListAdjust (← getContrPos stx)
       let contrSyntax := contrSyntax (← getContrPos stx) prodSyntax
       return contrSyntax
   | `(tensorExpr| ($a:tensorExpr)) => do
@@ -383,7 +380,6 @@ def negSyntax (T1 : Term) : Term :=
 
 end negNode
 
-
 /-- Returns the full list of indices after contraction. TODO: Include evaluation. -/
 partial def getIndicesFull (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
   match stx with

HepLean/Tensors/Tree/NodeIdentities/Basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.Tree.Basic
-import LLMLean
 /-!
 
 ## Basic node identities

HepLean/Tensors/Tree/NodeIdentities/PermProd.lean

@@ -51,19 +51,19 @@ theorem prod_perm_left (t : TensorTree S c) (t2 : TensorTree S c2) :
     Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply]
   change (S.F.map (σ ▷ OverColor.mk c2) ≫ S.F.map (equivToIso finSumFinEquiv).hom).hom _ = _
   rw [← S.F.map_comp, ← (Iso.hom_inv_id_assoc (equivToIso finSumFinEquiv)
-      (σ ▷ OverColor.mk c2 ≫ (equivToIso finSumFinEquiv).hom)),  S.F.map_comp]
+      (σ ▷ OverColor.mk c2 ≫ (equivToIso finSumFinEquiv).hom)), S.F.map_comp]
   rfl
 
 /-- When a `prod` acts on a `perm` node in the right entry, the `perm` node can be moved through
   the `prod` node via left-whiskering. -/
-theorem prod_perm_right  (t2 : TensorTree S c2) (t : TensorTree S c) :
+theorem prod_perm_right (t2 : TensorTree S c2) (t : TensorTree S c) :
     (prod t2 (perm σ t)).tensor = (perm (permProdRight c2 σ) (prod t2 t)).tensor := by
   simp only [prod_tensor, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
     Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
     Action.FunctorCategoryEquivalence.functor_obj_obj, perm_tensor]
-  change  (S.F.map (equivToIso finSumFinEquiv).hom).hom
+  change (S.F.map (equivToIso finSumFinEquiv).hom).hom
     (((S.F.obj (OverColor.mk c2) ◁ S.F.map σ) ≫ S.F.μ (OverColor.mk c2) (OverColor.mk c')).hom
-       (t2.tensor ⊗ₜ[S.k] t.tensor))  = _
+    (t2.tensor ⊗ₜ[S.k] t.tensor)) = _
   rw [S.F.μ_natural_right]
   simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom,
     Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
@@ -73,7 +73,7 @@ theorem prod_perm_right  (t2 : TensorTree S c2) (t : TensorTree S c) :
   have hx : OverColor.mk c2 ◁ σ ≫ (equivToIso finSumFinEquiv).hom =
     (equivToIso finSumFinEquiv).hom ≫ (permProdRight c2 σ) := by
     simp only [Functor.id_obj, mk_hom, permProdRight, Iso.hom_inv_id_assoc]
-  rw [hx,  S.F.map_comp]
+  rw [hx, S.F.map_comp]
   rfl
 
 end TensorTree