refactor: Lint

HepLean/AnomalyCancellation/SM/Permutations.lean

@@ -31,7 +31,7 @@ def PermGroup (n : ℕ) := ∀ (_ : Fin 5), Equiv.Perm (Fin n)
 variable {n : ℕ}
 
 /-- The type `PermGroup n` inherits the instance of a group from it's
-  target space `Equiv.Perm`.  -/
+  target space `Equiv.Perm`. -/
 @[simp]
 instance : Group (PermGroup n) := Pi.group
 

HepLean/FeynmanDiagrams/Basic.lean

@@ -177,7 +177,7 @@ instance [IsFinitePreFeynmanRule P] (v : P.EdgeLabel) : DecidableEq (P.edgeLabel
   IsFinitePreFeynmanRule.edgeMapDecidable v
 
 /-- It is decidable to check whether a half edge of a diagram (an object in
-   `Over (P.HalfEdgeLabel × 𝓔 × 𝓥)`) corresponds to a given vertex. -/
+  `Over (P.HalfEdgeLabel × 𝓔 × 𝓥)`) corresponds to a given vertex. -/
 instance preimageVertexDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓥] (v : 𝓥)
     (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) :
     DecidablePred fun x => x ∈ (P.toVertex.obj F).hom ⁻¹' {v} := fun y =>
@@ -186,7 +186,7 @@ instance preimageVertexDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓥] (v :
   | isFalse h => isFalse h
 
 /-- It is decidable to check whether a half edge of a diagram (an object in
-   `Over (P.HalfEdgeLabel × 𝓔 × 𝓥)`) corresponds to a given edge. -/
+  `Over (P.HalfEdgeLabel × 𝓔 × 𝓥)`) corresponds to a given edge. -/
 instance preimageEdgeDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓔] (v : 𝓔)
     (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) :
     DecidablePred fun x => x ∈ (P.toEdge.obj F).hom ⁻¹' {v} := fun y =>

HepLean/Meta/Basic.lean

@@ -59,9 +59,9 @@ def Imports.getUserConsts (imp : Import) : MetaM (Array ConstantInfo) := do
   let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.belowSuffix)
   let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.ibelowSuffix)
   /- Removing syntax category declarations. -/
-  let x := x.filter (fun c => ¬ c.name.toString = "Informal.informalAssignment.quot" )
-  let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.indexExpr.quot" )
-  let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.tensorExpr.quot" )
+  let x := x.filter (fun c => ¬ c.name.toString = "Informal.informalAssignment.quot")
+  let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.indexExpr.quot")
+  let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.tensorExpr.quot")
   pure x
 
 /-- Lines from import. -/
@@ -76,21 +76,20 @@ def Imports.getLines (imp : Import) : IO (Array String) := do
 
 -/
 
-
 /-- Turns a name into a Lean file. -/
 def Name.toFile (c : Name) : MetaM String := do
   return s!"./{c.toString.replace "." "/" ++ ".lean"}"
 
 /-- Given a name, returns the line number. -/
 def Name.lineNumber (c : Name) : MetaM Nat := do
-  match ← findDeclarationRanges? c  with
+  match ← findDeclarationRanges? c with
   | some decl => pure decl.range.pos.line
   | none => panic! s!"{c} is a declaration without position"
 
 /-- Returns the location of a name. -/
 def Name.location (c : Name) : MetaM String := do
   let env ← getEnv
-  let x := env.getModuleFor?  c
+  let x := env.getModuleFor? c
   match x with
   | some decl => pure ((← Name.toFile decl) ++ ":" ++ toString (← Name.lineNumber c) ++ " "
     ++ c.toString)
@@ -98,7 +97,7 @@ def Name.location (c : Name) : MetaM String := do
 
 /-- Determines if a name has a location. -/
 def Name.hasPos (c : Name) : MetaM Bool := do
-  match ← findDeclarationRanges? c  with
+  match ← findDeclarationRanges? c with
   | some _ => pure true
   | none => pure false
 
@@ -116,7 +115,7 @@ def noDefs : MetaM Nat := do
   let x ← imports.mapM Imports.getUserConsts
   let x := x.flatten
   let x := x.filter (fun c => c.isDef)
-  let x ←  x.filterM (fun c => (Name.hasPos c.name))
+  let x ← x.filterM (fun c => (Name.hasPos c.name))
   pure x.toList.length
 
 /-- Number of definitions. -/
@@ -125,7 +124,7 @@ def noLemmas : MetaM Nat := do
   let x ← imports.mapM Imports.getUserConsts
   let x := x.flatten
   let x := x.filter (fun c => ¬ c.isDef)
-  let x ←  x.filterM (fun c => (Name.hasPos c.name))
+  let x ← x.filterM (fun c => (Name.hasPos c.name))
   pure x.toList.length
 
 /-- Number of definitions without a doc-string. -/
@@ -134,7 +133,7 @@ def noDefsNoDocString : MetaM Nat := do
   let x ← imports.mapM Imports.getUserConsts
   let x := x.flatten
   let x := x.filter (fun c => c.isDef)
-  let x ←  x.filterM (fun c => (Name.hasPos c.name))
+  let x ← x.filterM (fun c => (Name.hasPos c.name))
   let x ← x.filterM (fun c => do
     return Bool.not (← (Name.hasDocString c.name)))
   pure x.toList.length
@@ -145,7 +144,7 @@ def noLemmasNoDocString : MetaM Nat := do
   let x ← imports.mapM Imports.getUserConsts
   let x := x.flatten
   let x := x.filter (fun c => ¬ c.isDef)
-  let x ←  x.filterM (fun c => (Name.hasPos c.name))
+  let x ← x.filterM (fun c => (Name.hasPos c.name))
   let x ← x.filterM (fun c => do
     return Bool.not (← (Name.hasDocString c.name)))
   pure x.toList.length

HepLean/StandardModel/HiggsBoson/GaugeAction.lean

@@ -144,7 +144,7 @@ def rotateGuageGroup {φ : HiggsVec} (hφ : φ ≠ 0) : GaugeGroupI :=
     ⟨1, ⟨(rotateMatrix φ), rotateMatrix_specialUnitary hφ⟩, 1⟩
 
 /-- Acting on a non-zero Higgs vector with its rotation matrix gives a vector which is
-  zero in the first componenent and a positive real in the second component.  -/
+  zero in the first componenent and a positive real in the second component. -/
 lemma rotateGuageGroup_apply {φ : HiggsVec} (hφ : φ ≠ 0) :
     rep (rotateGuageGroup hφ) φ = ![0, Complex.ofRealHom ‖φ‖] := by
   rw [rep_apply]

HepLean/Tensors/OverColor/Basic.lean

@@ -63,7 +63,7 @@ def toEquiv (m : f ⟶ g) : f.left ≃ g.left where
   right_inv := by
     simpa only [Over.comp_left] using congrFun (congrArg (fun x => x.left) m.inv_hom_id)
 
-/-- The equivalence of types underlying the identity morphism is the reflexive equivalence.  -/
+/-- The equivalence of types underlying the identity morphism is the reflexive equivalence. -/
 @[simp]
 lemma toEquiv_id (f : OverColor C) : toEquiv (𝟙 f) = Equiv.refl f.left := by
   rfl