r : ℝ
h : sign r = 0
⊢ r = 0
r : ℝ
⊢ sign r = 0 ↔ r = 0
refine' ⟨fun h => _, fun h => h.symm ▸ sign_zero⟩
case inl
r : ℝ
h : sign r = 0
hn : r < 0
⊢ r = 0

case inr.inl
h : sign 0 = 0
⊢ 0 = 0

case inr.inr
r : ℝ
h : sign r = 0
hp : 0 < r
⊢ r = 0
r : ℝ
h : sign r = 0
⊢ r = 0
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
case inl
r : ℝ
h : 1 = 0
hn : r < 0
⊢ r = 0
case inl
r : ℝ
h : sign r = 0
hn : r < 0
⊢ r = 0
rw [sign_of_neg hn, neg_eq_zero] at h
no goals
case inl
r : ℝ
h : 1 = 0
hn : r < 0
⊢ r = 0
exact (one_ne_zero h).elim
no goals
case inr.inl
h : sign 0 = 0
⊢ 0 = 0
rfl
case inr.inr
r : ℝ
h : 1 = 0
hp : 0 < r
⊢ r = 0
case inr.inr
r : ℝ
h : sign r = 0
hp : 0 < r
⊢ r = 0
rw [sign_of_pos hp] at h
no goals
case inr.inr
r : ℝ
h : 1 = 0
hp : 0 < r
⊢ r = 0
exact (one_ne_zero h).elim