α : Type u_1
β : Type ?u.1805192
γ : Type ?u.1805195
δ : Type ?u.1805198
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
⊢ (⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => g a), ∫⁻ (a : α), g_1 a ∂Measure.withDensity μ f) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => (f * g) a), ∫⁻ (a : α), g_1 a ∂μ
α : Type u_1
β : Type ?u.1805192
γ : Type ?u.1805195
δ : Type ?u.1805198
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f) ≤ ∫⁻ (a : α), (f * g) a ∂μ
rw [← iSup_lintegral_measurable_le_eq_lintegral, ← iSup_lintegral_measurable_le_eq_lintegral]
α : Type u_1
β : Type ?u.1805192
γ : Type ?u.1805195
δ : Type ?u.1805198
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => g a
⊢ (∫⁻ (a : α), i a ∂Measure.withDensity μ f) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => (f * g) a), ∫⁻ (a : α), g_1 a ∂μ
α : Type u_1
β : Type ?u.1805192
γ : Type ?u.1805195
δ : Type ?u.1805198
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
⊢ (⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => g a), ∫⁻ (a : α), g_1 a ∂Measure.withDensity μ f) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => (f * g) a), ∫⁻ (a : α), g_1 a ∂μ
refine' iSup₂_le fun i i_meas => iSup_le fun hi => _
α : Type u_1
β : Type ?u.1805192
γ : Type ?u.1805195
δ : Type ?u.1805198
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => g a
A : f * i ≤ f * g
⊢ (∫⁻ (a : α), i a ∂Measure.withDensity μ f) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => (f * g) a), ∫⁻ (a : α), g_1 a ∂μ
α : Type u_1
β : Type ?u.1805192
γ : Type ?u.1805195
δ : Type ?u.1805198
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => g a
⊢ (∫⁻ (a : α), i a ∂Measure.withDensity μ f) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => (f * g) a), ∫⁻ (a : α), g_1 a ∂μ
have A : f * i ≤ f * g := fun x => mul_le_mul_left' (hi x) _
α : Type u_1
β : Type ?u.1805192
γ : Type ?u.1805195
δ : Type ?u.1805198
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => g a
A : f * i ≤ f * g
⊢ (∫⁻ (a : α), i a ∂Measure.withDensity μ f) ≤ ⨆ (_ : f * i ≤ fun a => (f * g) a), ∫⁻ (a : α), (f * i) a ∂μ
α : Type u_1
β : Type ?u.1805192
γ : Type ?u.1805195
δ : Type ?u.1805198
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => g a
A : f * i ≤ f * g
⊢ (∫⁻ (a : α), i a ∂Measure.withDensity μ f) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => (f * g) a), ∫⁻ (a : α), g_1 a ∂μ
refine' le_iSup₂_of_le (f * i) (f_meas.mul i_meas) _
no goals
α : Type u_1
β : Type ?u.1805192
γ : Type ?u.1805195
δ : Type ?u.1805198
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => g a
A : f * i ≤ f * g
⊢ (∫⁻ (a : α), i a ∂Measure.withDensity μ f) ≤ ⨆ (_ : f * i ≤ fun a => (f * g) a), ∫⁻ (a : α), (f * i) a ∂μ
exact le_iSup_of_le A (le_of_eq (lintegral_withDensity_eq_lintegral_mul _ f_meas i_meas))