refactor: Lint

HepLean/SpaceTime/LorentzVector/Basic.lean

@@ -4,10 +4,7 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Data.Complex.Exponential
-import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners
 import Mathlib.Analysis.InnerProductSpace.PiL2
-import Mathlib.LinearAlgebra.Matrix.DotProduct
-import LeanCopilot
 /-!
 
 # Lorentz vectors
@@ -62,6 +59,7 @@ def time : ℝ := v (Sum.inl 0)
 @[simps!]
 noncomputable def stdBasis : Basis (Fin 1 ⊕ Fin (d)) ℝ (LorentzVector d) := Pi.basisFun ℝ _
 
+/-- Notation for `stdBasis`. -/
 scoped[LorentzVector] notation "e" => stdBasis
 
 lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : e μ ν = if μ = ν then 1 else 0 := by
@@ -72,12 +70,10 @@ lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : e μ ν = if μ = ν then 1 els
 /-- The standard unit time vector. -/
 noncomputable abbrev timeVec : (LorentzVector d) := e (Sum.inl 0)
 
-@[simp]
 lemma timeVec_space : (@timeVec d).space = 0 := by
   funext i
   simp only [space, Function.comp_apply, stdBasis_apply, Fin.isValue, ↓reduceIte, PiLp.zero_apply]
 
-@[simp]
 lemma timeVec_time: (@timeVec d).time = 1 := by
   simp only [time, Fin.isValue, stdBasis_apply, ↓reduceIte]
 
@@ -106,19 +102,14 @@ def spaceReflectionLin : LorentzVector d →ₗ[ℝ] LorentzVector d where
       apply smul_eq_mul
     · simp [ HSMul.hSMul, SMul.smul]
 
-
 /-- The reflection of space. -/
 @[simp]
 def spaceReflection : LorentzVector d := spaceReflectionLin v
 
-@[simp]
 lemma spaceReflection_space : v.spaceReflection.space = - v.space := by
   rfl
 
-@[simp]
 lemma spaceReflection_time : v.spaceReflection.time = v.time := by
   rfl
 
-
-
 end LorentzVector

HepLean/SpaceTime/LorentzVector/NormOne.lean

@@ -13,6 +13,7 @@ import HepLean.SpaceTime.MinkowskiMetric
 
 open minkowskiMetric
 
+/-- The set of Lorentz vectors with norm 1. -/
 @[simp]
 def NormOneLorentzVector (d : ℕ) : Set (LorentzVector d) :=
   fun x => ⟪x, x⟫ₘ = 1
@@ -105,11 +106,8 @@ lemma mem_iff : v ∈ FuturePointing d ↔ 0 < v.1.time := by
   rfl
 
 lemma mem_iff_time_nonneg : v ∈ FuturePointing d ↔ 0 ≤ v.1.time := by
-  refine Iff.intro (fun h => ?_) (fun h => ?_)
-  exact le_of_lt ((mem_iff v).mp h)
-  have h1 := (mem_iff v).mp
-  simp at h1
-  rw [@time_nonneg_iff] at h
+  refine Iff.intro (fun h => le_of_lt h) (fun h => ?_)
+  rw [time_nonneg_iff] at h
   rw [mem_iff]
   linarith