-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_eq_iSup_eapprox_lintegral {f : α → ℝ≥0∞} (hf : Measurable f) :
    ∫⁻ a, f a ∂μ = ⨆ n, (eapprox f n).lintegral μ :=
  calc
    ∫⁻ a, f a ∂μ = ∫⁻ a, ⨆ n, (eapprox f n : α → ℝ≥0∞) a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ⨆ n, ∫⁻ (a : α), (eapprox f n) a ∂μ = ⨆ n, (eapprox f n).lintegral μ

Tactic:
congr

Result:
case e_s
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun n => ∫⁻ (a : α), (eapprox f n) a ∂μ) = fun n => (eapprox f n).lintegral μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), ⨆ n, (eapprox f n) a ∂μ = ⨆ n, ∫⁻ (a : α), (eapprox f n) a ∂μ

Tactic:
apply lintegral_iSup

Result:
case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable ⇑(eapprox f n)

case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Monotone fun n => ⇑(eapprox f n)

Proof state:
case e_s
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun n => ∫⁻ (a : α), (eapprox f n) a ∂μ) = fun n => (eapprox f n).lintegral μ

Tactic:
ext n

Result:
case e_s.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ ∫⁻ (a : α), (eapprox f n) a ∂μ = (eapprox f n).lintegral μ

Proof state:
case e_f.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ f a = ⨆ n, (eapprox f n) a

Tactic:
rw [iSup_eapprox_apply hf]

Result:
no goals

Proof state:
case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable ⇑(eapprox f n)

Tactic:
measurability

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), ⨆ n, (eapprox f n) a ∂μ

Tactic:
congr

Result:
case e_f
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun a => f a) = fun a => ⨆ n, (eapprox f n) a

Proof state:
case e_f
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun a => f a) = fun a => ⨆ n, (eapprox f n) a

Tactic:
ext a

Result:
case e_f.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ f a = ⨆ n, (eapprox f n) a

Proof state:
case e_s.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ ∫⁻ (a : α), (eapprox f n) a ∂μ = (eapprox f n).lintegral μ

Tactic:
rw [(eapprox f n).lintegral_eq_lintegral]

Result:
no goals

Proof state:
case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
⊢ (fun n => ⇑(eapprox f n)) i ≤ (fun n => ⇑(eapprox f n)) j

Tactic:
exact monotone_eapprox f h

Result:
no goals

Proof state:
case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Monotone fun n => ⇑(eapprox f n)

Tactic:
intro i j h

Result:
case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
⊢ (fun n => ⇑(eapprox f n)) i ≤ (fun n => ⇑(eapprox f n)) j