awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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),
    (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ + f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have neg : ∀ (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),
    (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ + f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
Tactic: rcases h₁ hL₁ with ⟨g₁, g₁_le, g₁_top, hg₁⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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),
    (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ + f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have neg : ∀ (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),
    (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ + f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
Tactic: rcases h₂ hL₂ with ⟨g₂, g₂_le, g₂_top, hg₂⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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∞) ∂μ
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ + f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have neg : ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
Tactic: refine ⟨g₁ + g₂, fun x => add_le_add (g₁_le x) (g₂_le x), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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∞) ∂μ
neg : ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ + f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have neg₁ : L < ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
Tactic: refine ⟨g₁ + g₂, fun x => add_le_add (g₁_le x) (g₂_le x), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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∞) ∂μ < ∞
have apply : ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
  ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
Tactic: apply lt_of_le_of_lt _ (add_lt_top.2 ⟨g₁_top, g₂_top⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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∞) ∂μ ≤
    ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have rw : ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
  ∫⁻ (a : α), (↑((g₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) + (↑((g₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ
Tactic: rw [← lintegral_add_left g₁.measurable.coe_nnreal_ennreal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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∞) ∂μ
⊢ L < ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have apply : ∫⁻ (x : α), (↑((g₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
  ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
Tactic: apply hL.trans ((ENNReal.add_lt_add hg₁ hg₂).trans_le _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have rw : ∫⁻ (a : α), (↑((g₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) + (↑((g₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≤
  ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
Tactic: rw [← lintegral_add_left g₁.measurable.coe_nnreal_ennreal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α), (g : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have hL₁ : ∃ (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
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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 μ
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α), (g : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have 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∞) ∂μ
Tactic: rcases hL with ⟨g₀, hg₀, g₀L⟩
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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∞) ∂μ
have h : ∫⁻ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = (SimpleFunc.map ofNNReal g₀).lintegral μ
Tactic: convert! g₀L
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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∞) ∂μ = (SimpleFunc.map ofNNReal g₀).lintegral μ
have h : ∫⁻ (x : α), (↑((g₀ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (a : α), (ofNNReal ∘ (⇑g₀ : (a : α) → ℝ≥0)) a ∂μ
Tactic: rw [← SimpleFunc.lintegral_eq_lintegral, SimpleFunc.coe_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
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 μ
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α), (g : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have h'L : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
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),
    (∀ (x : α), (g : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have 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∞) ∂μ
Tactic: rcases SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral h'L with ⟨g, hg, gL, gtop⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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 ∂μ
have refine_1 : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a
Tactic: refine (lintegral_iInf ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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
⊢ ⨅ (n : ℕ), ∫⁻ (a : α), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a ∂μ = ∫⁻ (a : α), ⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a ∂μ
have refine_2 : Antitone.{0, u_1} (β := α → ℝ≥0∞) fun (n : ℕ) (a : α) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a
Tactic: refine (lintegral_iInf ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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
⊢ ⨅ (n : ℕ), ∫⁻ (a : α), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a ∂μ = ∫⁻ (a : α), ⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a ∂μ
have refine_3 : ∫⁻ (a : α), ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i a ∂μ ≠ ∞
Tactic: refine (lintegral_iInf ?_ ?_ ?_).symm