no goals
α : Type u_1
β : Type ?u.962296
γ : Type ?u.962299
δ : Type ?u.962302
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
ε : ℝ≥0∞
⊢ ε * ↑↑μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ
simpa only [lintegral_zero, zero_add] using
  lintegral_add_mul_meas_add_le_le_lintegral (ae_of_all _ fun x => zero_le (f x)) hf ε