refactor: Lint

HepLean/Tensors/OverColor/Discrete.lean

@@ -29,7 +29,7 @@ noncomputable section
 def pair : Discrete C ⥤ Rep k G := F ⊗ F
 
 /-- The isomorphism between the image of `(pair F).obj` and
-  `(lift.obj F).obj (OverColor.mk ![c,c])`.  -/
+  `(lift.obj F).obj (OverColor.mk ![c,c])`. -/
 def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverColor.mk ![c,c]) := by
   symm
   apply ((lift.obj F).mapIso fin2Iso).trans
@@ -50,11 +50,11 @@ def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverCol
 
 /-- The functor taking `c` to `F c ⊗ F (τ c)`. -/
 def pairτ (τ : C → C) : Discrete C ⥤ Rep k G :=
-  F ⊗ ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤  Discrete C) ⋙ F)
+  F ⊗ ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F)
 
 /-- The functor taking `c` to `F (τ c) ⊗ F c`. -/
 def τPair (τ : C → C) : Discrete C ⥤ Rep k G :=
-  ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤  Discrete C) ⋙ F) ⊗ F
+  ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F) ⊗ F
 
 end
 end Discrete

HepLean/Tensors/OverColor/Iso.lean

@@ -42,7 +42,7 @@ def mkIso {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2 :=
 
 /-- The isomorphism splitting a `mk c` for `Fin 2 → C` into the tensor product of
   the `Fin 1 → C` maps defined by `c 0` and `c 1`. -/
-def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] :=by
+def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] := by
   let e1 : Fin 2 ≃ Fin 1 ⊕ Fin 1 := (finSumFinEquiv (n := 1)).symm
   apply (equivToIso e1).trans
   apply (mkSum _).trans
@@ -175,7 +175,6 @@ def contrPairFin1Fin1 (τ : C → C) (c : Fin 1 ⊕ Fin 1 → C)
 
 variable {k : Type} [CommRing k] {G : Type} [Group G]
 
-
 /-- The Isomorphism between a `Fin n.succ.succ → C` and the product containing an object in the
   image of `contrPair` based on the given values. -/
 def contrPairEquiv {n : ℕ} (τ : C → C) (c : Fin n.succ.succ → C) (i : Fin n.succ.succ)
@@ -188,7 +187,6 @@ def contrPairEquiv {n : ℕ} (τ : C → C) (c : Fin n.succ.succ → C) (i : Fin
     (contrPairFin1Fin1 τ ((c ∘ ⇑(finExtractTwo i j).symm) ∘ Sum.inl) (by simpa using h)) <|
     mkIso (by ext x; simp)
 
-
 /-- Given a function `c` from `Fin 1` to `C`, this function returns a morphism
   from `mk c` to `mk ![c 0]`. --/
 def permFinOne (c : Fin 1 → C) : mk c ⟶ mk ![c 0] :=
@@ -197,7 +195,7 @@ def permFinOne (c : Fin 1 → C) : mk c ⟶ mk ![c 0] :=
     fin_cases x
     rfl)).hom
 
-/-- This a function that takes a function `c` from `Fin 2` to  `C` and
+/-- This a function that takes a function `c` from `Fin 2` to `C` and
 returns a morphism from `mk c` to `mk ![c 0, c 1]`. --/
 def permFinTwo (c : Fin 2 → C) : mk c ⟶ mk ![c 0, c 1] :=
   (mkIso (by
@@ -213,6 +211,5 @@ def permFinThree (c : Fin 3 → C) : mk c ⟶ mk ![c 0, c 1, c 2] :=
     fin_cases x <;>
     rfl)).hom
 
-
 end OverColor
 end IndexNotation

HepLean/Tensors/OverColor/Lift.lean

@@ -666,14 +666,14 @@ between the vector space obtained by applying the lift of `F` and that obtained
 `F`.
 --/
 def forgetLiftAppV (c : C) : ((lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c))).V ≃ₗ[k]
-     (F.obj (Discrete.mk c)).V :=
+    (F.obj (Discrete.mk c)).V :=
   (PiTensorProduct.subsingletonEquiv 0 :
-    (⨂[k] (_ : Fin 1), (F.obj (Discrete.mk c))) ≃ₗ[k] F.obj (Discrete.mk c) )
+    (⨂[k] (_ : Fin 1), (F.obj (Discrete.mk c))) ≃ₗ[k] F.obj (Discrete.mk c))
 
 /-- The `forgetLiftAppV` function takes an object `c` of type `C` and returns a isomorphism
 between the objects obtained by applying the lift of `F` and that obtained by applying
-`F`.  -/
-def forgetLiftApp (c : C) : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1 ) => c))
+`F`. -/
+def forgetLiftApp (c : C) : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c))
     ≅ F.obj (Discrete.mk c) :=
     Action.mkIso (forgetLiftAppV F c).toModuleIso
   (fun g => by

HepLean/Tensors/Tree/Basic.lean

@@ -67,7 +67,7 @@ def metric (c : S.C) : S.F.obj (OverColor.mk ![c, c]) :=
 -/
 
 /-- The isomorphism of objects in `Rep S.k S.G` given an `i` in `Fin n.succ.succ` and
- a `j` in `Fin n.succ` allowing us to undertake contraction. -/
+  a `j` in `Fin n.succ` allowing us to undertake contraction. -/
 def contrIso {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)) :
     S.F.obj (OverColor.mk c) ≅ ((OverColor.Discrete.pairτ S.FDiscrete S.τ).obj
@@ -168,12 +168,12 @@ abbrev twoNodeE (S : TensorStruct) (c1 c2 : S.C)
 
 /-- The node `constTwoNodeE` of a tensor tree, with all arguments explicit. -/
 abbrev constTwoNodeE (S : TensorStruct) (c1 c2 : S.C)
-    (v :  𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) :
+    (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) :
     TensorTree S ![c1, c2] := constTwoNode v
 
 /-- The node `constThreeNodeE` of a tensor tree, with all arguments explicit. -/
-abbrev constThreeNodeE (S : TensorStruct) (c1 c2  c3 : S.C)
-    (v :  𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2) ⊗
+abbrev constThreeNodeE (S : TensorStruct) (c1 c2 c3 : S.C)
+    (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2) ⊗
       S.FDiscrete.obj (Discrete.mk c3)) : TensorTree S ![c1, c2, c3] :=
     constThreeNode v
 
@@ -205,7 +205,7 @@ def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (Over
   | smul a t => a • t.tensor
   | prod t1 t2 => (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom
     ((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor))
-  | contr i j h t  => (S.contrMap _ i j h).hom t.tensor
+  | contr i j h t => (S.contrMap _ i j h).hom t.tensor
   | _ => 0
 
 lemma tensor_tensorNode {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) :

HepLean/Tensors/Tree/Elab.lean

@@ -178,9 +178,11 @@ def termNodeSyntax (T : Term) : TermElabM Term := do
       | _ => throwError "Could not create terminal node syntax (termNodeSyntax). "
     | _ => return Syntax.mkApp (mkIdent ``TensorTree.vecNode) #[T]
   | 2, 1 =>
-    match ← isDefEq type (← stringToType "CoeSort.coe leftHanded ⊗ CoeSort.coe Lorentz.complexContr") with
+    match ← isDefEq type (← stringToType
+      "CoeSort.coe leftHanded ⊗ CoeSort.coe Lorentz.complexContr") with
     | true => return Syntax.mkApp (mkIdent ``TensorTree.twoNodeE)
-                #[mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.upL, mkIdent ``Fermion.Color.up, T]
+                #[mkIdent ``Fermion.complexLorentzTensor,
+                mkIdent ``Fermion.Color.upL, mkIdent ``Fermion.Color.up, T]
     | _ => return Syntax.mkApp (mkIdent ``TensorTree.twoNode) #[T]
   | 3, 1 => return Syntax.mkApp (mkIdent ``TensorTree.threeNode) #[T]
   | 1, 2 => return Syntax.mkApp (mkIdent ``TensorTree.constVecNode) #[T]
@@ -191,7 +193,7 @@ def termNodeSyntax (T : Term) : TermElabM Term := do
       println! "here"
       return Syntax.mkApp (mkIdent ``TensorTree.constTwoNodeE) #[
         mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.down,
-         mkIdent ``Fermion.Color.down, T]
+        mkIdent ``Fermion.Color.down, T]
     | _ => return Syntax.mkApp (mkIdent ``TensorTree.constTwoNode) #[T]
   | 3, 2 =>
     /- Specific types. -/
@@ -238,7 +240,8 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
 /-- For each element of `l : List (ℕ × ℕ)` applies `TensorTree.contr` to the given term. -/
 def contrSyntax (l : List (ℕ × ℕ)) (T : Term) : Term :=
   l.foldl (fun T' (x0, x1) => Syntax.mkApp (mkIdent ``TensorTree.contr)
-    #[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), mkIdent `sorry, mkIdent ``rfl, T']) T
+    #[Syntax.mkNumLit (toString x1),
+    Syntax.mkNumLit (toString x0), mkIdent ``rfl, T']) T
 
 /-- Creates the syntax associated with a tensor node. -/
 def syntaxFull (stx : Syntax) : TermElabM Term := do