diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
index 2375989..8f14a5d 100644
--- a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
+++ b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.Basic
 import HepLean.SpaceTime.MinkowskiMetric
 import Mathlib.Algebra.Lie.Classical
 /-!
@@ -42,7 +41,7 @@ lemma mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1
   simpa [LieAlgebra.Orthogonal.so', IsSkewAdjoint, IsAdjointPair] using h
 
 lemma mem_iff {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ} :
-  A ∈ lorentzAlgebra ↔ Aᵀ * η  = - η * A :=
+    A ∈ lorentzAlgebra ↔ Aᵀ * η  = - η * A :=
   Iff.intro (fun h => transpose_eta ⟨A, h⟩) (fun h => mem_of_transpose_eta_eq_eta_mul_self h)
 
 lemma mem_iff'  (A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) :
diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean
index 9975707..30d2b82 100644
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.MinkowskiMetric
-import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
 import HepLean.SpaceTime.LorentzVector.NormOne
 /-!
 # The Lorentz Group
@@ -24,11 +23,8 @@ identity.
 
 -/
 
-
 noncomputable section
 
-
-open Manifold
 open Matrix
 open Complex
 open ComplexConjugate
@@ -159,7 +155,6 @@ open minkowskiMetric
 
 variable  {Λ Λ' : LorentzGroup d}
 
-@[simp]
 lemma coe_inv  : (Λ⁻¹).1 = Λ.1⁻¹:= by
   refine (inv_eq_left_inv ?h).symm
   exact mem_iff_dual_mul_self.mp Λ.2
diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
index 7719ec4..ea7c655 100644
--- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
@@ -21,7 +21,6 @@ matrices.
 noncomputable section
 
 
-open Manifold
 open Matrix
 open Complex
 open ComplexConjugate
diff --git a/HepLean/SpaceTime/LorentzGroup/Proper.lean b/HepLean/SpaceTime/LorentzGroup/Proper.lean
index 56b1ff7..2457446 100644
--- a/HepLean/SpaceTime/LorentzGroup/Proper.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Proper.lean
@@ -15,7 +15,6 @@ We define the give a series of lemmas related to the determinant of the lorentz
 noncomputable section
 
 
-open Manifold
 open Matrix
 open Complex
 open ComplexConjugate
diff --git a/HepLean/SpaceTime/LorentzVector/Basic.lean b/HepLean/SpaceTime/LorentzVector/Basic.lean
index 72d9a06..45543c2 100644
--- a/HepLean/SpaceTime/LorentzVector/Basic.lean
+++ b/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
diff --git a/HepLean/SpaceTime/LorentzVector/NormOne.lean b/HepLean/SpaceTime/LorentzVector/NormOne.lean
index 3e96884..532d8dd 100644
--- a/HepLean/SpaceTime/LorentzVector/NormOne.lean
+++ b/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
 
diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean
index 27ad271..aba0497 100644
--- a/HepLean/SpaceTime/MinkowskiMetric.lean
+++ b/HepLean/SpaceTime/MinkowskiMetric.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzVector.Basic
 import Mathlib.Algebra.Lie.Classical
-import Mathlib.LinearAlgebra.QuadraticForm.Basic
 /-!
 
 # The Minkowski Metric
@@ -33,6 +32,7 @@ namespace minkowskiMatrix
 
 variable {d : ℕ}
 
+/-- Notation for `minkowskiMatrix`. -/
 scoped[minkowskiMatrix] notation "η" => minkowskiMatrix
 
 @[simp]
@@ -116,6 +116,7 @@ open LorentzVector
 variable {d : ℕ}
 variable (v w : LorentzVector d)
 
+/-- Notation for `minkowskiMetric`. -/
 scoped[minkowskiMetric] notation "⟪" v "," w "⟫ₘ" => minkowskiMetric v w
 /-!
 
@@ -318,17 +319,14 @@ lemma basis_left (μ : Fin 1 ⊕ Fin d)  : ⟪e μ, v⟫ₘ  = η μ μ * v μ :
     simp [stdBasis_apply, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
   · simp [stdBasis_apply, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
 
-@[simp]
 lemma on_timeVec : ⟪timeVec, @timeVec d⟫ₘ = 1 := by
   simp only [timeVec, Fin.isValue, basis_left, minkowskiMatrix,
     LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_apply_eq, Sum.elim_inl, stdBasis_apply,
     ↓reduceIte, mul_one]
 
-@[simp]
 lemma on_basis_mulVec (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, Λ *ᵥ e ν⟫ₘ = η μ μ * Λ μ ν  := by
   simp [basis_left, mulVec, dotProduct, stdBasis_apply]
 
-@[simp]
 lemma on_basis (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, e ν⟫ₘ = η μ ν := by
   rw [basis_left, stdBasis_apply]
   by_cases h : μ = ν
diff --git a/HepLean/SpaceTime/SL2C/Basic.lean b/HepLean/SpaceTime/SL2C/Basic.lean
index 34e6ee2..d24152c 100644
--- a/HepLean/SpaceTime/SL2C/Basic.lean
+++ b/HepLean/SpaceTime/SL2C/Basic.lean
@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzGroup.Basic
 import Mathlib.RepresentationTheory.Basic
+import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
 /-!
 # The group SL(2, ℂ) and it's relation to the Lorentz group
 
@@ -86,7 +87,8 @@ In the next section we will restrict this homomorphism to the restricted Lorentz
 
 lemma iff_det_selfAdjoint (Λ : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ):  Λ ∈ LorentzGroup 3 ↔
     ∀ (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)),
-    det ((toSelfAdjointMatrix ∘ toLin LorentzVector.stdBasis LorentzVector.stdBasis Λ ∘ toSelfAdjointMatrix.symm) x).1
+    det ((toSelfAdjointMatrix ∘
+    toLin LorentzVector.stdBasis LorentzVector.stdBasis Λ ∘ toSelfAdjointMatrix.symm) x).1
     = det x.1 := by
   rw [LorentzGroup.mem_iff_norm]
   apply Iff.intro