awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
this : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
const :
  ∀ (t : Set α) (ht : MeasurableSet t) (ts : t ⊆ s) (mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t)
    (t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α),
          LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0)
            ((piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0) : (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)
          ((piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
obtain ⟨t, ht, ts, mlt, t_top⟩ :
      ∃ t : Set α, MeasurableSet t ∧ t ⊆ s ∧ L / ↑c < μ t ∧ μ t < ∞ :=
      Measure.exists_subset_measure_lt_top hs this

Premises used: MeasureTheory.Measure.exists_subset_measure_lt_top, Set
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
this : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α),
        LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0)
          ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
⟨piecewise t ht (const α c) (const α 0), fun x => ?_, ?_, ?_⟩

Premises used: MeasureTheory.SimpleFunc.const, And.intro, Exists.intro, OfNat.ofNat, MeasureTheory.SimpleFunc.piecewise
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
this : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
const :
  ∀ (x : α),
    LE.le (α := ℝ≥0) ((piecewise t ht (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
      ((piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
const₁ : ∫⁻ (x : α), (↑((piecewise t ht (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞
const₂ : L < ∫⁻ (x : α), (↑((piecewise t ht (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α),
        LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0)
          ((piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
refine ⟨piecewise t ht (const α c) (const α 0), fun x => ?_, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
this : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
⊢ LE.le (α := ℝ≥0) ((piecewise t ht (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
    ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)

Tactic:
indicator_le_indicator_of_subset ts (fun x => ?_) x

Premises used: Set.indicator_le_indicator_of_subset, Set.indicator, Set.piecewise, ite
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
this : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
const :
  ∀ (x : α),
    LE.le (α := (fun (a : α) ↦ ℝ≥0) x) (0 x : ℝ≥0) (((SimpleFunc.const α c : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
⊢ LE.le (α := ℝ≥0) ((piecewise t ht (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
    ((piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)

Tactic:
refine indicator_le_indicator_of_subset ts (fun x => ?_) x

Premises used: Set.indicator_le_indicator_of_subset
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
this : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x_1 x : α
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0) x) (0 x : ℝ≥0) (((const α c : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
this : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x_1 x : α
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0) x) (0 x : ℝ≥0) (((const α c : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
this : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α), (↑((piecewise t ht (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞

Tactic:
simp only [ht, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero, univ_inter,
        piecewise_eq_indicator, ENNReal.coe_indicator, Function.const_apply, lintegral_indicator,
        lintegral_const, Measure.restrict_apply', ENNReal.mul_lt_top ENNReal.coe_lt_top t_top]

Premises used: Function.const_apply, MeasureTheory.lintegral_const, MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, Set.univ_inter, ENNReal.mul_lt_top, MeasureTheory.lintegral_indicator, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, MeasureTheory.Measure.restrict_apply', MeasureTheory.SimpleFunc.coe_const, ENNReal.coe_lt_top, ENNReal.coe_indicator
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
this : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
const : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ L < ∫⁻ (x : α), (↑((piecewise t ht (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
simp only [ht, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero,
        piecewise_eq_indicator, ENNReal.coe_indicator, Function.const_apply, lintegral_indicator,
        lintegral_const, Measure.restrict_apply', univ_inter]

Premises used: Function.const_apply, MeasureTheory.lintegral_const, MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, Set.univ_inter, MeasureTheory.lintegral_indicator, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, MeasureTheory.Measure.restrict_apply', MeasureTheory.SimpleFunc.coe_const, ENNReal.coe_indicator
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
this : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
const : (↑c : ℝ≥0∞) ≠ 0 ∨ L ≠ 0
const₁ : (↑c : ℝ≥0∞) ≠ ∞ ∨ L ≠ ∞
⊢ L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rwa [mul_comm, ← ENNReal.div_lt_iff]

Premises used: mul_comm, ENNReal.div_lt_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
this : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑c : ℝ≥0∞) ≠ 0 ∨ L ≠ 0

Tactic:
simp only [c_ne_zero, Ne, ENNReal.coe_eq_zero, not_false_iff, true_or]

Premises used: true_or, Ne, ENNReal.coe_eq_zero, not_false_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c_ne_zero : c ≠ 0
this : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / (↑c : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) t
t_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑c : ℝ≥0∞) ≠ ∞ ∨ L ≠ ∞

Tactic:
simp only [Ne, coe_ne_top, not_false_iff, true_or]

Premises used: true_or, Ne, not_false_iff, ENNReal.coe_ne_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 : L < ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
rwa rwa₁ rwa₂ rwa₃ : L < ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) + (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ
⊢ L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
rwa [← lintegral_add_left f₁.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 : L < ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ 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]
-- 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∞) ∂μ
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
⊢ L < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
simp only [hf₁, zero_add] at hL

Premises used: zero_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∞
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
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
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
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_left, zero_le']

Premises used: MeasureTheory.SimpleFunc.coe_add, Pi.add_apply, zero_le', le_add_iff_nonneg_left