-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
/-- If a monotone sequence of functions has an upper bound and the sequence of integrals of these
functions tends to the integral of the upper bound, then the sequence of functions converges
almost everywhere to the upper bound. Auxiliary version assuming moreover that the
functions in the sequence are ae measurable. -/
lemma tendsto_of_lintegral_tendsto_of_monotone_aux {α : Type*} {mα : MeasurableSpace α}
    {f : ℕ → α → ℝ≥0∞} {F : α → ℝ≥0∞} {μ : Measure α}
    (hf_meas : ∀ n, AEMeasurable (f n) μ) (hF_meas : AEMeasurable F μ)
    (hf_tendsto : Tendsto (fun i ↦ ∫⁻ a, f i a ∂μ) atTop (𝓝 (∫⁻ a, F a ∂μ)))
    (hf_mono : ∀ᵐ a ∂μ, Monotone (fun i ↦ f i a))
    (h_bound : ∀ᵐ a ∂μ, ∀ i, f i a ≤ F a) (h_int_finite : ∫⁻ a, F a ∂μ ≠ ∞) :
    ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Proof state:
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ⊤
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a => if h : ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l) then h.choose else ⊤
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F' a))
⊢ F' =ᶠ[ae μ] F

Tactic:
have hF'_le : F' ≤ᵐ[μ] F := by
  filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto
  exact le_of_tendsto' h_tendsto (fun m ↦ h_le _)

Result:
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ⊤
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a => if h : ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l) then h.choose else ⊤
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F' a))
hF'_le : F' ≤ᶠ[ae μ] F
⊢ F' =ᶠ[ae μ] F

Proof state:
case h.inl
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ⊤
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ⊤
h_mono : Monotone fun i => f i a
h_absurd : ∀ (b : ℝ≥0∞), ∃ a_1, b ≤ f a_1 a
⊢ ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l)

Tactic:
obtain ⟨i, hi⟩ := h_absurd (F a + 1)

Result:
case h.inl.intro
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ⊤
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ⊤
h_mono : Monotone fun i => f i a
h_absurd : ∀ (b : ℝ≥0∞), ∃ a_1, b ≤ f a_1 a
i : ℕ
hi : F a + 1 ≤ f i a
⊢ ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l)