Constant Time dist Space Deriv

lemma constantTime_distSpaceDeriv {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M]    (i : Fin d) (f : (Space d) →d[ℝ] M) :    Space.distSpaceDeriv i (constantTime f) = constantTime (Space.distDeriv i f) := by  ext η  simp [constantTime_apply]  rw [Space.distDeriv_apply, Space.distSpaceDeriv_apply]  rw [fderivD_apply, fderivD_apply, constantTime_apply]  congr 2  ext x  simp [timeIntegralSchwartz_apply]  symm  change fderiv ℝ (timeIntegralSchwartz η) x (basis i) = _  calc _      _ = fderiv ℝ (fun x => ∫ t, η (t, x) ∂volume) x (basis i) := by rfl      _ = (∫ t, fderiv ℝ (fun x => η (t, x)) x) (basis i) := by        rw [(time_integral_hasFDerivAt η x).fderiv]      _ = (∫ t, fderiv ℝ (fun x => η (t, x)) x (basis i)) := by        rw [ContinuousLinearMap.integral_apply]        exact integrable_fderiv_space η x  congr  funext t  change (fderiv ℝ (η ∘ fun x => (t, x)) x) (basis i) = _  rw [fderiv_comp, DifferentiableAt.fderiv_prodMk]  simp only [fderiv_fun_const, Pi.zero_apply, fderiv_fun_id, ContinuousLinearMap.coe_comp,    Function.comp_apply, ContinuousLinearMap.prod_apply, _root_.zero_apply,    ContinuousLinearMap.coe_id', id_eq]  · fun_prop  · fun_prop  · apply Differentiable.differentiableAt    exact η.smooth'.differentiable (by simp)  · fun_prop