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 : 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∞) ∂μ
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∞) ∂μ
⊢ ∃ (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
-- 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 : 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 < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
simp only [hf₂, add_zero] at hL

Premises used: add_zero
-- 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∞
hf₁ : ¬∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hf₂ : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = 0
hL : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
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∞) ∂μ
⊢ ∃ (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⟩
-- 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∞
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∞) ∂μ

Tactic:
⟨g, fun x => (g_le x).trans ?_, g_top, gL⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- 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∞
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∞) ∂μ
pos : ∀ (x : α), LE.le (α := ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0) ((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∞) ∂μ

Tactic:
refine ⟨g, fun x => (g_le x).trans ?_, g_top, gL⟩
-- 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∞
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∞) ∂μ
x : α
⊢ LE.le (α := ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ + f₂ : (a : α) → ℝ≥0) x : ℝ≥0)

Tactic:
simp only [SimpleFunc.coe_add, Pi.add_apply, le_add_iff_nonneg_right, zero_le']

Premises used: le_add_iff_nonneg_right, MeasureTheory.SimpleFunc.coe_add, Pi.add_apply, zero_le'
-- 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 : 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₁ < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ,
    ∃ L₂ < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ, L < L₁ + L₂

Tactic:
ENNReal.exists_lt_add_of_lt_add hL hf₁ hf₂

Premises used: ENNReal.exists_lt_add_of_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 : 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
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∞) ∂μ
⊢ ∃ (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₂

Premises used: ENNReal.exists_lt_add_of_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₂
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∞) ∂μ
⊢ ∃ (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₁⟩
-- 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∞) ∂μ
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∞) ∂μ
⊢ ∃ (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₂⟩
-- 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∞) ∂μ
⊢ ∃ (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:
⟨g₁ + g₂, fun x => add_le_add (g₁_le x) (g₂_le x), ?_, ?_⟩

Premises used: add_le_add, HAdd.hAdd, And.intro, Exists.intro
-- 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∞) ∂μ
neg : ∫⁻ (x : α), (↑((g₁ + g₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
neg₁ : L < ∫⁻ (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∞) ∂μ

Tactic:
refine ⟨g₁ + g₂, fun x => add_le_add (g₁_le x) (g₂_le x), ?_, ?_⟩