α : Type u_2
β : Type u_1
γ : Type ?u.1150567
δ : Type ?u.1150570
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
⊢ (⨆ (g_1 : β → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => f a), ∫⁻ (a : β), g_1 a ∂Measure.map g μ) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => f (g a)), ∫⁻ (a : α), g_1 a ∂μ
α : Type u_2
β : Type u_1
γ : Type ?u.1150567
δ : Type ?u.1150570
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
⊢ (∫⁻ (a : β), f a ∂Measure.map g μ) ≤ ∫⁻ (a : α), f (g a) ∂μ
rw [← iSup_lintegral_measurable_le_eq_lintegral, ← iSup_lintegral_measurable_le_eq_lintegral]
α : Type u_2
β : Type u_1
γ : Type ?u.1150567
δ : Type ?u.1150570
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
i : β → ℝ≥0∞
hi : Measurable i
h'i : i ≤ fun a => f a
⊢ (∫⁻ (a : β), i a ∂Measure.map g μ) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => f (g a)), ∫⁻ (a : α), g_1 a ∂μ
α : Type u_2
β : Type u_1
γ : Type ?u.1150567
δ : Type ?u.1150570
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
⊢ (⨆ (g_1 : β → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => f a), ∫⁻ (a : β), g_1 a ∂Measure.map g μ) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => f (g a)), ∫⁻ (a : α), g_1 a ∂μ
refine' iSup₂_le fun i hi => iSup_le fun h'i => _
α : Type u_2
β : Type u_1
γ : Type ?u.1150567
δ : Type ?u.1150570
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
i : β → ℝ≥0∞
hi : Measurable i
h'i : i ≤ fun a => f a
⊢ (∫⁻ (a : β), i a ∂Measure.map g μ) ≤ ⨆ (_ : i ∘ g ≤ fun a => f (g a)), ∫⁻ (a : α), (i ∘ g) a ∂μ
α : Type u_2
β : Type u_1
γ : Type ?u.1150567
δ : Type ?u.1150570
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
i : β → ℝ≥0∞
hi : Measurable i
h'i : i ≤ fun a => f a
⊢ (∫⁻ (a : β), i a ∂Measure.map g μ) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => f (g a)), ∫⁻ (a : α), g_1 a ∂μ
refine' le_iSup₂_of_le (i ∘ g) (hi.comp hg) _
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1150567
δ : Type ?u.1150570
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hg : Measurable g
i : β → ℝ≥0∞
hi : Measurable i
h'i : i ≤ fun a => f a
⊢ (∫⁻ (a : β), i a ∂Measure.map g μ) ≤ ⨆ (_ : i ∘ g ≤ fun a => f (g a)), ∫⁻ (a : α), (i ∘ g) a ∂μ
exact le_iSup_of_le (fun x => h'i (g x)) (le_of_eq (lintegral_map hi hg))