refactor: Improve todos and remove ambiguous

HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean

@@ -388,7 +388,11 @@ lemma pauliMatrix_contr_lower_3_1_1 :
   · congr 2
     decide
 
-TODO "Work out why `pauliCo_prod_basis_expand'` is needed."
+TODO "Work out why `pauliCo_prod_basis_expand'` is needed, since it is exactly the same
+  as `pauliCo_prod_basis_expand` which is defined in another file. One will see that
+  replacing instances of `pauliCo_prod_basis_expand'` with `pauliCo_prod_basis_expand`
+  does not work."
+
 /-- This lemma is exactly the same as `pauliCo_prod_basis_expand`.
   It is needed here for `pauliMatrix_contract_pauliMatrix_aux`. It is unclear why
   `pauliMatrix_lower_basis_expand_prod` does not work. -/

HepLean/Lorentz/ComplexVector/Basic.lean

@@ -129,7 +129,6 @@ lemma inclCongrRealLorentz_ρ (M : SL(2, ℂ)) (v : ContrMod 3) :
   rw [LorentzGroup.toComplex_mulVec_ofReal]
   rfl
 
-TODO "Rename."
 lemma SL2CRep_ρ_basis (M : SL(2, ℂ)) (i : Fin 1 ⊕ Fin 3) :
     (complexContr.ρ M) (complexContrBasis i) =
     ∑ j, (SL2C.toLorentzGroup M).1 j i •
@@ -141,6 +140,5 @@ lemma SL2CRep_ρ_basis (M : SL(2, ℂ)) (i : Fin 1 ⊕ Fin 3) :
   simp only [LinearMap.map_smulₛₗ, ofRealHom_eq_coe, coe_smul]
   rw [complexContrBasis_of_real]
 
-TODO "Include relation to real Lorentz vectors."
 end Lorentz
 end

HepLean/Lorentz/Group/Basic.lean

@@ -15,7 +15,7 @@ We define the Lorentz group.
 - http://home.ku.edu.tr/~amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf
 
 -/
-TODO "Show that the Lorentz group is a Lie group."
+TODO "Define the Lie group structure on the Lorentz group."
 
 noncomputable section
 

HepLean/Lorentz/Group/Boosts.lean

@@ -21,7 +21,6 @@ A boost is the special case of a generalised boost when `u = stdBasis 0`.
   https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf
 
 -/
-TODO "Show that generalised boosts are in the restricted Lorentz group."
 noncomputable section
 
 namespace LorentzGroup
@@ -204,10 +203,14 @@ lemma toMatrix_in_lorentzGroup (u v : FuturePointing d) : (toMatrix u v) ∈ Lor
   refine hn _ ?_ h1
   simpa using (FuturePointing.one_add_metric_non_zero u v)
 
+TODO "Make `toLorentz` the definition of a generalised boost. This will involve
+  refactoring this file."
 /-- A generalised boost as an element of the Lorentz Group. -/
 def toLorentz (u v : FuturePointing d) : LorentzGroup d :=
   ⟨toMatrix u v, toMatrix_in_lorentzGroup u v⟩
 
+TODO "Show that generalised boosts are in the restricted Lorentz group."
+
 lemma toLorentz_continuous (u : FuturePointing d) : Continuous (toLorentz u) := by
   refine Continuous.subtype_mk ?_ (fun x => toMatrix_in_lorentzGroup u x)
   exact toMatrix_continuous u

HepLean/Lorentz/Group/Restricted.lean

@@ -11,8 +11,10 @@ This file is currently a stub.
 
 -/
 TODO "Add definition of the restricted Lorentz group."
-TODO "Prove member of the restricted Lorentz group is combo of boost and rotation."
-TODO "Prove restricted Lorentz group equivalent to connected component of identity."
+TODO "Prove that every member of the restricted Lorentz group is
+  combiniation of a boost and a rotation."
+TODO "Prove restricted Lorentz group equivalent to connected component of identity
+  of the Lorentz group."
 
 noncomputable section