no goals
α : Type u_1
E : Type ?u.8096866
F : Type ?u.8096869
G : Type ?u.8096872
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
f : { x // x ∈ Lp ℝ p }
a : α
h : ↑↑(negPart f) a = max (-↑↑f a) 0
⊢ ↑↑(negPart f) a = -min (↑↑f a) 0
rw [h, ← max_neg_neg, neg_zero]