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