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

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

Tactic:
intro n

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

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

Tactic:
rw [← SimpleFunc.const_mul_lintegral, ← SimpleFunc.lintegral_eq_lintegral]

Result:
no goals

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

Tactic:
exact mul_le_mul_left' (monotone_eapprox _ h _) _

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

Tactic:
funext a

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

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

Tactic:
rw [← ENNReal.mul_iSup, lintegral_eq_iSup_eapprox_lintegral hf]

Result:
no goals

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

Tactic:
congr

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

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

Tactic:
rw [lintegral_iSup]

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

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

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

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

Tactic:
rw [← iSup_eapprox_apply hf, ENNReal.mul_iSup]

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

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

Tactic:
exact SimpleFunc.measurable _

Result:
no goals

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

Tactic:
congr

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

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

Tactic:
funext n

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

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

Tactic:
intro i j h a

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