case inl
r : ℝ
hn : r < 0
⊢ sign (-r) = -sign r

case inr.inl

⊢ sign (-0) = -sign 0

case inr.inr
r : ℝ
hp : 0 < r
⊢ sign (-r) = -sign r
r : ℝ
⊢ sign (-r) = -sign r
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
no goals
case inl
r : ℝ
hn : r < 0
⊢ sign (-r) = -sign r
rw [sign_of_neg hn, sign_of_pos (neg_pos.mpr hn), neg_neg]
no goals
case inr.inl

⊢ sign (-0) = -sign 0
rw [sign_zero, neg_zero, sign_zero]
no goals
case inr.inr
r : ℝ
hp : 0 < r
⊢ sign (-r) = -sign r
rw [sign_of_pos hp, sign_of_neg (neg_lt_zero.mpr hp)]