Aestrongly Measurable bilin Form Integrand Of Coeff

theorem aestronglyMeasurable_bilinFormIntegrandOfCoeff    {Ω : Set E} {u v : E → ℝ}    (A : EllipticCoeff d Ω)    (hu : MemW1pWitness 2 u Ω) (hv : MemW1pWitness 2 v Ω) :    AEStronglyMeasurable (bilinFormIntegrandOfCoeff A hu hv) (volume.restrict Ω) := by  have hF_aemeas :      AEMeasurable        (fun x => ∑ i : Fin d, (∑ j : Fin d, A.a x i j * hu.weakGrad x j) * hv.weakGrad x i)        (volume.restrict Ω) := by    have hsum :        AEMeasurable          (∑ i : Fin d, fun x => (∑ j : Fin d, A.a x i j * hu.weakGrad x j) * hv.weakGrad x i)          (volume.restrict Ω) := by      refine Finset.aemeasurable_sum (s := (Finset.univ : Finset (Fin d)))        (f := fun i x => (∑ j : Fin d, A.a x i j * hu.weakGrad x j) * hv.weakGrad x i) ?_      intro i _      have hrow :          AEMeasurable (fun x => ∑ j : Fin d, A.a x i j * hu.weakGrad x j)            (volume.restrict Ω) := by        have hrow_sum :            AEMeasurable (∑ j : Fin d, fun x => A.a x i j * hu.weakGrad x j)              (volume.restrict Ω) := by          refine Finset.aemeasurable_sum (s := (Finset.univ : Finset (Fin d)))            (f := fun j x => A.a x i j * hu.weakGrad x j) ?_          intro j _          exact (A.measurable_apply i j).aemeasurable.mul            (hu.weakGrad_component_memLp j).aemeasurable        convert hrow_sum using 1        ext x        simp      exact hrow.mul (hv.weakGrad_component_memLp i).aemeasurable    convert hsum using 1    ext x    simp  have hscalar : ∀ a b : ℝ, ⟪a, b⟫_ℝ = a * b := by    intro a b    simpa using (RCLike.inner_apply' a b)  refine hF_aemeas.aestronglyMeasurable.congr ?_  filter_upwards with x  simp [bilinFormIntegrandOfCoeff, PiLp.inner_apply, matMulE_apply, Matrix.mulVec,    dotProduct, hscalar]