Angular Velocity Tensor transpose

lemma angularVelocityTensor_transpose (M : RigidBodyMotion d) (t : Time)    (hR : DifferentiableAt ℝ (fun s => (M.orientation s).1) t) :    (M.angularVelocityTensor t)ᵀ = - M.angularVelocityTensor t := by  have hconst : (fun s => (M.orientation s).1 * ((M.orientation s).1)ᵀ)      = fun _ => (1 : Matrix (Fin d) (Fin d) ℝ) := by    funext s    exact M.orientation_mul_transpose s  have hderiv0 : ∂ₜ (fun s => (M.orientation s).1 * ((M.orientation s).1)ᵀ) t = 0 := by    rw [hconst]    exact Time.deriv_const 1  have hprod := Time.deriv_matrix_mul (fun s => (M.orientation s).1)    (fun s => ((M.orientation s).1)ᵀ) t hR hR.matrix_transpose  rw [Time.deriv_matrix_transpose (fun s => (M.orientation s).1) t hR, hderiv0] at hprod  rw [angularVelocityTensor, transpose_mul, transpose_transpose]  exact eq_neg_of_add_eq_zero_left hprod.symm