α : Type u_1
β : Type ?u.70000
γ : Type ?u.70003
δ : Type ?u.70006
m✝ : MeasurableSpace α
μ✝ ν✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
f g : α → ℝ≥0∞
hfg : f ≤ g
⊢ (⨆ (g : α →ₛ ℝ≥0∞) (_ : ↑g ≤ fun a => f a), SimpleFunc.lintegral g μ) ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => g a), SimpleFunc.lintegral g_1 ν
α : Type u_1
β : Type ?u.70000
γ : Type ?u.70003
δ : Type ?u.70006
m✝ : MeasurableSpace α
μ✝ ν✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
f g : α → ℝ≥0∞
hfg : f ≤ g
⊢ (∫⁻ (a : α), f a ∂μ) ≤ ∫⁻ (a : α), g a ∂ν
rw [lintegral, lintegral]
no goals
α : Type u_1
β : Type ?u.70000
γ : Type ?u.70003
δ : Type ?u.70006
m✝ : MeasurableSpace α
μ✝ ν✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
f g : α → ℝ≥0∞
hfg : f ≤ g
⊢ (⨆ (g : α →ₛ ℝ≥0∞) (_ : ↑g ≤ fun a => f a), SimpleFunc.lintegral g μ) ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => g a), SimpleFunc.lintegral g_1 ν
exact iSup_mono fun φ => iSup_mono' fun hφ => ⟨le_trans hφ hfg, lintegral_mono (le_refl φ) hμν⟩