case inl
r : ℝ
hn : r < 0
⊢ sign r = -1 ∨ sign r = 0 ∨ sign r = 1

case inr.inl

⊢ sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1

case inr.inr
r : ℝ
hp : 0 < r
⊢ sign r = -1 ∨ sign r = 0 ∨ sign r = 1
r : ℝ
⊢ sign r = -1 ∨ sign r = 0 ∨ sign r = 1
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
no goals
case inl
r : ℝ
hn : r < 0
⊢ sign r = -1 ∨ sign r = 0 ∨ sign r = 1
exact Or.inl <| sign_of_neg hn
no goals
case inr.inl

⊢ sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1
exact Or.inr <| Or.inl <| sign_zero
no goals
case inr.inr
r : ℝ
hp : 0 < r
⊢ sign r = -1 ∨ sign r = 0 ∨ sign r = 1
exact Or.inr <| Or.inr <| sign_of_pos hp