Constant Time dist Time Deriv

@[simp]lemma constantTime_distTimeDeriv {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ}    (f : (Space d) →d[ℝ] M) :    Space.distTimeDeriv (constantTime f) = 0 := by  ext η  simp [Space.distTimeDeriv_apply, fderivD_apply, constantTime_apply]  suffices h : (timeIntegralSchwartz ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0))      ((fderivCLM ℝ (Time × Space d) ℝ) η))) = 0 by    rw [h]    simp  ext x  rw [timeIntegralSchwartz_apply]  calc _    _ = ∫ (t : Time), fderiv ℝ η (t, x) (1, 0) := by rfl    _ = ∫ (t : Time), fderiv ℝ (fun t => η (t, x)) t 1 := by      congr      funext t      change _ = (fderiv ℝ (η ∘ fun t => (t, x)) t) 1      rw [fderiv_comp, DifferentiableAt.fderiv_prodMk]      simp only [fderiv_fun_id, fderiv_fun_const, Pi.zero_apply,        ContinuousLinearMap.coe_comp, Function.comp_apply, ContinuousLinearMap.prod_apply,        ContinuousLinearMap.coe_id', id_eq, _root_.zero_apply]      · fun_prop      · fun_prop      · apply Differentiable.differentiableAt        exact η.smooth'.differentiable (by simp)      · fun_prop    _ = ∫ (t : Time), (fun t => 1) t * fderiv ℝ (fun t => η (t, x)) t 1 := by simp    _ = - ∫ (t : Time), fderiv ℝ (fun t => 1) t 1 * (fun t => η (t, x)) t := by      rw [integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable]      · simp      · conv_lhs =>          enter [t]          simp only [one_mul]          change (fderiv ℝ (η ∘ fun t => (t, x)) t) 1          rw [fderiv_comp _ (by            apply Differentiable.differentiableAt            exact η.smooth'.differentiable (by simp))            (by fun_prop), DifferentiableAt.fderiv_prodMk (by fun_prop) (by fun_prop)]          simp only [fderiv_fun_id, fderiv_fun_const, Pi.ofNat_apply,            ContinuousLinearMap.comp_apply, ContinuousLinearMap.prod_apply,            ContinuousLinearMap.id_apply, _root_.zero_apply]        exact integrable_time_integral (LineDeriv.lineDerivOpCLM ℝ _ ((1, 0) : Time × Space d) η) x      · simp        exact integrable_time_integral η x      · fun_prop      · fun_prop  simp