To Undamped equation Of Motion

lemma toUndamped_equationOfMotion (S : DampedHarmonicOscillator) (hS : S.IsUndamped)    (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) :    S.EquationOfMotion xₜ ↔ (S.toUndamped hS).EquationOfMotion xₜ := by  have hγ : S.γ = 0 := by simpa [IsUndamped] using hS  rw [S.equationOfMotion_iff_newtons_2nd_law xₜ,    (S.toUndamped hS).equationOfMotion_iff_newtons_2nd_law xₜ hx]  refine forall_congr' fun t => ?_  rw [show (S.toUndamped hS).m = S.m from rfl,    show HarmonicOscillator.force (S.toUndamped hS) (xₜ t) = force S xₜ t from by      simp [force, HarmonicOscillator.force_eq_linear, toUndamped, hγ]]