-- 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 pos
α : 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
hf₂ : ∫⁻ (x : α), ↑(f₂ x) ∂μ = 0
hL : L < ∫⁻ (x : α), ↑(f₁ x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
rcases h₁ hL with ⟨g, g_le, g_top, gL⟩

Result:
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
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) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Proof state:
α : 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
⊢ L / ↑c < μ s

Tactic:
rwa [ENNReal.div_lt_iff, mul_comm]

Result:
case h0
α : 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
⊢ ↑c ≠ 0 ∨ L ≠ 0

case ht
α : 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
⊢ ↑c ≠ ⊤ ∨ L ≠ ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
⊢ c ≠ 0

Tactic:
intro hc

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
hc : c = 0
⊢ False

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₁ + g₂) x) ∂μ ≤ ∫⁻ (a : α), ↑(g₁ a) + ↑(g₂ a) ∂μ

Tactic:
exact le_rfl

Result:
no goals

Proof state:
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 < ↑c * μ t

Tactic:
rwa [mul_comm, ← ENNReal.div_lt_iff]

Result:
case h_ind.intro.intro.intro.intro.refine_3.h0
α : 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 < ⊤
⊢ ↑c ≠ 0 ∨ L ≠ 0

case h_ind.intro.intro.intro.intro.refine_3.ht
α : 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 < ⊤
⊢ ↑c ≠ ⊤ ∨ L ≠ ⊤

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

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

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

Proof state:
case h0
α : 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
⊢ ↑c ≠ 0 ∨ L ≠ 0

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

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
hc : c = 0
⊢ False

Tactic:
simp only [hc, ENNReal.coe_zero, zero_mul, not_lt_zero] at hL

Result:
no goals

Proof state:
case pos
α : 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
⊢ ∃ g, (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

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

Result:
case pos
α : 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, (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ