∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [BorelSpace β] {ι : Type u_3} [Countable ι]
  [Nonempty ι] {μ : MeasureTheory.Measure α} {f : ι → α → β} {L : Filter ι} [L.IsCountablyGenerated],
  (∀ (n : ι), AEMeasurable (f n) μ) →
    (∀ᵐ (x : α) ∂μ, ∃ l, Filter.Tendsto (fun n => f n x) L (nhds l)) →
      ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) L (nhds (f_lim x))