Kinetic Energy integrand split

lemma kineticEnergy_integrand_split {d : ℕ} (M : RigidBodyMotion d) (t : Time) :    cmap (fun y => (⟪M.velocityClosedForm t y, M.velocityClosedForm t y⟫_ℝ))        (M.contDiff_velocityClosedForm_inner t)      = cmap (fun y =>            (∂ₜ (fun s => (M.orientation s).1) t *ᵥ fun j => y j - M.centerOfMass j) ⬝ᵥ            (∂ₜ (fun s => (M.orientation s).1) t *ᵥ fun j => y j - M.centerOfMass j))          (by simp only [dotProduct, Matrix.mulVec]; fun_prop)        + ∑ j, (2 * (((M.centerOfMassVelocity t : Fin d → ℝ) ᵥ*              ∂ₜ (fun s => (M.orientation s).1) t) j)) •            cmap (fun y => y j - M.centerOfMass j) (by fun_prop)        + (⟪M.centerOfMassVelocity t, M.centerOfMassVelocity t⟫_ℝ) •            (1 : C^⊤⟮𝓘(ℝ, Space d), Space d; 𝓘(ℝ, ℝ), ℝ⟯) := by  ext y  simp only [cmap_apply, ContMDiffMap.coe_add, ContMDiffMap.coe_smul, ContMDiffMap.coe_one,    Pi.add_apply, Pi.smul_apply, Pi.one_apply, smul_eq_mul, mul_one]  rw [← ContMDiffMap.coeFnAddMonoidHom_apply, map_sum, Finset.sum_apply]  simp only [ContMDiffMap.coeFnAddMonoidHom_apply, ContMDiffMap.coe_smul, Pi.smul_apply,    cmap_apply, smul_eq_mul]  rw [show (⟪M.velocityClosedForm t y, M.velocityClosedForm t y⟫_ℝ)        = (M.velocityClosedForm t y : Fin d → ℝ) ⬝ᵥ (M.velocityClosedForm t y : Fin d → ℝ) from      Space.inner_eq_sum _ _,    velocityClosedForm_val,    show (⟪M.centerOfMassVelocity t, M.centerOfMassVelocity t⟫_ℝ)        = (M.centerOfMassVelocity t : Fin d → ℝ) ⬝ᵥ (M.centerOfMassVelocity t : Fin d → ℝ) from      Space.inner_eq_sum _ _,    add_dotProduct, dotProduct_add, dotProduct_add,    dotProduct_comm (∂ₜ (fun s => (M.orientation s).1) t *ᵥ fun j => y j - M.centerOfMass j)      (M.centerOfMassVelocity t : Fin d → ℝ),    dotProduct_mulVec (M.centerOfMassVelocity t : Fin d → ℝ)      (∂ₜ (fun s => (M.orientation s).1) t) (fun j => y j - M.centerOfMass j)]  simp only [dotProduct, two_mul, add_mul, Finset.sum_add_distrib]  ring