r : ℝ
hr : r ≠ 0
h : 0 = sign r * r
⊢ r = 0
r : ℝ
hr : r ≠ 0
⊢ 0 < sign r * r
refine' lt_of_le_of_ne (sign_mul_nonneg r) fun h => hr _
r : ℝ
hr : r ≠ 0
h : 0 = sign r * r
hs0 : sign r = 0
⊢ r = 0
r : ℝ
hr : r ≠ 0
h : 0 = sign r * r
⊢ r = 0
have hs0 := (zero_eq_mul.mp h).resolve_right hr
no goals
r : ℝ
hr : r ≠ 0
h : 0 = sign r * r
hs0 : sign r = 0
⊢ r = 0
exact sign_eq_zero_iff.mp hs0