Acceleration eq of equation Of Motion

lemma acceleration_eq_of_equationOfMotion (z : Time → EuclideanSpace ℝ (Fin 1))    (hEOM : S.EquationOfMotion z) (t : Time) :    ∂ₜ (∂ₜ z) t = (-(S.m⁻¹ * S.k)) • z t + (-(S.m⁻¹ * S.γ)) • ∂ₜ z t := by  have hm : S.m ≠ 0 := S.m_ne_zero  have hsum : S.m • ∂ₜ (∂ₜ z) t + (S.γ • ∂ₜ z t + S.k • z t) = 0 := by    rw [← add_assoc]; exact hEOM t  have hma : S.m • ∂ₜ (∂ₜ z) t = -(S.k • z t) - S.γ • ∂ₜ z t := by    rw [eq_neg_of_add_eq_zero_left hsum]; module  have hkey : ∂ₜ (∂ₜ z) t = S.m⁻¹ • (S.m • ∂ₜ (∂ₜ z) t) := by    rw [smul_smul, inv_mul_cancel₀ hm, one_smul]  rw [hkey, hma]  module