case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ sign r * r

case inr.inl

⊢ 0 ≤ sign 0 * 0

case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ sign r * r
r : ℝ
⊢ 0 ≤ sign r * r
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ -1 * r
case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ sign r * r
rw [sign_of_neg hn]
no goals
case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ -1 * r
exact mul_nonneg_of_nonpos_of_nonpos (by norm_num) hn.le
no goals
r : ℝ
hn : r < 0
⊢ -1 ≤ 0
norm_num
no goals
case inr.inl

⊢ 0 ≤ sign 0 * 0
rw [mul_zero]
case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r
case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ sign r * r
rw [sign_of_pos hp, one_mul]
no goals
case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r
exact hp.le