-- Module: Mathlib.Probability.Martingale.Convergence
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 Ω
hpi : IsPiSystem.{u_1} (α := Ω) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s}
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 ∂μ)
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) tᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
hgeq :
  ∫ (x : Ω) in tᶜ, g x ∂μ.trim hle = HSub.hSub (α := ℝ) (∫ (x : Ω), g x ∂μ.trim hle) (∫ (x : Ω) in t, g x ∂μ.trim hle)
hheq :
  ∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ.trim hle =
    HSub.hSub (α := ℝ) (∫ (x : Ω), limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ.trim hle)
      (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ.trim hle)
compl :
  Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ.trim hle)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
compl₁ :
  Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ.trim hle)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ.trim hle)
compl₂ :
  HSub.hSub (α := ℝ) (∫ (x : Ω), g x ∂μ.trim hle) (∫ (x : Ω) in t, g x ∂μ.trim hle) =
    ∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ.trim hle
compl₃ :
  HSub.hSub (α := ℝ) (∫ (x : Ω), g x ∂μ.trim hle) (∫ (x : Ω) in t, g x ∂μ.trim hle) =
    HSub.hSub (α := ℝ) (∫ (x : Ω), limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ.trim hle)
      (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ.trim hle)
compl₄ :
  HSub.hSub (α := ℝ) (∫ (x : Ω), g x ∂μ.trim hle) (∫ (x : Ω) in t, g x ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : Ω), limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ.trim hle)
      (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ.trim hle)
compl₅ :
  HSub.hSub (α := ℝ) (∫ (x : Ω), g x ∂μ.trim hle) (∫ (x : Ω) in t, g x ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : Ω), limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ.trim hle)
      (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
compl₆ :
  HSub.hSub (α := ℝ) (∫ (x : Ω), g x ∂μ) (∫ (x : Ω) in t, g x ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : Ω), limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ.trim hle)
      (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
compl₇ :
  HSub.hSub (α := ℝ) (∫ (x : Ω), g x ∂μ) (∫ (x : Ω) in t, g x ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : Ω), limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
      (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
compl₈ :
  HSub.hSub (α := ℝ) (∫ (x : Ω) in Set.univ, g x ∂μ) (∫ (x : Ω) in t, g x ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : Ω), limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
      (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
compl₉ :
  HSub.hSub (α := ℝ)
      (∫ (x : Ω) in Set.univ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
      (∫ (x : Ω) in t, g x ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : Ω), limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
      (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
compl₁₀ :
  HSub.hSub (α := ℝ) (∫ (x : Ω), limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
      (∫ (x : Ω) in t, g x ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : Ω), limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
      (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
compl₁₁ compl₁₂ :
  HSub.hSub (α := ℝ) (∫ (x : Ω), limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
      (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : Ω), limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
      (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)

Tactic:
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 _ _)]

Premises used: MeasureTheory.measure_lt_top, MeasureTheory.setIntegral_trim, MeasurableSet.compl, OfNat.ofNat, MeasureTheory.setIntegral_univ, MeasurableSet.univ, MeasureTheory.Filtration.stronglyMeasurable_limitProcess, MeasureTheory.integral_trim