∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} [inst_1 : SemilatticeSup ι] [Nonempty ι] [Countable ι] {f : ι → α → β} {g : α → β}
  [MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) →
    MeasureTheory.StronglyMeasurable g →
      (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
        ∀ {ε : ℝ}, 0 < ε → ∃ t, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g Filter.atTop tᶜ