-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_2
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 (β := ℝ≥0∞) 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 : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
let let₁ let₂ : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
let₃ :
  let F' : α → ℝ≥0∞ := fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞;
  ∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))),
    ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
let₄ :
  let F' : α → ℝ≥0∞ := fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞;
  ∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))), F' =ᶠ[ae μ] F
let₅ :
  let F' : α → ℝ≥0∞ := fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞;
  ∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))) (hF'_le : F' ≤ᶠ[ae μ] F),
    F' =ᶠ[ae μ] F
let₆ :
  let F' : α → ℝ≥0∞ := fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞;
  ∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))) (hF'_le : F' ≤ᶠ[ae μ] F),
    ∫⁻ (a : α), F' a ∂μ = ∫⁻ (a : α), F a ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have let₇ : let F' : α → ℝ≥0∞ := fun (a : α) ↦
  if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
    h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
  else ∞;
∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))) (hF'_le : F' ≤ᶠ[ae μ] F),
  Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
Tactic: classical
  let F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
    then h.choose else ∞
  have hF'_tendsto : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) := by
    filter_upwards [h_exists] with a ha
    simp_rw [F', dif_pos ha]
    exact ha.choose_spec
  suffices F' =ᵐ[μ] F by
    filter_upwards [this, hF'_tendsto] with a h_eq h_tendsto using h_eq ▸ h_tendsto
  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 _)
  suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ from
    ae_eq_of_ae_le_of_lintegral_le hF'_le (this ▸ h_int_finite) hF_meas this.symm.le
  refine tendsto_nhds_unique ?_ hf_tendsto
  exact lintegral_tendsto_of_tendsto_of_monotone hf_meas hf_mono hF'_tendsto