-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral {m : MeasurableSpace α}
    {μ : Measure α} [SigmaFinite μ] {f : α →ₛ ℝ≥0} {L : ℝ≥0∞} (hL : L < ∫⁻ x, f x ∂μ) :
    ∃ g : α →ₛ ℝ≥0, (∀ x, g x ≤ f x) ∧ ∫⁻ x, g x ∂μ < ∞ ∧ L < ∫⁻ x, g x ∂μ

Proof state:
case h_ind.intro.intro.intro.intro.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ⊤
⊢ ∫⁻ (x : α), ↑((piecewise t ht (const α c) (const α 0)) x) ∂μ < ⊤

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]

Result:
no goals

Proof state:
case h_ind.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ⊤
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

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

Result:
case h_ind.intro.intro.intro.intro.refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ⊤
x : α
⊢ (piecewise t ht (const α c) (const α 0)) x ≤ (piecewise s hs (const α c) (const α 0)) x

case h_ind.intro.intro.intro.intro.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ⊤
⊢ ∫⁻ (x : α), ↑((piecewise t ht (const α c) (const α 0)) x) ∂μ < ⊤

case h_ind.intro.intro.intro.intro.refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ⊤
⊢ L < ∫⁻ (x : α), ↑((piecewise t ht (const α c) (const α 0)) x) ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ⇑f₁) (support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hL✝ : L < ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ
hf₁ : ¬∫⁻ (x : α), ↑(f₁ x) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), ↑(f₂ x) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(f₁ x) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), ↑(f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), g₁ x ≤ f₁ x
g₁_top : ∫⁻ (x : α), ↑(g₁ x) ∂μ < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), g₂ x ≤ f₂ x
g₂_top : ∫⁻ (x : α), ↑(g₂ x) ∂μ < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(g₂ x) ∂μ
⊢ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ∫⁻ (x : α), ↑(g₂ x) ∂μ ≤ ∫⁻ (x : α), ↑((g₁ + g₂) x) ∂μ

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

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ⇑f₁) (support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hL✝ : L < ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ
hf₁ : ¬∫⁻ (x : α), ↑(f₁ x) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), ↑(f₂ x) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(f₁ x) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), ↑(f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), g₁ x ≤ f₁ x
g₁_top : ∫⁻ (x : α), ↑(g₁ x) ∂μ < ⊤
hg₁ : L₁ < ∫⁻ (x : α), ↑(g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), g₂ x ≤ f₂ x
g₂_top : ∫⁻ (x : α), ↑(g₂ x) ∂μ < ⊤
hg₂ : L₂ < ∫⁻ (x : α), ↑(g₂ x) ∂μ
⊢ ∫⁻ (a : α), ↑(g₁ a) + ↑(g₂ a) ∂μ ≤ ∫⁻ (x : α), ↑((g₁ + g₂) x) ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ⇑f₁) (support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ
⊢ L < ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ

Tactic:
rwa [← lintegral_add_left f₁.measurable.coe_nnreal_ennreal]

Result:
no goals

Proof state:
case pos.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (support ⇑f₁) (support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hf₁ : ∫⁻ (x : α), ↑(f₁ x) ∂μ = 0
hL : L < ∫⁻ (x : α), ↑(f₂ x) ∂μ
g : α →ₛ ℝ≥0
g_le : ∀ (x : α), g x ≤ f₂ x
g_top : ∫⁻ (x : α), ↑(g x) ∂μ < ⊤
gL : L < ∫⁻ (x : α), ↑(g x) ∂μ
x : α
⊢ f₂ x ≤ (f₁ + f₂) x

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

Result:
no goals

Proof state:
case h_ind
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

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

Result:
case h_ind.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ⊤
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ