-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem 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.e'_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ ∫⁻ (x : α), ↑(g₀ x) ∂μ = ∫⁻ (a : α), (ofNNReal ∘ ⇑g₀) a ∂μ

Tactic:
simp only [Function.comp_apply]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
h'L : L < ∫⁻ (x : α), ↑(g₀ x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
rcases SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral h'L with ⟨g, hg, gL, gtop⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
h'L : L < ∫⁻ (x : α), ↑(g₀ x) ∂μ
g : α →ₛ ℝ≥0
hg : ∀ (x : α), g x ≤ g₀ x
gL : ∫⁻ (x : α), ↑(g x) ∂μ < ⊤
gtop : L < ∫⁻ (x : α), ↑(g x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
h'L : L < ∫⁻ (x : α), ↑(g₀ x) ∂μ
g : α →ₛ ℝ≥0
hg : ∀ (x : α), g x ≤ g₀ x
gL : ∫⁻ (x : α), ↑(g x) ∂μ < ⊤
gtop : L < ∫⁻ (x : α), ↑(g x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
exact ⟨g, fun x => (hg x).trans (coe_le_coe.1 (hg₀ x)), gL, gtop⟩

Result:
no goals

Proof state:
case h.e'_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ ∫⁻ (x : α), ↑(g₀ x) ∂μ = (SimpleFunc.map ofNNReal g₀).lintegral μ

Tactic:
rw [← SimpleFunc.lintegral_eq_lintegral, coe_map]

Result:
case h.e'_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ ∫⁻ (x : α), ↑(g₀ x) ∂μ = ∫⁻ (a : α), (ofNNReal ∘ ⇑g₀) a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(f x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
simp_rw [lintegral_eq_nnreal, lt_iSup_iff] at hL

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : ∃ i, ∃ (_ : ∀ (x : α), ↑(i x) ≤ ↑(f x)), L < (SimpleFunc.map ofNNReal i).lintegral μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Proof state:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
have h'L : L < ∫⁻ x, g₀ x ∂μ := by
  convert g₀L
  rw [← SimpleFunc.lintegral_eq_lintegral, coe_map]
  simp only [Function.comp_apply]

Result:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
h'L : L < ∫⁻ (x : α), ↑(g₀ x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : ∃ i, ∃ (_ : ∀ (x : α), ↑(i x) ≤ ↑(f x)), L < (SimpleFunc.map ofNNReal i).lintegral μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
rcases hL with ⟨g₀, hg₀, g₀L⟩

Result:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ L < ∫⁻ (x : α), ↑(g₀ x) ∂μ

Tactic:
convert g₀L

Result:
case h.e'_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ ∫⁻ (x : α), ↑(g₀ x) ∂μ = (SimpleFunc.map ofNNReal g₀).lintegral μ