-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
        (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpi : IsPiSystem.{u_1} (α := Ω) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s}
empty :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ) (∫ (x : Ω) in ∅, g x ∂μ)
      (∫ (x : Ω) in ∅, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
basic :
  ∀ (s : Set Ω) (hs : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s} s),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
        (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
compl :
  ∀ (t : Set Ω) (htmeas : MeasurableSet t)
    (ht :
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : Ω) in t, g x ∂μ)
          (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) tᶜ : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ)
        (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
    (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
have iUnion : ∀ (f : ℕ → Set Ω) (hf : Pairwise (Function.onFun Disjoint f)) (hfmeas : ∀ (i : ℕ), MeasurableSet (f i))
  (heq :
    ∀ (i : ℕ),
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : Ω) in f i, g x ∂μ)
          (∫ (x : Ω) in f i, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ) (∫ (x : Ω) in ⋃ (i : ℕ), f i, g x ∂μ)
      (∫ (x : Ω) in ⋃ (i : ℕ), f i,
        limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
Tactic: induction s, hs
    using MeasurableSpace.induction_on_inter (MeasurableSpace.measurableSpace_iSup_eq ℱ) hpi with
  | empty =>
    simp only [Measure.restrict_empty, integral_zero_measure]
  | basic s hs =>
    rcases hs with ⟨n, hn⟩
    exact this n _ hn
  | compl t htmeas ht =>
    have hgeq := @setIntegral_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas (hg.trim hle hgmeas)
    have hheq := @setIntegral_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas
      (hlimint.trim hle stronglyMeasurable_limitProcess)
    rw [setIntegral_trim hle hgmeas htmeas.compl,
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas.compl, hgeq, hheq, ←
      setIntegral_trim hle hgmeas htmeas, ←
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas, ← integral_trim hle hgmeas, ←
      integral_trim hle stronglyMeasurable_limitProcess, ← setIntegral_univ,
      this 0 _ MeasurableSet.univ, setIntegral_univ, ht (measure_lt_top _ _)]
  | iUnion f hf hfmeas heq =>
    rw [integral_iUnion (fun n => hle _ (hfmeas n)) hf hg.integrableOn,
      integral_iUnion (fun n => hle _ (hfmeas n)) hf hlimint.integrableOn]
    exact tsum_congr fun n => heq _ (measure_lt_top _ _)
Cleared hypotheses: hs, h