∀ {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace α] [BorelSpace α] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] {g : α → E}
  {l : Filter ι} {x₀ : α} {s t : Set α} {φ : ι → α → ℝ} {a : E},
  MeasurableSet s →
    t ∈ nhdsWithin x₀ s →
      (∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)) →
        Filter.Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (nhds 1) →
          (∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) →
            MeasureTheory.IntegrableOn g s μ →
              Filter.Tendsto g (nhdsWithin x₀ s) (nhds a) →
                ∀ᶠ (i : ι) in l, MeasureTheory.IntegrableOn (fun x => φ i x • g x) s μ