Return time

lemma return_time (IC : InitialConditions) (non_trivial : IC.x₀ ≠ 0 ∨ IC.v₀ ≠ 0)    (t : Time) (ht : IC.trajectory S t = IC.x₀ ∧ ∂ₜ (IC.trajectory S) t = IC.v₀) :    ∃ n : ℤ,  (n : ℝ) * (T S) = t := by  have htx := ht.left  have htv := ht.right  rw [InitialConditions.trajectory_eq] at htx  rw [InitialConditions.trajectory_velocity] at htv  simp at htx  simp at htv  set c := cos (S.ω * t)  set s :=  sin (S.ω * t)  set xx := inner ℝ IC.x₀ IC.x₀  set vv := inner ℝ IC.v₀ IC.v₀  set xv := inner ℝ IC.x₀ IC.v₀  set det := vv + xx *  S.ω^2  have hxx0 : 0 ≤ xx := real_inner_self_nonneg  have hvv0 : 0 ≤ vv := real_inner_self_nonneg  have hω2 : 0 < S.ω ^ 2 := pow_pos S.ω_pos 2  have zero_lt_det : 0 < det := by    show 0 < vv + xx * S.ω ^ 2    rcases non_trivial with hx | hv    · nlinarith [real_inner_self_pos.mpr hx]    · nlinarith [real_inner_self_pos.mpr hv]  have det_ne_zero : det ≠ 0 := zero_lt_det.ne'  have hxx : c * xx + (s / S.ω) * xv = xx := by    have h := congrArg (inner ℝ IC.x₀) htx    simpa only [inner_add_right, real_inner_smul_right] using h  have hvv : - S.ω * s * xv + c * vv = vv := by    have h := congrArg (fun w => inner ℝ w IC.v₀) htv    simpa only [inner_add_left, inner_neg_left, real_inner_smul_left, neg_mul, mul_assoc] using h  have hcos : 1 = cos (S.ω * t) := by    calc    1 =  det / det := by simp only [ne_eq, det_ne_zero, not_false_eq_true, div_self]    _ = (vv + xx * S.ω^2 ) / det := by rfl    _ = c * ((vv + xx * S.ω^2) / det) + s * xv *S.ω* (S.ω/S.ω-1 ) / det := by      nth_rewrite 1 [← hvv, ← hxx]      ring_nf    _ = c * ((vv + xx * S.ω^2) / det ) := by      simp only [ne_eq, S.ω_ne_zero, not_false_eq_true,        div_self, sub_self, mul_zero, zero_div, add_zero]    _ = c * (det / det) := by rfl    _ = c := by simp only [ne_eq, det_ne_zero, not_false_eq_true, div_self, mul_one]    _ = _ := by rfl  obtain ⟨n, hn⟩ := (Real.cos_eq_one_iff (S.ω * t)).mp hcos.symm  refine ⟨n, ?_⟩  rw [period_eq]  field_simp [S.ω_ne_zero]  linear_combination hn