Dist Deriv constant Slice Dist same

lemma distDeriv_constantSliceDist_same {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M]    {d : ℕ} (i : Fin d.succ) (f : (Space d) →d[ℝ] M) :    distDeriv i (constantSliceDist i f) = 0 := by  ext η  simp [constantSliceDist_apply, Space.distDeriv_apply, Distribution.fderivD_apply]  trans f 0; swap  · simp  congr  ext x  simp [sliceSchwartz_apply]  calc _    _ = ∫ r, fderiv ℝ η ((slice i).symm (r, x)) (basis i) := by rfl    _ = ∫ r, fderiv ℝ (fun r => η ((slice i).symm (r, x))) r 1 := by        congr        funext r        rw [basis_self_eq_slice, fderiv_fun_slice_symm_left_apply]        exact η.differentiableAt    _ = ∫ (r : ℝ), (fun r => 1) r * fderiv ℝ (fun r => η ((slice i).symm (r, x))) r 1 := by simp    _ = - ∫ (r : ℝ), fderiv ℝ (fun t => 1) r 1 * (fun r => η ((slice i).symm (r, x))) r := by      rw [integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable]      · simp      · simp        change Integrable (fun r => fderiv ℝ (fun r => η ((slice i).symm (r, x))) r 1) volume        fun_prop      · simp        exact schwartzMap_integrable_slice_symm i η x      · fun_prop      · fun_prop  simp