α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : ↑sign a = 0
⊢ a = 0
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ ↑sign a = 0 ↔ a = 0
refine' ⟨fun h => _, fun h => h.symm ▸ sign_zero⟩
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = 0
⊢ a = 0
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : ↑sign a = 0
⊢ a = 0
rw [sign_apply] at h
case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
h : 0 = 0
⊢ a = 0
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = 0
⊢ a = 0
split_ifs at h with h_1 h_2
case inr.inr.refl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
⊢ a = 0
case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
h : 0 = 0
⊢ a = 0
cases' h
no goals
case inr.inr.refl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
⊢ a = 0
exact (le_of_not_lt h_1).eq_of_not_lt h_2