α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
h : ↑sign a = -1
⊢ a < 0
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
⊢ ↑sign a = -1 ↔ a < 0
refine' ⟨fun h => _, fun h => sign_neg h⟩
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = -1
⊢ a < 0
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
h : ↑sign a = -1
⊢ a < 0
rw [sign_apply] at h
case inr.inl
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
h✝¹ : ¬0 < a
h✝ : a < 0
h : -1 = -1
⊢ a < 0
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = -1
⊢ a < 0
split_ifs at h
no goals
case inr.inl
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
h✝¹ : ¬0 < a
h✝ : a < 0
h : -1 = -1
⊢ a < 0
assumption