refactor: Lint

HepLean/Lorentz/ComplexTensor/Bispinors/Basic.lean

@@ -31,6 +31,10 @@ open Lorentz
 
 -/
 
+TODO "To increase the speed of these files `(vecNodeE complexLorentzTensor .up p).tensor | μ` is
+  written out expliclity. Notation should be introduced so that we can just write `p | μ` or
+  similar without slowing things down."
+
 /-- A bispinor `pᵃᵃ` created from a lorentz vector `p^μ`. -/
 def contrBispinorUp (p : complexContr) :=
   {pauliCo | μ α β ⊗ (vecNodeE complexLorentzTensor .up p).tensor | μ}ᵀ.tensor

HepLean/Lorentz/ComplexTensor/Metrics/Basic.lean

@@ -96,17 +96,17 @@ lemma tensorNode_coMetric : {η' | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE
 
 /-- The definitional tensor node relation for `contrMetric`. -/
 lemma tensorNode_contrMetric : {η | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
-  .up .up Lorentz.contrMetric).tensor := by
+    .up .up Lorentz.contrMetric).tensor := by
   rfl
 
 /-- The definitional tensor node relation for `leftMetric`. -/
 lemma tensorNode_leftMetric : {εL | α α'}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
-  .upL .upL Fermion.leftMetric).tensor := by
+    .upL .upL Fermion.leftMetric).tensor := by
   rfl
 
 /-- The definitional tensor node relation for `rightMetric`. -/
 lemma tensorNode_rightMetric : {εR | β β'}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
-  .upR .upR Fermion.rightMetric).tensor:= by
+    .upR .upR Fermion.rightMetric).tensor:= by
   rfl
 
 /-- The definitional tensor node relation for `altLeftMetric`. -/