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

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

Tactic:
simp only [Pi.add_apply]

Result:
no goals

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

Tactic:
simp only [iSup_eapprox_apply, hf, hg]

Result:
no goals

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

Tactic:
intro i j h

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

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

Tactic:
rw [ENNReal.iSup_add_iSup_of_monotone]

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

case e_f.h.hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ Monotone fun n => (eapprox f n) a

case e_f.h.hg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ Monotone fun n => (eapprox g n) a

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

Tactic:
simp only [Pi.add_apply, SimpleFunc.coe_add]

Result:
no goals

Proof state:
case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
i j : ℕ
h : i ≤ j
a : α
⊢ (eapprox f i) a + (eapprox g i) a ≤ (eapprox f j) a + (eapprox g j) a

Tactic:
gcongr <;> exact monotone_eapprox _ h _

Result:
no goals

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

Tactic:
congr

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

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

Tactic:
intro i j h

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

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

Tactic:
exact SimpleFunc.lintegral_mono (monotone_eapprox _ h) le_rfl

Result:
no goals

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

Tactic:
rw [lintegral_eq_iSup_eapprox_lintegral hf, lintegral_eq_iSup_eapprox_lintegral hg]

Result:
no goals

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

Tactic:
dsimp

Result:
case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
i j : ℕ
h : i ≤ j
a : α
⊢ (eapprox f i) a + (eapprox g i) a ≤ (eapprox f j) a + (eapprox g j) a

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

Tactic:
intro i j h a

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

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

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

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

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

Tactic:
exact monotone_eapprox _ h a

Result:
no goals

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

Tactic:
rw [lintegral_iSup]

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

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

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

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

Tactic:
funext n

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

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

Tactic:
fun_prop

Result:
no goals

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

Tactic:
funext a

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