Space fun of time deriv eq zero

lemma space_fun_of_time_deriv_eq_zero {d} {M} [NormedAddCommGroup M] [NormedSpace ℝ M]    {f : Time → Space d → M} (hf : Differentiable ℝ ↿f)    (h : ∀ t x, ∂ₜ (f · x) t = 0) :    ∃ (g : Space d → M), ∀ t x, f t x = g x := by  use fun x => f 0 x  intro t x  apply is_const_of_fderiv_eq_zero (f := fun t' => f t' x) (𝕜 := ℝ)  · fun_prop  intro t  ext r  simp only [_root_.zero_apply]  trans r.val • (fderiv ℝ (fun t' => f t' x) t) 1  · rw [← map_smul]    congr    ext    simp  rw [← Time.deriv_eq, h t x, smul_zero]