no goals
α : Type u_1
β : Type ?u.12757
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : 0 ≤ r
⊢ (r • j).negPart = Real.toNNReal r • j.negPart
rw [real_smul_def, ← smul_negPart, if_pos hr]