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