Dist Time Deriv commute dist Space Deriv

lemma distTimeDeriv_commute_distSpaceDeriv {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]    (i : Fin d) (f : (Time × Space d) →d[ℝ] M) :    distTimeDeriv (distSpaceDeriv i f) = distSpaceDeriv i (distTimeDeriv f) := by  ext κ  simp only [distTimeDeriv_apply, distSpaceDeriv_apply, fderivD_apply, neg_neg]  congr 1  ext x  change fderiv ℝ (fun x => fderiv ℝ κ x (1, 0)) x (0, basis i) =    fderiv ℝ (fun x => fderiv ℝ κ x (0, basis i)) x (1, 0)  have h1 := smooth κ 2  rw [fderiv_clm_apply, fderiv_clm_apply]  · simp only [fderiv_fun_const, Pi.zero_apply, ContinuousLinearMap.comp_zero, zero_add,      ContinuousLinearMap.flip_apply]    exact (h1.contDiffAt.isSymmSndFDerivAt (by simp)).eq (0, basis i) (1, 0)  all_goals fun_prop