no goals
α : Type u_1
β : Type ?u.746780
γ : Type ?u.746783
δ : Type ?u.746786
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : HasFiniteIntegral f
x : α
⊢ ‖max (f x) 0‖ ≤ ‖f x‖
simp [abs_le, le_abs_self]