Fderiv time commute fderiv space

lemma fderiv_time_commute_fderiv_space {M} [NormedAddCommGroup M] [NormedSpace ℝ M]    (f : Time → Space d → M) (t dt : Time) (x dx : Space d)    (hf : ContDiff ℝ 2 ↿f) :    fderiv ℝ (fun t' => fderiv ℝ (fun x' => f t' x') x dx) t dt    = fderiv ℝ (fun x' => fderiv ℝ (fun t' => f t' x') t dt) x dx := by  trans fderiv ℝ (fun t' => (fderiv ℝ (↿f) (t', x) (0, dx))) t dt  · congr    funext t'    exact fderiv_space_eq_fderiv_curry f t' x dx (hf.differentiable (by simp))  trans fderiv ℝ (fun x => (fderiv ℝ (↿f) x (0, dx))) (t, x) (dt, 0)  · exact fderiv_time_eq_fderiv_curry (fun t x => fderiv ℝ ↿f (t, x) (0, dx)) t dt x (by fun_prop)  symm  trans fderiv ℝ (fun x' => (fderiv ℝ (↿f) (t, x') (dt, 0))) x dx  · congr    funext x'    exact fderiv_time_eq_fderiv_curry f t dt x' (hf.differentiable (by simp))  trans fderiv ℝ (fun t => (fderiv ℝ (↿f) t (dt, 0))) (t, x) (0, dx)  · exact fderiv_space_eq_fderiv_curry (fun t x => fderiv ℝ ↿f (t, x) (dt, 0)) t x dx (by fun_prop)  rw [fderiv_clm_apply, fderiv_clm_apply]  · simp only [fderiv_fun_const, Pi.zero_apply, ContinuousLinearMap.comp_zero, zero_add,      ContinuousLinearMap.flip_apply]    exact (hf.contDiffAt.isSymmSndFDerivAt (by simp)).eq (0, dx) (dt, 0)  all_goals fun_prop