Kinetic Energy eq translational add body Angular Velocity

theorem kineticEnergy_eq_translational_add_bodyAngularVelocity (M : RigidBodyMotion 3) (t : Time)    (h : M.mass ≠ 0) (hR : DifferentiableAt ℝ (fun s => (M.orientation s).1) t)    (hc : M.centerOfMass = 0) :    M.kineticEnergy t      = (1 / (2 : ℝ)) * M.mass * (⟪M.centerOfMassVelocity t, M.centerOfMassVelocity t⟫_ℝ)        + M.toRigidBody.rotationalKineticEnergy (M.bodyAngularVelocity t) := by  rw [M.kineticEnergy_eq_translational_add_rotational t h,    RigidBody.rotationalKineticEnergy_eq_integral]  congr 1  congr 2  ext y  have hy : (fun j => (y : Fin 3 → ℝ) j - M.centerOfMass j) = (y : Fin 3 → ℝ) := by    simp [hc]  simp only [cmap_apply, ContMDiffMap.coeFn_mk]  rw [hy, M.deriv_orientation_mulVec_eq_orientation_bodyAngularVelocity_cross (y : Fin 3 → ℝ) t hR,    Matrix.dotProduct_mulVec_orthogonal (mul_eq_one_comm.mp (M.orientation_mul_transpose t))]