α : Type u_1
β : Type ?u.297696
E : Type ?u.297699
F : Type ?u.297702
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
s✝ s : Set α
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f
⊢ (∫ (x : α), indicator {a | f a ≤ 0} (fun x => f x) x ∂μ) ≤ ∫ (x : α), indicator s (fun x => f x) x ∂μ
α : Type u_1
β : Type ?u.297696
E : Type ?u.297699
F : Type ?u.297702
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
s✝ s : Set α
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f
⊢ (∫ (x : α) in {y | f y ≤ 0}, f x ∂μ) ≤ ∫ (x : α) in s, f x ∂μ
rw [← integral_indicator hs, ←
  integral_indicator (hf.measurableSet_le stronglyMeasurable_const)]
no goals
α : Type u_1
β : Type ?u.297696
E : Type ?u.297699
F : Type ?u.297702
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
s✝ s : Set α
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f
⊢ (∫ (x : α), indicator {a | f a ≤ 0} (fun x => f x) x ∂μ) ≤ ∫ (x : α), indicator s (fun x => f x) x ∂μ
exact
  integral_mono (hfi.indicator (hf.measurableSet_le stronglyMeasurable_const))
    (hfi.indicator hs) (indicator_nonpos_le_indicator s f)