no goals
α : Type u_1
β : Type ?u.15046
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
⊢ (r • j).negPart = Real.toNNReal (-r) • j.posPart
rw [real_smul_def, ← smul_posPart, if_neg (not_le.2 hr), neg_negPart]