case inl
r : ℝ
hn : r < 0
⊢ sign r⁻¹ = sign r

case inr.inl

⊢ sign 0⁻¹ = sign 0

case inr.inr
r : ℝ
hp : 0 < r
⊢ sign r⁻¹ = sign r
r : ℝ
⊢ sign r⁻¹ = sign r
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
no goals
case inl
r : ℝ
hn : r < 0
⊢ sign r⁻¹ = sign r
rw [sign_of_neg hn, sign_of_neg (inv_lt_zero.mpr hn)]
no goals
case inr.inl

⊢ sign 0⁻¹ = sign 0
rw [sign_zero, inv_zero, sign_zero]
no goals
case inr.inr
r : ℝ
hp : 0 < r
⊢ sign r⁻¹ = sign r
rw [sign_of_pos hp, sign_of_pos (inv_pos.mpr hp)]