no goals
α : Type u_2
β : Type u_1
ι : Type ?u.74487
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
⊢ (∫⁻ (x : α), ↑‖Set.indicator {x | max M 0 ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
simpa