Theorem: Int.add_neg_self_left (Extra/Int/Lemmas.lean)

State before:
i : Int
⊢ -i + i = 0
Tactic:
cases i using Int.casesMkOn with
| mk mi ni => rw [neg_mk, mk_add_mk, Nat.add_comm mi ni, mk_self]
State after:
no goals

State before:
case mk
mi ni : Nat
⊢ -(mi ⊖ ni) + (mi ⊖ ni) = 0
Tactic:
rw [neg_mk, mk_add_mk, Nat.add_comm mi ni, mk_self]
State after:
no goals