Trajectory velocity eq zero iff norm eq amplitude

lemma trajectory_velocity_eq_zero_iff_norm_eq_amplitude (IC : InitialConditions)    (t : Time) :    ∂ₜ (IC.trajectory S) t = 0 ↔      ‖IC.trajectory S t‖ = (AmplitudePhase.fromInitialConditions S IC).A := by  by_cases hA : (AmplitudePhase.fromInitialConditions S IC).A = 0  · rw [trajectory_velocity_eq_sin, trajectory_eq_cos]    simp [hA]  rw [trajectory_velocity_eq_zero_iff_sin_eq_zero S IC hA t, trajectory_eq_cos]  set A := (AmplitudePhase.fromInitialConditions S IC).A  set θ := S.ω * t.val - (AmplitudePhase.fromInitialConditions S IC).φ  show sin θ = 0 ↔ ‖EuclideanSpace.single 0 (A * cos θ)‖ = A  have hA' : A ≠ 0 := by simpa [A] using hA  have hA_nonneg : 0 ≤ A := norm_nonneg (⟨IC.x₀ 0, IC.v₀ 0 / S.ω⟩ : ℂ)  have hA_pos : 0 < A := lt_of_le_of_ne hA_nonneg (Ne.symm hA')  constructor  · intro hsin    rcases Real.sin_eq_zero_iff_cos_eq.mp hsin with hcos | hcos <;>      simp [hcos, abs_of_pos hA_pos]  · intro hnorm    have hnorm' : |A * cos θ| = A := by      simpa using hnorm    have hcos_abs : |cos θ| = 1 := by      rw [abs_mul, abs_of_pos hA_pos] at hnorm'      exact mul_left_cancel₀ hA' (hnorm'.trans (mul_one A).symm)    obtain ⟨n, hn⟩ := Real.abs_cos_eq_one_iff.mp hcos_abs    exact Real.sin_eq_zero_iff.mpr ⟨n, hn⟩