case a
α : Type u_1
β : Type ?u.71667
γ : Type ?u.71670
δ : Type ?u.71673
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ (⨆ (g : α → ℝ≥0∞) (_ : Measurable g) (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ) ≤ ∫⁻ (a : α), f a ∂μ

case a
α : Type u_1
β : Type ?u.71667
γ : Type ?u.71670
δ : Type ?u.71673
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α), f a ∂μ) ≤ ⨆ (g : α → ℝ≥0∞) (_ : Measurable g) (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ
α : Type u_1
β : Type ?u.71667
γ : Type ?u.71670
δ : Type ?u.71673
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ (⨆ (g : α → ℝ≥0∞) (_ : Measurable g) (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ) = ∫⁻ (a : α), f a ∂μ
apply le_antisymm
no goals
case a
α : Type u_1
β : Type ?u.71667
γ : Type ?u.71670
δ : Type ?u.71673
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ (⨆ (g : α → ℝ≥0∞) (_ : Measurable g) (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ) ≤ ∫⁻ (a : α), f a ∂μ
exact iSup_le fun i => iSup_le fun _ => iSup_le fun h'i => lintegral_mono h'i
case a
α : Type u_1
β : Type ?u.71667
γ : Type ?u.71670
δ : Type ?u.71673
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ (⨆ (g : α →ₛ ℝ≥0∞) (_ : ↑g ≤ fun a => f a), SimpleFunc.lintegral g μ) ≤
    ⨆ (g : α → ℝ≥0∞) (_ : Measurable g) (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ
case a
α : Type u_1
β : Type ?u.71667
γ : Type ?u.71670
δ : Type ?u.71673
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α), f a ∂μ) ≤ ⨆ (g : α → ℝ≥0∞) (_ : Measurable g) (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ
rw [lintegral]
case a
α : Type u_1
β : Type ?u.71667
γ : Type ?u.71670
δ : Type ?u.71673
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
i : α →ₛ ℝ≥0∞
hi : ↑i ≤ fun a => f a
⊢ SimpleFunc.lintegral i μ ≤ ∫⁻ (a : α), ↑i a ∂μ
case a
α : Type u_1
β : Type ?u.71667
γ : Type ?u.71670
δ : Type ?u.71673
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ (⨆ (g : α →ₛ ℝ≥0∞) (_ : ↑g ≤ fun a => f a), SimpleFunc.lintegral g μ) ≤
    ⨆ (g : α → ℝ≥0∞) (_ : Measurable g) (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ
refine' iSup₂_le fun i hi => le_iSup₂_of_le i i.measurable <| le_iSup_of_le hi _
no goals
case a
α : Type u_1
β : Type ?u.71667
γ : Type ?u.71670
δ : Type ?u.71673
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
i : α →ₛ ℝ≥0∞
hi : ↑i ≤ fun a => f a
⊢ SimpleFunc.lintegral i μ ≤ ∫⁻ (a : α), ↑i a ∂μ
exact le_of_eq (i.lintegral_eq_lintegral _).symm