Equal up to const of deriv eq

lemma equal_up_to_const_of_deriv_eq {d} {M} [NormedAddCommGroup M] [NormedSpace ℝ M]    {f g : Time → Space d → M} (hf : Differentiable ℝ ↿f) (hg : Differentiable ℝ ↿g)    (h₁ : ∀ t x, ∂ₜ (f · x) t = ∂ₜ (g · x) t)    (h₂ : ∀ t x i, Space.deriv i (f t) x = Space.deriv i (g t) x) :    ∃ (c : M), ∀ t x, f t x = g t x + c := by  suffices h : ∃ c', ∀ t x, f t x - g t x = c' by    obtain ⟨c', hc'⟩ := h    use c'    intro t x    rw [← hc' t x]    simp  apply const_of_time_deriv_space_deriv_eq_zero  · exact Differentiable.fun_sub hf hg  · intro t x    rw [Time.deriv_eq, fderiv_fun_sub]    simp [← Time.deriv_eq, h₁]    all_goals fun_prop  · intro t x i    rw [Space.deriv_eq_fderiv_basis, fderiv_fun_sub]    simp [← Space.deriv_eq_fderiv_basis, h₂]    all_goals fun_prop