diff --git a/HepLean.lean b/HepLean.lean
index 6c336db..fa45853 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -56,7 +56,11 @@ import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
 import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
 import HepLean.SpaceTime.Basic
 import HepLean.SpaceTime.CliffordAlgebra
-import HepLean.SpaceTime.LorentzGroup
+import HepLean.SpaceTime.FourVelocity
+import HepLean.SpaceTime.LorentzGroup.Basic
+import HepLean.SpaceTime.LorentzGroup.Boosts
+import HepLean.SpaceTime.LorentzGroup.Orthochronous
+import HepLean.SpaceTime.LorentzGroup.Proper
 import HepLean.SpaceTime.Metric
 import HepLean.StandardModel.Basic
 import HepLean.StandardModel.HiggsBoson.Basic
diff --git a/HepLean/SpaceTime/FourVelocity.lean b/HepLean/SpaceTime/FourVelocity.lean
index f637944..9b60b2d 100644
--- a/HepLean/SpaceTime/FourVelocity.lean
+++ b/HepLean/SpaceTime/FourVelocity.lean
@@ -15,6 +15,7 @@ We define
 -/
 open spaceTime
 
+/-- A `spaceTime` vector for which `ηLin x x = 1`. -/
 @[simp]
 def PreFourVelocity : Set spaceTime :=
   fun x => ηLin x x = 1
@@ -26,6 +27,7 @@ namespace PreFourVelocity
 lemma mem_PreFourVelocity_iff {x : spaceTime} : x ∈ PreFourVelocity ↔ ηLin x x = 1 := by
   rfl
 
+/-- The negative of a `PreFourVelocity` as a `PreFourVelocity`. -/
 def neg (v : PreFourVelocity) : PreFourVelocity := ⟨-v, by
   rw [mem_PreFourVelocity_iff]
   simp only [map_neg, LinearMap.neg_apply, neg_neg]
@@ -68,6 +70,7 @@ lemma zero_nonneg_iff (v : PreFourVelocity) : 0 ≤ v.1 0 ↔ 1 ≤ v.1 0 := by
   · intro h
     linarith
 
+/-- A `PreFourVelocity` is a `FourVelocity` if its time componenet is non-negative. -/
 def IsFourVelocity (v : PreFourVelocity) : Prop := 0 ≤ v.1 0
 
 
@@ -141,6 +144,7 @@ lemma euclid_norm_not_IsFourVelocity_IsFourVelocity {v v' : PreFourVelocity}
 
 end PreFourVelocity
 
+/-- The set of `PreFourVelocity`'s which are four velocities. -/
 def FourVelocity : Set PreFourVelocity :=
   fun x => PreFourVelocity.IsFourVelocity x
 
@@ -158,11 +162,13 @@ lemma time_comp (x : FourVelocity) : x.1.1 0 = √(1 + ‖x.1.1.space‖ ^ 2) :=
   refine Or.inl (And.intro ?_ x.2)
   rw [← PreFourVelocity.zero_sq x.1, sq]
 
+/-- The `FourVelocity` which has all space components zero. -/
 def zero : FourVelocity := ⟨⟨![1, 0, 0, 0], by
   rw [mem_PreFourVelocity_iff, ηLin_expand]; simp⟩, by
   rw [mem_FourVelocity_iff]; simp⟩
 
 
+/-- A continuous path from the zero `FourVelocity` to any other. -/
 noncomputable def pathFromZero (u : FourVelocity) : Path zero u where
   toFun t := ⟨
     ⟨![√(1 + t ^ 2 * ‖u.1.1.space‖ ^ 2), t * u.1.1 1, t * u.1.1 2, t * u.1.1 3],
@@ -189,15 +195,16 @@ noncomputable def pathFromZero (u : FourVelocity) : Path zero u where
     fin_cases i
       <;> continuity
   source' := by
-    simp
+    simp only [Set.Icc.coe_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, space,
+      Fin.isValue, zero_mul, add_zero, Real.sqrt_one]
     rfl
   target' := by
-    simp
+    simp only [Set.Icc.coe_one, one_pow, space, Fin.isValue, one_mul]
     refine SetCoe.ext ?_
     refine SetCoe.ext ?_
     funext i
     fin_cases i
-    simp
+    simp only [Fin.isValue, Fin.zero_eta, Matrix.cons_val_zero]
     exact (time_comp _).symm
     all_goals rfl
 
diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean
index 2e13118..2c2d119 100644
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@@ -113,9 +113,9 @@ def lorentzGroup : Subgroup (GL (Fin 4) ℝ) where
 instance : TopologicalGroup lorentzGroup :=
   Subgroup.instTopologicalGroupSubtypeMem lorentzGroup
 
-@[simps!]
+/-- The lift of a matrix perserving `ηLin` to a Lorentz Group element. -/
 def PreservesηLin.liftLor {Λ : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) :
-  lorentzGroup := ⟨liftGL h, h⟩
+    lorentzGroup := ⟨liftGL h, h⟩
 
 namespace lorentzGroup
 
@@ -127,6 +127,8 @@ def transpose (Λ : lorentzGroup) : lorentzGroup :=
   PreservesηLin.liftLor ((PreservesηLin.iff_transpose Λ.1).mp Λ.2)
 
 
+/-- The continuous map from `GL (Fin 4) ℝ` to `Matrix (Fin 4) (Fin 4) ℝ` whose kernal is
+the Lorentz group. -/
 def kernalMap : C(GL (Fin 4) ℝ, Matrix (Fin 4) (Fin 4) ℝ) where
   toFun Λ := η * Λ.1ᵀ * η * Λ.1
   continuous_toFun := by
diff --git a/HepLean/SpaceTime/LorentzGroup/Boosts.lean b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
index 2de9a49..a0c35ea 100644
--- a/HepLean/SpaceTime/LorentzGroup/Boosts.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
@@ -34,7 +34,7 @@ namespace lorentzGroup
 
 open FourVelocity
 
-
+/-- An auxillary linear map used in the definition of a genearlised boost. -/
 def genBoostAux₁ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where
   toFun x := (2 * ηLin x u) • v.1.1
   map_add' x y := by
@@ -45,7 +45,7 @@ def genBoostAux₁ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where
       RingHom.id_apply]
     rw [← mul_assoc, mul_comm 2 c, mul_assoc, mul_smul]
 
-
+/-- An auxillary linear map used in the definition of a genearlised boost. -/
 def genBoostAux₂ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where
   toFun x := - (ηLin x (u + v) / (1 + ηLin u v)) • (u + v)
   map_add' x y := by
@@ -60,6 +60,8 @@ def genBoostAux₂ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where
     rw [mul_div_assoc, neg_mul_eq_mul_neg, smul_smul]
     rfl
 
+/-- An genearlised boost. This is a Lorentz transformation which takes the four velocity `u`
+to `v`. -/
 def genBoost (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime :=
   LinearMap.id + genBoostAux₁ u v + genBoostAux₂ u v
 
@@ -81,6 +83,7 @@ lemma self (u : FourVelocity) : genBoost u u = LinearMap.id := by
   ring
   rfl
 
+/-- A generalised boost as a matrix. -/
 def toMatrix (u v : FourVelocity) : Matrix (Fin 4) (Fin 4) ℝ :=
   LinearMap.toMatrix stdBasis stdBasis (genBoost u v)
 
@@ -124,7 +127,6 @@ lemma toMatrix_continuous (u : FourVelocity) : Continuous (toMatrix u) := by
   exact fun x => one_plus_ne_zero u x
 
 
-
 lemma toMatrix_PreservesηLin (u v : FourVelocity) : PreservesηLin (toMatrix u v) := by
   intro x y
   rw [toMatrix_mulVec, toMatrix_mulVec, genBoost, genBoostAux₁, genBoostAux₂]
@@ -136,6 +138,7 @@ lemma toMatrix_PreservesηLin (u v : FourVelocity) : PreservesηLin (toMatrix u
   rw [u.1.2, v.1.2, ηLin_symm v u, ηLin_symm u y, ηLin_symm v y]
   ring
 
+/-- A generalised boost as an element of the Lorentz Group. -/
 def toLorentz (u v : FourVelocity) : lorentzGroup :=
   PreservesηLin.liftLor (toMatrix_PreservesηLin u v)
 
diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
index 75b9c9f..832953f 100644
--- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
@@ -46,23 +46,25 @@ def fstCol (Λ : lorentzGroup) : PreFourVelocity := ⟨Λ.1 *ᵥ stdBasis 0, by
   rw [← h00]
   ring⟩
 
+/-- A Lorentz transformation is  `orthochronous` if its `0 0` element is non-negative. -/
 def IsOrthochronous (Λ : lorentzGroup) : Prop := 0 ≤ Λ.1 0 0
 
 lemma IsOrthochronous_iff_transpose (Λ : lorentzGroup) :
     IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) := by
-  simp [IsOrthochronous]
-  simp [transpose]
+  simp only [IsOrthochronous, Fin.isValue, transpose, PreservesηLin.liftLor, PreservesηLin.liftGL,
+    transpose_transpose, transpose_apply]
 
 lemma IsOrthochronous_iff_fstCol_IsFourVelocity (Λ : lorentzGroup) :
     IsOrthochronous Λ ↔ IsFourVelocity (fstCol Λ) := by
   simp [IsOrthochronous, IsFourVelocity]
   rw [stdBasis_mulVec]
 
+/-- The continuous map taking a Lorentz transformation to its `0 0` element. -/
 def mapZeroZeroComp : C(lorentzGroup, ℝ) := ⟨fun Λ => Λ.1 0 0, by
   refine Continuous.matrix_elem ?_ 0 0
   refine Continuous.comp' Units.continuous_val continuous_subtype_val⟩
 
-
+/-- An auxillary function used in the definition of `orthchroMapReal`. -/
 def stepFunction : ℝ → ℝ := fun t =>
   if t ≤ -1 then -1 else
     if 1 ≤  t then 1 else t
@@ -78,6 +80,8 @@ lemma stepFunction_continuous : Continuous stepFunction := by
   rw [Set.Ici_def, @frontier_Ici, @Set.mem_singleton_iff] at ha
   simp [ha]
 
+/-- The continuous map from `lorentzGroup` to `ℝ` wh
+taking Orthochronous elements to `1` and non-orthochronous to `-1`. -/
 def orthchroMapReal : C(lorentzGroup, ℝ) := ContinuousMap.comp
   ⟨stepFunction, stepFunction_continuous⟩ mapZeroZeroComp
 
@@ -108,6 +112,7 @@ lemma orthchroMapReal_minus_one_or_one (Λ : lorentzGroup) :
 
 local notation  "ℤ₂" => Multiplicative (ZMod 2)
 
+/-- A continuous map from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/
 def orthchroMap : C(lorentzGroup, ℤ₂) :=
   ContinuousMap.comp coeForℤ₂ {
     toFun := fun Λ => ⟨orthchroMapReal Λ, orthchroMapReal_minus_one_or_one Λ⟩,
@@ -127,7 +132,7 @@ lemma zero_zero_mul (Λ Λ' : lorentzGroup) :
     ⟪(fstCol (transpose Λ)).1.space, (fstCol Λ').1.space⟫_ℝ := by
   rw [@Subgroup.coe_mul, @GeneralLinearGroup.coe_mul, mul_apply, Fin.sum_univ_four]
   rw [@PiLp.inner_apply, Fin.sum_univ_three]
-  simp [transpose, stdBasis_mulVec]
+  simp [transpose, stdBasis_mulVec, PreservesηLin.liftLor, PreservesηLin.liftGL]
   ring
 
 lemma mul_othchron_of_othchron_othchron {Λ Λ' : lorentzGroup} (h : IsOrthochronous Λ)
@@ -164,24 +169,25 @@ lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : lorentzGroup} (h : ¬
   rw [zero_zero_mul]
   exact euclid_norm_not_IsFourVelocity_IsFourVelocity h h'
 
+/-- The representation from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/
 def orthchroRep : lorentzGroup →* ℤ₂ where
   toFun := orthchroMap
   map_one' := by
     have h1 : IsOrthochronous 1 := by simp [IsOrthochronous]
     rw [orthchroMap_IsOrthochronous h1]
   map_mul' Λ Λ' := by
-    simp
+    simp only
     by_cases h : IsOrthochronous Λ
      <;> by_cases h' : IsOrthochronous Λ'
     rw [orthchroMap_IsOrthochronous h, orthchroMap_IsOrthochronous h',
       orthchroMap_IsOrthochronous (mul_othchron_of_othchron_othchron h h')]
-    simp
+    simp only [mul_one]
     rw [orthchroMap_IsOrthochronous h, orthchroMap_not_IsOrthochronous h',
       orthchroMap_not_IsOrthochronous (mul_not_othchron_of_othchron_not_othchron h h')]
-    simp
+    simp only [Nat.reduceAdd, one_mul]
     rw [orthchroMap_not_IsOrthochronous h, orthchroMap_IsOrthochronous h',
       orthchroMap_not_IsOrthochronous (mul_not_othchron_of_not_othchron_othchron h h')]
-    simp
+    simp only [Nat.reduceAdd, mul_one]
     rw [orthchroMap_not_IsOrthochronous h, orthchroMap_not_IsOrthochronous h',
       orthchroMap_IsOrthochronous (mul_othchron_of_not_othchron_not_othchron h h')]
     simp only [Nat.reduceAdd]