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

State before:
k m n : Nat
⊢ k + m ⊖ k + n = m ⊖ n
Tactic:
induction k with
| zero => rw [Nat.zero_add, Nat.zero_add]
| succ k ih => rw [Nat.succ_add, Nat.succ_add, succ_mk_succ]; exact ih
State after:
no goals

State before:
case zero
m n : Nat
⊢ 0 + m ⊖ 0 + n = m ⊖ n
Tactic:
rw [Nat.zero_add, Nat.zero_add]
State after:
no goals

State before:
case succ
m n k : Nat
ih : k + m ⊖ k + n = m ⊖ n
⊢ k + 1 + m ⊖ k + 1 + n = m ⊖ n
Tactic:
rw [Nat.succ_add, Nat.succ_add, succ_mk_succ]
State after:
case succ
m n k : Nat
ih : k + m ⊖ k + n = m ⊖ n
⊢ k + m ⊖ k + n = m ⊖ n

State before:
case succ
m n k : Nat
ih : k + m ⊖ k + n = m ⊖ n
⊢ k + m ⊖ k + n = m ⊖ n
Tactic:
exact ih
State after:
no goals