Space deriv differentiable time

@[fun_prop]lemma space_deriv_differentiable_time {d i} {M} [NormedAddCommGroup M] [NormedSpace ℝ M]    {f : Time → Space d → M} (hf : ContDiff ℝ 2 ↿f) (x : Space d) :    Differentiable ℝ (fun t => Space.deriv i (f t) x) := by  conv =>    enter [2, t];    rw [Space.deriv_eq_fderiv_basis]  apply Differentiable.clm_apply  · have hdd : Differentiable ℝ ↿f := hf.differentiable (by simp)    have h1 (t : Time) : fderiv ℝ (fun x => f t x) x      = fderiv ℝ (↿f) (t, x) ∘L (ContinuousLinearMap.inr ℝ Time (Space d)) := by      ext w      simp only [ContinuousLinearMap.coe_comp, Function.comp_apply, ContinuousLinearMap.inr_apply]      rw [← fderiv_space_eq_fderiv_curry f t x w hdd]    conv =>      enter [2, y]      change fderiv ℝ (fun x => f y x) x      rw [h1]    fun_prop  · fun_prop