awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L : ℝ≥0∞
hL_1 : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hf₁ : ¬∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₁ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)
g₁_top : ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₂ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)
g₂_top : ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
apply :
  ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞

Tactic:
apply lt_of_le_of_lt _ (add_lt_top.2 ⟨g₁_top, g₂_top⟩)

Premises used: Iff.mpr, lt_of_le_of_lt, And.intro, ENNReal.add_lt_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L : ℝ≥0∞
hL_1 : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hf₁ : ¬∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₁ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)
g₁_top : ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₂ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)
g₂_top : ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
rw :
  ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (a : α), (↑((g₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) + (↑((g₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ
⊢ ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
rw [← lintegral_add_left g₁.measurable.coe_nnreal_ennreal]

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.SimpleFunc.measurable, MeasureTheory.lintegral_add_left
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L : ℝ≥0∞
hL_1 : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hf₁ : ¬∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₁ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)
g₁_top : ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₂ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)
g₂_top : ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (a : α), (↑((g₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) + (↑((g₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ

Tactic:
le_rfl

Premises used: ENNReal.ofNNReal, le_rfl, WithTop.map₂, WithTop.some, Option.map₂
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L : ℝ≥0∞
hL_1 : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hf₁ : ¬∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₁ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)
g₁_top : ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₂ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)
g₂_top : ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (a : α), (↑((g₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) + (↑((g₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L : ℝ≥0∞
hL_1 : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hf₁ : ¬∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₁ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)
g₁_top : ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₂ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)
g₂_top : ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
apply :
  ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ L < ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
apply hL.trans ((ENNReal.add_lt_add hg₁ hg₂).trans_le _)

Premises used: LT.lt.trans_le, LT.lt.trans, ENNReal.add_lt_add
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L : ℝ≥0∞
hL_1 : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hf₁ : ¬∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₁ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)
g₁_top : ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₂ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)
g₂_top : ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
rw :
  ∫⁻ (a : α), (↑((g₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) + (↑((g₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
rw [← lintegral_add_left g₁.measurable.coe_nnreal_ennreal]

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.SimpleFunc.measurable, MeasureTheory.lintegral_add_left
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L : ℝ≥0∞
hL_1 : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hf₁ : ¬∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₁ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)
g₁_top : ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), LE.le (α := ℝ≥0) ((g₂ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)
g₂_top : ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ ∫⁻ (a : α), (↑((g₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) + (↑((g₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
simp only [coe_add, Pi.add_apply, ENNReal.coe_add, le_rfl]

Premises used: le_rfl, MeasureTheory.SimpleFunc.coe_add, ENNReal.coe_add, Pi.add_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ
⊢ ∃ (i : α →ₛ ℝ≥0) (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
    L < (SimpleFunc.map ofNNReal i).lintegral μ

Tactic:
simp_rw [lintegral_eq_nnreal, lt_iSup_iff] at hL

Premises used: MeasureTheory.lintegral_eq_nnreal, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL :
  ∃ (i : α →ₛ ℝ≥0) (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
    L < (SimpleFunc.map ofNNReal i).lintegral μ
rcases :
  ∀ (g₀ : α →ₛ ℝ≥0) (hg₀ : ∀ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞))
    (g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), (g : (a : α) → ℝ≥0) x ≤ f x) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α), (g : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
rcases hL with ⟨g₀, hg₀, g₀L⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ L < (SimpleFunc.map ofNNReal g₀).lintegral μ

Tactic:
g₀L
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
h : ∫⁻ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ L < ∫⁻ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
convert! g₀L
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
h : ∫⁻ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (a : α), (ofNNReal ∘ (⇑g₀ : (a : α) → ℝ≥0)) a ∂μ
⊢ ∫⁻ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = (SimpleFunc.map ofNNReal g₀).lintegral μ

Tactic:
rw [← SimpleFunc.lintegral_eq_lintegral, SimpleFunc.coe_map]

Premises used: MeasureTheory.SimpleFunc.coe_map, MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ ∫⁻ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (a : α), (ofNNReal ∘ (⇑g₀ : (a : α) → ℝ≥0)) a ∂μ

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ L < ∫⁻ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
have h'L : L < ∫⁻ x, g₀ x ∂μ := by
    convert! g₀L
    rw [← SimpleFunc.lintegral_eq_lintegral, SimpleFunc.coe_map]
    simp only [Function.comp_apply]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
h'L : L < ∫⁻ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
rcases :
  ∀ (g : α →ₛ ℝ≥0) (hg : ∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((g₀ : (a : α) → ℝ≥0) x : ℝ≥0))
    (gL : ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞)
    (gtop : L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α), (g : (a : α) → ℝ≥0) x ≤ f x) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α), (g : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
rcases SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral h'L with ⟨g, hg, gL, gtop⟩

Premises used: MeasureTheory.SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
h'L : L < ∫⁻ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
g : α →ₛ ℝ≥0
hg : ∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((g₀ : (a : α) → ℝ≥0) x : ℝ≥0)
gL : ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
gtop : L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α), (g : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
⟨g, fun x => (hg x).trans (ENNReal.coe_le_coe.1 (hg₀ x)), gL, gtop⟩

Premises used: ENNReal.coe_le_coe, And.intro, Exists.intro, Iff.mp, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
h'L : L < ∫⁻ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
g : α →ₛ ℝ≥0
hg : ∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((g₀ : (a : α) → ℝ≥0) x : ℝ≥0)
gL : ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
gtop : L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α), (g : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
exact ⟨g, fun x => (hg x).trans (ENNReal.coe_le_coe.1 (hg₀ x)), gL, gtop⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
⊢ ⨅ (n : ℕ), ∫⁻ (a : α), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a ∂μ = ∫⁻ (a : α), ⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a ∂μ

Tactic:
(lintegral_iInf ?_ ?_ ?_).symm

Premises used: MeasureTheory.lintegral_iInf, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
refine_1 : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a
refine_2 : Antitone.{0, u_1} (β := α → ℝ≥0∞) fun (n : ℕ) (a : α) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a
refine_3 : ∫⁻ (a : α), ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i a ∂μ ≠ ∞
⊢ ⨅ (n : ℕ), ∫⁻ (a : α), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a ∂μ = ∫⁻ (a : α), ⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a ∂μ

Tactic:
refine (lintegral_iInf ?_ ?_ ?_).symm

Premises used: MeasureTheory.lintegral_iInf, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
n : ℕ
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a

Tactic:
.biSup _ (Set.to_countable _) (fun i _ ↦ hf_meas i)

Premises used: Measurable.biSup, Set.Mem, Set.to_countable
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
n : ℕ
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a

Tactic:
exact .biSup _ (Set.to_countable _) (fun i _ ↦ hf_meas i)