cases i with
| ofNat n =>
  { simp [Int.neg]
    cases n
    { simp }
    { simp [Int.negOfNat] } }
| negSucc n =>
  { simp [Int.neg]
    have hnp1 : (↑n + 1 : ℤ) = ↑(n + 1) :=
      by simp
    rw [hnp1]
    rfl }
case h
i : ℤ
⊢ Int.neg (Int.neg i) = i
no goals