Dist Div of Function

lemma distDiv_ofFunction {d : ℕ} {f : Space d → EuclideanSpace ℝ (Fin d)}    {hf : IsDistBounded f} (η : 𝓢(Space d, ℝ)) :    (∇ᵈ ⬝ (distOfFunction f hf)) η =    - ∫ x : Space d, ⟪f x, ∇ η x⟫_ℝ := by  rw [distDiv_apply_eq_sum_fderivD]  conv_rhs =>    enter [1, 2, x]    rw [grad_eq_sum, inner_sum]  conv_lhs =>    enter [2, i]    rw [fderivD_apply, distOfFunction_apply]  /- The following lemma could probably be moved out of this result. -/  have integrable_lemma (i j : Fin d) :      Integrable (fun x =>        (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i))        ((fderivCLM ℝ (Space d) ℝ) η)) x • f x) j) volume := by    simp only [PiLp.smul_apply]    exact (hf.pi_comp j).integrable_space _  rw [MeasureTheory.integral_finsetSum]  · simp    congr    funext i    rw [MeasureTheory.eval_integral_piLp]    · congr      funext x      simp [inner_smul_right, EuclideanSpace.inner_single_right]      left      rw [deriv_eq_fderiv_basis]    · intro j      exact integrable_lemma i j  · intro i hi    simp only [inner_smul_right, EuclideanSpace.inner_single_right, conj_trivial, one_mul]    convert integrable_lemma i i using 2    rename_i x    simp only [evalCLM_apply_apply, fderivCLM_apply, PiLp.smul_apply, smul_eq_mul,      mul_eq_mul_right_iff]    left    rw [deriv_eq_fderiv_basis]