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 : L < ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have rwa : L < ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) + (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ
Tactic: rwa [← lintegral_add_left f₁.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₁ 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 : L < ∫⁻ (x : α), (↑((f₁ + f₂ : (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 hL₁ : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
Tactic: replace hL : L < ∫⁻ x, f₁ x ∂μ + ∫⁻ x, f₂ x ∂μ := by
      rwa [← lintegral_add_left f₁.measurable.coe_nnreal_ennreal]
Cleared hypotheses: hL
-- 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 : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (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 pos : ∀ (hf₁ : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 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: by_cases hf₁ : ∫⁻ x, f₁ x ∂μ = 0
-- 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 : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
pos :
  ∀ (hf₁ : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 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∞) ∂μ
⊢ ∃ (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 : ∀ (hf₁ : ¬∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 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: by_cases hf₁ : ∫⁻ x, f₁ x ∂μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
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 : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hf₁ : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 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 hL₁ : L < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
Tactic: simp only [hf₁, zero_add] 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₁ 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∞
hf₁ : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hL : L < ∫⁻ (x : α), (↑((f₂ : (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 pos : ∀ (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∞) ∂μ < ∞)
  (gL : 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, gL⟩
-- 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∞
hf₁ : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hL : L < ∫⁻ (x : α), (↑((f₂ : (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∞) ∂μ < ∞
gL : 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 pos : ∀ (x : α), LE.le (α := ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ + f₂ : (a : α) → ℝ≥0) x : ℝ≥0)
Tactic: refine ⟨g, fun x => (g_le x).trans ?_, g_top, gL⟩
-- 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 : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hf₁ : ¬∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 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 pos : ∀ (hf₂ : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 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: by_cases hf₂ : ∫⁻ x, f₂ x ∂μ = 0
-- 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 : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
hf₁ : ¬∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
pos :
  ∀ (hf₂ : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 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∞) ∂μ
⊢ ∃ (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 : ∀ (hf₂ : ¬∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 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: by_cases hf₂ : ∫⁻ x, f₂ x ∂μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
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 : 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
⊢ ∃ (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 hL₁ : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
Tactic: simp only [hf₂, add_zero] 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₁ 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∞
hf₁ : ¬∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hf₂ : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hL : L < ∫⁻ (x : α), (↑((f₁ : (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 pos : ∀ (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∞) ∂μ < ∞)
  (gL : 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, gL⟩
-- 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∞
hf₁ : ¬∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hf₂ : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hL : L < ∫⁻ (x : α), (↑((f₁ : (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∞) ∂μ < ∞
gL : 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 pos : ∀ (x : α), LE.le (α := ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ + f₂ : (a : α) → ℝ≥0) x : ℝ≥0)
Tactic: refine ⟨g, fun x => (g_le x).trans ?_, g_top, gL⟩
-- 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 : 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
⊢ ∃ (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₁ : ℝ≥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∞) ∂μ
Tactic: obtain ⟨L₁, hL₁, L₂, hL₂, hL⟩ : ∃ L₁ < ∫⁻ x, f₁ x ∂μ, ∃ L₂ < ∫⁻ x, f₂ x ∂μ, L < L₁ + L₂ :=
      ENNReal.exists_lt_add_of_lt_add hL hf₁ hf₂