To Initial Conditions from Initial Conditions

lemma toInitialConditions_fromInitialConditions (S : HarmonicOscillator)    (IC : InitialConditions) :    (fromInitialConditions S IC).toInitialConditions S = IC := by  have hω : S.ω ≠ 0 := S.ω_ne_zero  set z : ℂ := (⟨IC.x₀ 0, IC.v₀ 0 / S.ω⟩ : ℂ)  -- polar identities  have hcos : ‖z‖ * cos (Complex.arg z) = z.re := Complex.norm_mul_cos_arg z  have hsin : ‖z‖ * sin (Complex.arg z) = z.im := Complex.norm_mul_sin_arg z  -- By construction the parts of `z` are exactly the original data.  have hre : z.re = IC.x₀ 0 := rfl  have him : z.im = IC.v₀ 0 / S.ω := rfl  apply InitialConditions.ext  · -- Position: `‖z‖ cos (arg z) = Re z = IC.x₀ 0`, and `single 0 (IC.x₀ 0) = IC.x₀`.    show EuclideanSpace.single 0 (‖z‖ * cos (Complex.arg z)) = IC.x₀    rw [hcos, hre]    ext i; fin_cases i; simp  · -- Velocity: `‖z‖ ω sin (arg z) = ω · Im z = ω · (v₀ / ω) = IC.v₀ 0`, then reassemble.    show EuclideanSpace.single 0 (‖z‖ * S.ω * sin (Complex.arg z)) = IC.v₀    have hv : ‖z‖ * S.ω * sin (Complex.arg z) = IC.v₀ 0 := by      rw [mul_right_comm, hsin, him]; field_simp    rw [hv]    ext i; fin_cases i; simp