case inl
z : ℤ
hn : z < 0
⊢ sign ↑z = ↑(Int.sign z)

case inr.inl

⊢ sign ↑0 = ↑(Int.sign 0)

case inr.inr
z : ℤ
hp : 0 < z
⊢ sign ↑z = ↑(Int.sign z)
z : ℤ
⊢ sign ↑z = ↑(Int.sign z)
obtain hn | rfl | hp := lt_trichotomy z (0 : ℤ)
no goals
case inl
z : ℤ
hn : z < 0
⊢ sign ↑z = ↑(Int.sign z)
rw [sign_of_neg (Int.cast_lt_zero.mpr hn), Int.sign_eq_neg_one_of_neg hn, Int.cast_neg,
  Int.cast_one]
no goals
case inr.inl

⊢ sign ↑0 = ↑(Int.sign 0)
rw [Int.cast_zero, sign_zero, Int.sign_zero, Int.cast_zero]
no goals
case inr.inr
z : ℤ
hp : 0 < z
⊢ sign ↑z = ↑(Int.sign z)
rw [sign_of_pos (Int.cast_pos.mpr hp), Int.sign_eq_one_of_pos hp, Int.cast_one]