Exp is Orthochronous

theorem exp_isOrthochronous (A : lorentzAlgebra) :    LorentzGroup.IsOrthochronous ⟨NormedSpace.exp A.1, exp_mem_lorentzGroup A⟩ := by  -- The Lie algebra is a vector space, so there is a path from 0 to A.  let γ : Path (0 : lorentzAlgebra) A :=  { toFun := fun t => t.val • A,    continuous_toFun := by      exact Continuous.smul continuous_subtype_val continuous_const,    source' := by simp [zero_smul],    target' := by simp [one_smul] }  let exp_γ : Path (1 : LorentzGroup 3) ⟨NormedSpace.exp A.1, exp_mem_lorentzGroup A⟩ :=  { toFun := fun t => ⟨NormedSpace.exp (γ t).val, exp_mem_lorentzGroup (γ t)⟩,    continuous_toFun := by      apply Continuous.subtype_mk      apply Continuous.comp      · apply NormedSpace.exp_continuous      · exact Continuous.comp continuous_subtype_val (γ.continuous_toFun),    source' := by      ext i j      simp only [γ]      simp [NormedSpace.exp_zero],    target' := by      ext i j      simp only [γ]      simp}  have h_joined : Joined (1 : LorentzGroup 3) ⟨NormedSpace.exp A.1, exp_mem_lorentzGroup A⟩ :=    ⟨exp_γ⟩  have h_connected : ⟨NormedSpace.exp A.1, exp_mem_lorentzGroup A⟩ ∈ connectedComponent      (1 : LorentzGroup 3) :=    pathComponent_subset_component _ h_joined  rw [← LorentzGroup.isOrthochronous_on_connected_component h_connected]  exact LorentzGroup.id_isOrthochronous