[GOAL]
r : ℝ
hr : r < 0
⊢ sign r = -1
[PROOFSTEP]
rw [sign, if_pos hr]
[GOAL]
r : ℝ
hr : 0 < r
⊢ sign r = 1
[PROOFSTEP]
rw [sign, if_pos hr, if_neg hr.not_lt]
[GOAL]
⊢ sign 0 = 0
[PROOFSTEP]
rw [sign, if_neg (lt_irrefl _), if_neg (lt_irrefl _)]
[GOAL]
⊢ 0 < 1
[PROOFSTEP]
norm_num
[GOAL]
r : ℝ
⊢ sign r = -1 ∨ sign r = 0 ∨ sign r = 1
[PROOFSTEP]
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
[GOAL]
case inl
r : ℝ
hn : r < 0
⊢ sign r = -1 ∨ sign r = 0 ∨ sign r = 1
[PROOFSTEP]
exact Or.inl <| sign_of_neg hn
[GOAL]
case inr.inl
⊢ sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1
[PROOFSTEP]
exact Or.inr <| Or.inl <| sign_zero
[GOAL]
case inr.inr
r : ℝ
hp : 0 < r
⊢ sign r = -1 ∨ sign r = 0 ∨ sign r = 1
[PROOFSTEP]
exact Or.inr <| Or.inr <| sign_of_pos hp
[GOAL]
r : ℝ
⊢ sign r = 0 ↔ r = 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.symm ▸ sign_zero⟩
[GOAL]
r : ℝ
h : sign r = 0
⊢ r = 0
[PROOFSTEP]
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
[GOAL]
case inl
r : ℝ
h : sign r = 0
hn : r < 0
⊢ r = 0
[PROOFSTEP]
rw [sign_of_neg hn, neg_eq_zero] at h 
[GOAL]
case inl
r : ℝ
h : 1 = 0
hn : r < 0
⊢ r = 0
[PROOFSTEP]
exact (one_ne_zero h).elim
[GOAL]
case inr.inl
h : sign 0 = 0
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
r : ℝ
h : sign r = 0
hp : 0 < r
⊢ r = 0
[PROOFSTEP]
rw [sign_of_pos hp] at h 
[GOAL]
case inr.inr
r : ℝ
h : 1 = 0
hp : 0 < r
⊢ r = 0
[PROOFSTEP]
exact (one_ne_zero h).elim
[GOAL]
z : ℤ
⊢ sign ↑z = ↑(Int.sign z)
[PROOFSTEP]
obtain hn | rfl | hp := lt_trichotomy z (0 : ℤ)
[GOAL]
case inl
z : ℤ
hn : z < 0
⊢ sign ↑z = ↑(Int.sign z)
[PROOFSTEP]
rw [sign_of_neg (Int.cast_lt_zero.mpr hn), Int.sign_eq_neg_one_of_neg hn, Int.cast_neg, Int.cast_one]
[GOAL]
case inr.inl
⊢ sign ↑0 = ↑(Int.sign 0)
[PROOFSTEP]
rw [Int.cast_zero, sign_zero, Int.sign_zero, Int.cast_zero]
[GOAL]
case inr.inr
z : ℤ
hp : 0 < z
⊢ sign ↑z = ↑(Int.sign z)
[PROOFSTEP]
rw [sign_of_pos (Int.cast_pos.mpr hp), Int.sign_eq_one_of_pos hp, Int.cast_one]
[GOAL]
r : ℝ
⊢ sign (-r) = -sign r
[PROOFSTEP]
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
[GOAL]
case inl
r : ℝ
hn : r < 0
⊢ sign (-r) = -sign r
[PROOFSTEP]
rw [sign_of_neg hn, sign_of_pos (neg_pos.mpr hn), neg_neg]
[GOAL]
case inr.inl
⊢ sign (-0) = -sign 0
[PROOFSTEP]
rw [sign_zero, neg_zero, sign_zero]
[GOAL]
case inr.inr
r : ℝ
hp : 0 < r
⊢ sign (-r) = -sign r
[PROOFSTEP]
rw [sign_of_pos hp, sign_of_neg (neg_lt_zero.mpr hp)]
[GOAL]
r : ℝ
⊢ 0 ≤ sign r * r
[PROOFSTEP]
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
[GOAL]
case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ sign r * r
[PROOFSTEP]
rw [sign_of_neg hn]
[GOAL]
case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ -1 * r
[PROOFSTEP]
exact mul_nonneg_of_nonpos_of_nonpos (by norm_num) hn.le
[GOAL]
r : ℝ
hn : r < 0
⊢ -1 ≤ 0
[PROOFSTEP]
norm_num
[GOAL]
case inr.inl
⊢ 0 ≤ sign 0 * 0
[PROOFSTEP]
rw [mul_zero]
[GOAL]
case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ sign r * r
[PROOFSTEP]
rw [sign_of_pos hp, one_mul]
[GOAL]
case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r
[PROOFSTEP]
exact hp.le
[GOAL]
r : ℝ
hr : r ≠ 0
⊢ 0 < sign r * r
[PROOFSTEP]
refine' lt_of_le_of_ne (sign_mul_nonneg r) fun h => hr _
[GOAL]
r : ℝ
hr : r ≠ 0
h : 0 = sign r * r
⊢ r = 0
[PROOFSTEP]
have hs0 := (zero_eq_mul.mp h).resolve_right hr
[GOAL]
r : ℝ
hr : r ≠ 0
h : 0 = sign r * r
hs0 : sign r = 0
⊢ r = 0
[PROOFSTEP]
exact sign_eq_zero_iff.mp hs0
[GOAL]
r : ℝ
⊢ (sign r)⁻¹ = sign r
[PROOFSTEP]
obtain hn | hz | hp := sign_apply_eq r
[GOAL]
case inl
r : ℝ
hn : sign r = -1
⊢ (sign r)⁻¹ = sign r
[PROOFSTEP]
rw [hn]
[GOAL]
case inl
r : ℝ
hn : sign r = -1
⊢ (-1)⁻¹ = -1
[PROOFSTEP]
norm_num
[GOAL]
case inr.inl
r : ℝ
hz : sign r = 0
⊢ (sign r)⁻¹ = sign r
[PROOFSTEP]
rw [hz]
[GOAL]
case inr.inl
r : ℝ
hz : sign r = 0
⊢ 0⁻¹ = 0
[PROOFSTEP]
exact inv_zero
[GOAL]
case inr.inr
r : ℝ
hp : sign r = 1
⊢ (sign r)⁻¹ = sign r
[PROOFSTEP]
rw [hp]
[GOAL]
case inr.inr
r : ℝ
hp : sign r = 1
⊢ 1⁻¹ = 1
[PROOFSTEP]
exact inv_one
[GOAL]
r : ℝ
⊢ sign r⁻¹ = sign r
[PROOFSTEP]
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
[GOAL]
case inl
r : ℝ
hn : r < 0
⊢ sign r⁻¹ = sign r
[PROOFSTEP]
rw [sign_of_neg hn, sign_of_neg (inv_lt_zero.mpr hn)]
[GOAL]
case inr.inl
⊢ sign 0⁻¹ = sign 0
[PROOFSTEP]
rw [sign_zero, inv_zero, sign_zero]
[GOAL]
case inr.inr
r : ℝ
hp : 0 < r
⊢ sign r⁻¹ = sign r
[PROOFSTEP]
rw [sign_of_pos hp, sign_of_pos (inv_pos.mpr hp)]
