-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_eq_nnreal {m : MeasurableSpace α} (f : α → ℝ≥0∞) (μ : Measure α) :
    ∫⁻ a, f a ∂μ =
      ⨆ (φ : α →ₛ ℝ≥0) (_ : ∀ x, ↑(φ x) ≤ f x), (φ.map ((↑) : ℝ≥0 → ℝ≥0∞)).lintegral μ

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
⊢ ∫⁻ (a : α), f a ∂μ = ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
rw [lintegral]

Result:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral μ =
    ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral μ =
    ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
refine
  le_antisymm (iSup₂_le fun φ hφ ↦ ?_) (iSup_mono' fun φ ↦ ⟨φ.map ((↑) : ℝ≥0 → ℝ≥0∞), le_rfl⟩)

Result:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
by_cases h : ∀ᵐ a ∂μ, φ a ≠ ∞

Result:
case pos
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

case neg
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
ψ : α →ₛ ℝ≥0 := SimpleFunc.map ENNReal.toNNReal φ
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
replace h : ψ.map ((↑) : ℝ≥0 → ℝ≥0∞) =ᵐ[μ] φ := h.mono fun a => ENNReal.coe_toNNReal

Result:
case pos
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
ψ : α →ₛ ℝ≥0 := SimpleFunc.map ENNReal.toNNReal φ
h : ⇑(SimpleFunc.map ofNNReal ψ) =ᶠ[ae μ] ⇑φ
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
let ψ := φ.map ENNReal.toNNReal

Result:
case pos
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
ψ : α →ₛ ℝ≥0 := SimpleFunc.map ENNReal.toNNReal φ
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Proof state:
case neg.intro
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
b : ℝ≥0∞
hb : b < ⊤
n : ℕ
hn : b < ↑n * μ (⇑φ ⁻¹' {⊤})
⊢ ∃ i, b < ⨆ (_ : ∀ (x : α), ↑(i x) ≤ f x), (SimpleFunc.map ofNNReal i).lintegral μ

Tactic:
use (const α (n : ℝ≥0)).restrict (φ ⁻¹' {∞})

Result:
case h
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
b : ℝ≥0∞
hb : b < ⊤
n : ℕ
hn : b < ↑n * μ (⇑φ ⁻¹' {⊤})
⊢ b <
    ⨆ (_ : ∀ (x : α), ↑(((const α ↑n).restrict (⇑φ ⁻¹' {⊤})) x) ≤ f x),
      (SimpleFunc.map ofNNReal ((const α ↑n).restrict (⇑φ ⁻¹' {⊤}))).lintegral μ

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
refine le_trans le_top (ge_of_eq <| (iSup_eq_top _).2 fun b hb => ?_)

Result:
case neg
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
b : ℝ≥0∞
hb : b < ⊤
⊢ ∃ i, b < ⨆ (_ : ∀ (x : α), ↑(i x) ≤ f x), (SimpleFunc.map ofNNReal i).lintegral μ

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
b : ℝ≥0∞
hb : b < ⊤
⊢ ∃ i, b < ⨆ (_ : ∀ (x : α), ↑(i x) ≤ f x), (SimpleFunc.map ofNNReal i).lintegral μ

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, b < n * μ (φ ⁻¹' {∞}) := exists_nat_mul_gt h_meas (ne_of_lt hb)

Result:
case neg.intro
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
b : ℝ≥0∞
hb : b < ⊤
n : ℕ
hn : b < ↑n * μ (⇑φ ⁻¹' {⊤})
⊢ ∃ i, b < ⨆ (_ : ∀ (x : α), ↑(i x) ≤ f x), (SimpleFunc.map ofNNReal i).lintegral μ

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
have h_meas : μ (φ ⁻¹' {∞}) ≠ 0 := mt measure_zero_iff_ae_nmem.1 h

Result:
case neg
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
b : ℝ≥0∞
hb : b < ⊤
n : ℕ
hn : b < ↑n * μ (⇑φ ⁻¹' {⊤})
⊢ (∀ (x : α), (⇑φ ⁻¹' {⊤}).indicator (fun x => ↑(Function.const α (↑n) x)) x ≤ f x) ∧ b < ↑n * μ (⇑φ ⁻¹' {⊤})

Tactic:
refine ⟨indicator_le fun x hx => le_trans ?_ (hφ _), hn⟩

Result:
case h
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
b : ℝ≥0∞
hb : b < ⊤
n : ℕ
hn : b < ↑n * μ (⇑φ ⁻¹' {⊤})
x : α
hx : x ∈ ⇑φ ⁻¹' {⊤}
⊢ ↑(Function.const α (↑n) x) ≤ φ x

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
b : ℝ≥0∞
hb : b < ⊤
n : ℕ
hn : b < ↑n * μ (⇑φ ⁻¹' {⊤})
x : α
hx : x ∈ ⇑φ ⁻¹' {⊤}
⊢ ↑(Function.const α (↑n) x) ≤ φ x

Tactic:
simp only [mem_preimage, mem_singleton_iff] at hx

Result:
case h
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
b : ℝ≥0∞
hb : b < ⊤
n : ℕ
hn : b < ↑n * μ (⇑φ ⁻¹' {⊤})
x : α
hx : φ x = ⊤
⊢ ↑(Function.const α (↑n) x) ≤ φ x

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
ψ : α →ₛ ℝ≥0 := SimpleFunc.map ENNReal.toNNReal φ
h : ⇑(SimpleFunc.map ofNNReal ψ) =ᶠ[ae μ] ⇑φ
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
have : ∀ x, ↑(ψ x) ≤ f x := fun x => le_trans ENNReal.coe_toNNReal_le_self (hφ x)

Result:
case pos
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
ψ : α →ₛ ℝ≥0 := SimpleFunc.map ENNReal.toNNReal φ
h : ⇑(SimpleFunc.map ofNNReal ψ) =ᶠ[ae μ] ⇑φ
this : ∀ (x : α), ↑(ψ x) ≤ f x
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ