Angular Momentum eq inertia Tensor mul Vec

theorem angularMomentum_eq_inertiaTensor_mulVec (R : RigidBody 3) (ω : Fin 3 → ℝ) :    R.angularMomentum ω = R.inertiaTensor *ᵥ ω := by  funext i  simp only [angularMomentum, mulVec, dotProduct, inertiaTensor]  have hsmul : ∀ j : Fin 3,      R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, (x k) ^ 2 - x i * x j,        ContDiff.contMDiff <| by fun_prop⟩ * ω j      = R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, (x k) ^ 2 - x i * x j,        ContDiff.contMDiff <| by fun_prop⟩) := by    intro j    rw [map_smul, smul_eq_mul, mul_comm]  rw [Finset.sum_congr rfl (fun j _ => hsmul j), ← map_sum]  congr 1  ext x  simp only [ContMDiffMap.coeFn_mk]  rw [cross_cross_self_apply, ← ContMDiffMap.coeFnAddMonoidHom_apply, map_sum,    Finset.sum_apply]  simp only [ContMDiffMap.coeFnAddMonoidHom_apply, ContMDiffMap.coe_smul, Pi.smul_apply,    ContMDiffMap.coeFn_mk, smul_eq_mul]  fin_cases i <;> simp [Fin.sum_univ_three] <;> ring