α : Type u_2
β : Type u_1
γ : Type ?u.1033801
δ : Type ?u.1033804
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
⊢ (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) (Measure.map g μ)) =
    ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox (f ∘ g) n) μ
α : Type u_2
β : Type u_1
γ : Type ?u.1033801
δ : Type ?u.1033804
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
⊢ (∫⁻ (a : β), f a ∂Measure.map g μ) = ∫⁻ (a : α), f (g a) ∂μ
erw [lintegral_eq_iSup_eapprox_lintegral hf, lintegral_eq_iSup_eapprox_lintegral (hf.comp hg)]
case e_s.h
α : Type u_2
β : Type u_1
γ : Type ?u.1033801
δ : Type ?u.1033804
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ SimpleFunc.lintegral (eapprox f n) (Measure.map g μ) = SimpleFunc.lintegral (eapprox (f ∘ g) n) μ
α : Type u_2
β : Type u_1
γ : Type ?u.1033801
δ : Type ?u.1033804
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
⊢ (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) (Measure.map g μ)) =
    ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox (f ∘ g) n) μ
congr with n : 1
case h.e'_3.h.e'_3
α : Type u_2
β : Type u_1
γ : Type ?u.1033801
δ : Type ?u.1033804
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ eapprox (f ∘ g) n = comp (eapprox f n) g hg
case e_s.h
α : Type u_2
β : Type u_1
γ : Type ?u.1033801
δ : Type ?u.1033804
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ SimpleFunc.lintegral (eapprox f n) (Measure.map g μ) = SimpleFunc.lintegral (eapprox (f ∘ g) n) μ
convert SimpleFunc.lintegral_map _ hg
case h.e'_3.h.e'_3.H
α : Type u_2
β : Type u_1
γ : Type ?u.1033801
δ : Type ?u.1033804
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
x : α
⊢ ↑(eapprox (f ∘ g) n) x = ↑(comp (eapprox f n) g hg) x
case h.e'_3.h.e'_3
α : Type u_2
β : Type u_1
γ : Type ?u.1033801
δ : Type ?u.1033804
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ eapprox (f ∘ g) n = comp (eapprox f n) g hg
ext1 x
no goals
case h.e'_3.h.e'_3.H
α : Type u_2
β : Type u_1
γ : Type ?u.1033801
δ : Type ?u.1033804
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
x : α
⊢ ↑(eapprox (f ∘ g) n) x = ↑(comp (eapprox f n) g hg) x
simp only [eapprox_comp hf hg, coe_comp]