Fderiv cross commute

lemma fderiv_cross_commute {t : Time} {s : EuclideanSpace ℝ (Fin 3)}    {f : Time → EuclideanSpace ℝ (Fin 3)} (hf : Differentiable ℝ f) :    s ⨯ₑ₃ (fderiv ℝ (fun t' => f t') t) 1    = fderiv ℝ (fun t' => s ⨯ₑ₃ (f t')) t 1 := by  have h (i j : Fin 3) : s i * (fderiv ℝ (fun u => f u) t) 1 j -      s j * (fderiv ℝ (fun u => f u) t) 1 i      = (fderiv ℝ (fun t => s i * f t j - s j * f t i) t) 1:= by    rw [fderiv_fun_sub, fderiv_const_mul, fderiv_const_mul]    · simp only [FunLike.coe_sub, FunLike.coe_smul, Pi.sub_apply,        Pi.smul_apply, smul_eq_mul]      rw [Time.fderiv_euclid, Time.fderiv_euclid]      · intro i        repeat fun_prop      · fun_prop    · fun_prop    · fun_prop    · fun_prop    · fun_prop  rw [crossProduct]  ext i  fin_cases i <;>  · simp [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, WithLp.equiv_apply,      LinearMap.mk₂_apply, Fin.reduceFinMk, WithLp.equiv_symm_apply,      PiLp.toLp_apply, cons_val]    rw [h]    simp only [Fin.isValue]    rw [← Time.fderiv_euclid]    simp [Fin.isValue, cons_val_zero]    apply Time.differentiable_euclid    intro i    fin_cases i    · simp [Fin.zero_eta, Fin.isValue]      fun_prop    · simp [Fin.isValue]      fun_prop    · simp [Fin.isValue]      fun_prop