case inl
r : ℝ
hn : sign r = -1
⊢ (sign r)⁻¹ = sign r

case inr.inl
r : ℝ
hz : sign r = 0
⊢ (sign r)⁻¹ = sign r

case inr.inr
r : ℝ
hp : sign r = 1
⊢ (sign r)⁻¹ = sign r
r : ℝ
⊢ (sign r)⁻¹ = sign r
obtain hn | hz | hp := sign_apply_eq r
case inl
r : ℝ
hn : sign r = -1
⊢ (-1)⁻¹ = -1
case inl
r : ℝ
hn : sign r = -1
⊢ (sign r)⁻¹ = sign r
rw [hn]
no goals
case inl
r : ℝ
hn : sign r = -1
⊢ (-1)⁻¹ = -1
norm_num
case inr.inl
r : ℝ
hz : sign r = 0
⊢ 0⁻¹ = 0
case inr.inl
r : ℝ
hz : sign r = 0
⊢ (sign r)⁻¹ = sign r
rw [hz]
no goals
case inr.inl
r : ℝ
hz : sign r = 0
⊢ 0⁻¹ = 0
exact inv_zero
case inr.inr
r : ℝ
hp : sign r = 1
⊢ 1⁻¹ = 1
case inr.inr
r : ℝ
hp : sign r = 1
⊢ (sign r)⁻¹ = sign r
rw [hp]
no goals
case inr.inr
r : ℝ
hp : sign r = 1
⊢ 1⁻¹ = 1
exact inv_one