∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} {F : α → ENNReal},
  (∀ (n : ℕ), AEMeasurable (f n) μ) →
    (∀ᵐ (x : α) ∂μ, Antitone fun n => f n x) →
      ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤ →
        (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (F x))) →
          Filter.Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), F x ∂μ))