Aestrongly Measurable divergence RHSIntegrand Of Field

theorem aestronglyMeasurable_divergenceRHSIntegrandOfField    {Ω : Set E} {F : E → E} (hF : MemLp F 2 (volume.restrict Ω))    {v : E → ℝ} (hv : MemW1pWitness 2 v Ω) :    AEStronglyMeasurable (divergenceRHSIntegrandOfField F hv) (volume.restrict Ω) := by  have hF_ofLp_cont : Continuous (fun y : E => (WithLp.ofLp y : Fin d → ℝ)) := by    simpa using (PiLp.continuous_ofLp 2 (fun _ : Fin d => ℝ))  have hF_ofLp :      AEStronglyMeasurable (fun x => (WithLp.ofLp (F x) : Fin d → ℝ)) (volume.restrict Ω) :=    hF_ofLp_cont.comp_aestronglyMeasurable hF.aestronglyMeasurable  have hsum :      AEMeasurable        (∑ i : Fin d, fun x => F x i * hv.weakGrad x i)        (volume.restrict Ω) := by    refine Finset.aemeasurable_sum (s := (Finset.univ : Finset (Fin d)))      (f := fun i x => F x i * hv.weakGrad x i) ?_    intro i _hi    have hFi : AEMeasurable (fun x => F x i) (volume.restrict Ω) := by      simpa using        (Continuous.comp_aestronglyMeasurable (continuous_apply i) hF_ofLp).aemeasurable    exact hFi.mul (hv.weakGrad_component_memLp i).aemeasurable  have hscalar : ∀ a b : ℝ, ⟪a, b⟫_ℝ = a * b := by    intro a b    simpa using (RCLike.inner_apply' a b)  refine hsum.aestronglyMeasurable.congr ?_  filter_upwards with x  simp [divergenceRHSIntegrandOfField, PiLp.inner_apply, hscalar]