refactor: Lint

HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean

@@ -162,6 +162,5 @@ theorem special_case {S : (PureU1 (2 * n.succ.succ + 1)).Sols}
   have ht := special_case_lineInCubic_perm h
   exact lineInCubicPerm_zero ht
 
-
 end Odd
 end PureU1

HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean

@@ -298,7 +298,7 @@ lemma cubic_v_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.
     ring_nf
     exact add_eq_zero_iff_neg_eq.mpr (id (Eq.symm h))
   have h'' : (1 * (S.w * S.w) + (-1) * S.w + 1) ≠ 0 := by
-    refine quadratic_ne_zero_of_discrim_ne_sq ?_  S.w
+    refine quadratic_ne_zero_of_discrim_ne_sq ?_ S.w
     intro s
     by_contra hn
     have h : s ^ 2 < 0 := by

HepLean/FeynmanDiagrams/Basic.lean

@@ -59,19 +59,18 @@ variable (P : PreFeynmanRule)
 
 /-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)`
   to `Over (P.VertexLabel)` induced by projections on products. -/
-@[simps!]
 def toVertex {𝓔 𝓥 : Type} : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over 𝓥 :=
   Over.map <| Prod.snd ∘ Prod.snd
 
 /-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)`
   to `Over (P.EdgeLabel)` induced by projections on products. -/
-@[simps!]
+@[simps! obj_left obj_hom map_left map_right]
 def toEdge {𝓔 𝓥 : Type} : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over 𝓔 :=
   Over.map <| Prod.fst ∘ Prod.snd
 
 /-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)`
   to `Over (P.HalfEdgeLabel)` induced by projections on products. -/
-@[simps!]
+@[simps! obj_left obj_hom map_left map_right]
 def toHalfEdge {𝓔 𝓥 : Type} : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel :=
   Over.map Prod.fst
 
@@ -477,7 +476,7 @@ def edgeVertexEquiv {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 :
   right_inv := by aesop_cat
 
 /-- The functor of over-categories generated by `edgeVertexMap`. -/
-@[simps!]
+@[simps! obj_left obj_hom map_left map_right]
 def edgeVertexFunc {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) :
     Over (P.HalfEdgeLabel × F.𝓔 × F.𝓥) ⥤ Over (P.HalfEdgeLabel × G.𝓔 × G.𝓥) :=
   Over.map <| edgeVertexMap 𝓔 𝓥

HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean

@@ -141,13 +141,11 @@ lemma normSq_eq_innerProd_self (φ : HiggsField) (x : SpaceTime) :
 
 -/
 
-@[simp]
 lemma normSq_apply_im_zero (φ : HiggsField) (x : SpaceTime) :
     ((Complex.ofRealHom ‖φ x‖) ^ 2).im = 0 := by
   rw [sq]
   simp only [ofRealHom_eq_coe, mul_im, ofReal_re, ofReal_im, mul_zero, zero_mul, add_zero]
 
-@[simp]
 lemma normSq_apply_re_self (φ : HiggsField) (x : SpaceTime) :
     ((Complex.ofRealHom ‖φ x‖) ^ 2).re = φ.normSq x := by
   rw [sq]

HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean

@@ -53,7 +53,7 @@ lemma coMetric_basis_expand : {η' | μ ν}ᵀ.tensor =
       rfl
 
 /-- Provides the explicit expansion of the co-metric tensor in terms of the basis elements, as
-a tensor tree.-/
+a tensor tree. -/
 lemma coMetric_basis_expand_tree : {η' | μ ν}ᵀ.tensor =
     (TensorTree.add (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 0))) <|
     TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 1)))) <|

HepLean/Tensors/Tree/Elab.lean

@@ -33,7 +33,7 @@ import HepLean.Tensors.ComplexLorentz.Basic
   `{T | μ ν ⊗ T3 | μ σ}ᵀ` is `contr 0 1 _ (prodNode (tensorNode T1) (tensorNode T3))`.
   `{T | μ ν ⊗ T3 | μ ν }ᵀ` is
   `contr 0 0 _ (contr 0 1 _ (prodNode (tensorNode T1) (tensorNode T3)))`.
-- If `T4` is a tensor  `S.F (OverColor.mk ![c2, c1])` then
+- If `T4` is a tensor `S.F (OverColor.mk ![c2, c1])` then
   `{T | μ ν + T4 | ν μ }ᵀ`is `addNode (tensorNode T) (perm _ (tensorNode T4))` where `_`
   is the permutation of the two indices of `T4`.
   `{T | μ ν = T4 | ν μ }ᵀ` is `(tensorNode T).tensor = (perm _ (tensorNode T4)).tensor` is the
@@ -42,8 +42,8 @@ import HepLean.Tensors.ComplexLorentz.Basic
 ## Comments
 
 - In all of theses expressions `μ`, `ν` etc are free. It does not matter what they are called,
- Lean will elaborate them in the same way. I.e. `{T | μ ν ⊗ T3 | μ ν }ᵀ` is exactly the same
- to Lean as `{T | α β ⊗ T3 | α β }ᵀ`.
+  Lean will elaborate them in the same way. I.e. `{T | μ ν ⊗ T3 | μ ν }ᵀ` is exactly the same
+  to Lean as `{T | α β ⊗ T3 | α β }ᵀ`.
 - Note that compared to ordinary index notation, we do not rise or lower the indices.
   This is for two reasons: 1) It is difficult to make this general for all tensor species,
   2) It is a reduency in ordinary index notation, since the tensor `T` itself already tells you