α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
⊢ (⨆ (g_1 : β →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f a), SimpleFunc.lintegral g_1 (Measure.map g μ)) =
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f (g a)), SimpleFunc.lintegral g_1 μ
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
⊢ (∫⁻ (a : β), f a ∂Measure.map g μ) = ∫⁻ (a : α), f (g a) ∂μ
rw [lintegral, lintegral]
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ↑f₀ ≤ fun a => f a
⊢ SimpleFunc.lintegral f₀ (Measure.map g μ) ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f (g a)), SimpleFunc.lintegral g_1 μ

case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : α →ₛ ℝ≥0∞
hf₀ : ↑f₀ ≤ fun a => f (g a)
⊢ SimpleFunc.lintegral f₀ μ ≤ ⨆ (g_1 : β →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f a), SimpleFunc.lintegral g_1 (Measure.map g μ)
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
⊢ (⨆ (g_1 : β →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f a), SimpleFunc.lintegral g_1 (Measure.map g μ)) =
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f (g a)), SimpleFunc.lintegral g_1 μ
refine' le_antisymm (iSup₂_le fun f₀ hf₀ => _) (iSup₂_le fun f₀ hf₀ => _)
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ↑f₀ ≤ fun a => f a
⊢ SimpleFunc.lintegral (comp f₀ g (_ : Measurable g)) μ ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f (g a)), SimpleFunc.lintegral g_1 μ
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ↑f₀ ≤ fun a => f a
⊢ SimpleFunc.lintegral f₀ (Measure.map g μ) ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f (g a)), SimpleFunc.lintegral g_1 μ
rw [SimpleFunc.lintegral_map _ hg.measurable]
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ↑f₀ ≤ fun a => f a
this : ↑(comp f₀ g (_ : Measurable g)) ≤ f ∘ g
⊢ SimpleFunc.lintegral (comp f₀ g (_ : Measurable g)) μ ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f (g a)), SimpleFunc.lintegral g_1 μ
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ↑f₀ ≤ fun a => f a
⊢ SimpleFunc.lintegral (comp f₀ g (_ : Measurable g)) μ ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f (g a)), SimpleFunc.lintegral g_1 μ
have : (f₀.comp g hg.measurable : α → ℝ≥0∞) ≤ f ∘ g := fun x => hf₀ (g x)
no goals
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ↑f₀ ≤ fun a => f a
this : ↑(comp f₀ g (_ : Measurable g)) ≤ f ∘ g
⊢ SimpleFunc.lintegral (comp f₀ g (_ : Measurable g)) μ ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f (g a)), SimpleFunc.lintegral g_1 μ
exact le_iSup_of_le (comp f₀ g hg.measurable) (by exact le_iSup (α := ℝ≥0∞) _ this)
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ↑f₀ ≤ fun a => f a
this : ↑(comp f₀ g (_ : Measurable g)) ≤ f ∘ g
⊢ SimpleFunc.lintegral (comp f₀ g (_ : Measurable g)) μ ≤
    ⨆ (_ : ↑(comp f₀ g (_ : Measurable g)) ≤ fun a => f (g a)), SimpleFunc.lintegral (comp f₀ g (_ : Measurable g)) μ
exact le_iSup (α := ℝ≥0∞) _ this
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : α →ₛ ℝ≥0∞
hf₀ : ↑f₀ ≤ fun a => f (g a)
⊢ (∫⁻ (a : β), ↑(SimpleFunc.extend f₀ g hg (const β 0)) a ∂Measure.map g μ) ≤ ∫⁻ (a : β), f a ∂Measure.map g μ
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : α →ₛ ℝ≥0∞
hf₀ : ↑f₀ ≤ fun a => f (g a)
⊢ SimpleFunc.lintegral f₀ μ ≤ ⨆ (g_1 : β →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f a), SimpleFunc.lintegral g_1 (Measure.map g μ)
rw [← f₀.extend_comp_eq hg (const _ 0), ← SimpleFunc.lintegral_map, ←
  SimpleFunc.lintegral_eq_lintegral, ← lintegral]
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : α →ₛ ℝ≥0∞
hf₀ : ↑f₀ ≤ fun a => f (g a)
x : α
⊢ ↑(SimpleFunc.extend f₀ g hg (const β 0)) (g x) ≤ f (g x)
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : α →ₛ ℝ≥0∞
hf₀ : ↑f₀ ≤ fun a => f (g a)
⊢ (∫⁻ (a : β), ↑(SimpleFunc.extend f₀ g hg (const β 0)) a ∂Measure.map g μ) ≤ ∫⁻ (a : β), f a ∂Measure.map g μ
refine' lintegral_mono_ae (hg.ae_map_iff.2 <| eventually_of_forall fun x => _)
no goals
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1366326
δ : Type ?u.1366329
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : α →ₛ ℝ≥0∞
hf₀ : ↑f₀ ≤ fun a => f (g a)
x : α
⊢ ↑(SimpleFunc.extend f₀ g hg (const β 0)) (g x) ≤ f (g x)
exact (extend_apply _ _ _ _).trans_le (hf₀ _)