-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem exists_simpleFunc_forall_lintegral_sub_lt_of_pos {f : α → ℝ≥0∞} (h : ∫⁻ x, f x ∂μ ≠ ∞)
    {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ φ : α →ₛ ℝ≥0,
      (∀ x, ↑(φ x) ≤ f x) ∧
        ∀ ψ : α →ₛ ℝ≥0, (∀ x, ↑(ψ x) ≤ f x) → (map (↑) (ψ - φ)).lintegral μ < ε

Proof state:
case intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
⊢ ∃ φ,
    (∀ (x : α), ↑(φ x) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Tactic:
refine ⟨φ, hle, fun ψ hψ => ?_⟩

Result:
case intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
⊢ (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
this :
  ∃ i,
    ∃ (_ : i ∈ fun φ => ∀ (x : α), ↑(φ x) ≤ f x),
      ∃ b < (SimpleFunc.map ofNNReal i).lintegral μ + ε,
        ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
⊢ ∃ φ,
    (∀ (x : α), ↑(φ x) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Tactic:
rcases this with ⟨φ, hle : ∀ x, ↑(φ x) ≤ f x, b, hbφ, hb⟩

Result:
case intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
⊢ ∃ φ,
    (∀ (x : α), ↑(φ x) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Proof state:
case intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
⊢ (SimpleFunc.map ofNNReal (φ + (ψ - φ))).lintegral μ < (SimpleFunc.map ofNNReal φ).lintegral μ + ε

Tactic:
refine (hb _ fun x => le_trans ?_ (max_le (hle x) (hψ x))).trans_lt hbφ

Result:
case intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
x : α
⊢ ↑((φ + (ψ - φ)) x) ≤ ↑(φ x) ⊔ ↑(ψ x)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ φ,
    (∀ (x : α), ↑(φ x) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Tactic:
have := ENNReal.lt_add_right h hε

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
this :
  ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ <
    (⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ) + ε
⊢ ∃ φ,
    (∀ (x : α), ↑(φ x) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Proof state:
case intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
x : α
⊢ ↑((φ + (ψ - φ)) x) ≤ ↑(φ x) ⊔ ↑(ψ x)

Tactic:
norm_cast

Result:
case intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤
x : α
⊢ (φ + (ψ - φ)) x ≤ φ x ⊔ ψ x