-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
ℱ₁ ℱ₂ ℱ₃ ℱ₄ : ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
ℱ₅ :
  ∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0),
    ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
ℱ₆ :
  let g' : Ω → ℝ := fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0;
  ∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0)
    (hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))),
    ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
ℱ₇ :
  let g' : Ω → ℝ := fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0;
  ∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0)
    (hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω)))
    (hg'm : AEStronglyMeasurable g' (μ.trim hle)),
    ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
ℱ₈ :
  let g' : Ω → ℝ := fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0;
  ∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0)
    (hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))) (g : Ω → ℝ)
    (hgm : StronglyMeasurable g) (hae : g' =ᶠ[ae (μ.trim hle)] g),
    ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))
have ℱ₉ : let g' : Ω → ℝ := fun (ω : Ω) ↦
  if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
    h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
  else 0;
∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0)
  (hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))) (g : Ω → ℝ)
  (hgm : StronglyMeasurable g) (hae : g' =ᶠ[ae (μ.trim hle)] g)
  (hg : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))),
  ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
Tactic: classical
  suffices
      ∃ g, StronglyMeasurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) by
    rw [limitProcess, dif_pos this]
    exact (Classical.choose_spec this).2
  set g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then h.choose else 0
  have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _
  have hg' : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω)) := by
    filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
    simp_rw [g', dif_pos hω]
    exact hω.choose_spec
  have hg'm : AEStronglyMeasurable[⨆ n, ℱ n] g' (μ.trim hle) :=
    (@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, ℱ n) _ _ _ _ _ _ _
      (fun n => ((hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : ℱ n ≤ ⨆ n, ℱ n)
        le_rfl).aemeasurable) hg').aestronglyMeasurable
  obtain ⟨g, hgm, hae⟩ := hg'm
  have hg : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) := by
    filter_upwards [hae, hg'] with ω hω hg'ω
    exact hω ▸ hg'ω
  exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩