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

State before:
m n k : Nat
⊢ (m ⊖ n) + ofNat k = m + k ⊖ n
Tactic:
induction m, n with
| zero_zero => rw [zero_mk_zero, Int.zero_add, Nat.zero_add, mk_zero]
| zero_succ n => rw [zero_mk_succ, Nat.zero_add]; rfl
| succ_zero m => rw [succ_mk_zero, mk_zero]; rfl
| succ_succ m n ih => rw [succ_mk_succ, Nat.succ_add, succ_mk_succ, ih]
State after:
no goals

State before:
case zero_zero
k : Nat
⊢ (0 ⊖ 0) + ofNat k = 0 + k ⊖ 0
Tactic:
rw [zero_mk_zero, Int.zero_add, Nat.zero_add, mk_zero]
State after:
no goals

State before:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) + ofNat k = 0 + k ⊖ n
⊢ (0 ⊖ n + 1) + ofNat k = 0 + k ⊖ n + 1
Tactic:
rw [zero_mk_succ, Nat.zero_add]
State after:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) + ofNat k = 0 + k ⊖ n
⊢ -[n+1] + ofNat k = k ⊖ n + 1

State before:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) + ofNat k = 0 + k ⊖ n
⊢ -[n+1] + ofNat k = k ⊖ n + 1
Tactic:
rfl
State after:
no goals

State before:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) + ofNat k = m + k ⊖ 0
⊢ (m + 1 ⊖ 0) + ofNat k = m + 1 + k ⊖ 0
Tactic:
rw [succ_mk_zero, mk_zero]
State after:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) + ofNat k = m + k ⊖ 0
⊢ ofNat (m + 1) + ofNat k = ofNat (m + 1 + k)

State before:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) + ofNat k = m + k ⊖ 0
⊢ ofNat (m + 1) + ofNat k = ofNat (m + 1 + k)
Tactic:
rfl
State after:
no goals

State before:
case succ_succ
k m n : Nat
ih : (m ⊖ n) + ofNat k = m + k ⊖ n
⊢ (m + 1 ⊖ n + 1) + ofNat k = m + 1 + k ⊖ n + 1
Tactic:
rw [succ_mk_succ, Nat.succ_add, succ_mk_succ, ih]
State after:
no goals