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

State before:
m₁ n₁ m₂ n₂ : Nat
⊢ (m₁ ⊖ n₁) + (m₂ ⊖ n₂) = m₁ + m₂ ⊖ n₁ + n₂
Tactic:
induction m₂, n₂ with
| zero_zero => rw [zero_mk_zero, Int.add_zero, Nat.add_zero, Nat.add_zero]
| zero_succ n₂ => rw [zero_mk_succ, Nat.add_succ, mk_add_negSucc]; rfl
| succ_zero m₂ => rw [mk_zero, mk_add_ofNat]; rfl
| succ_succ m₂ n₂ ih => rw [succ_mk_succ, Nat.add_succ m₁ m₂, Nat.add_succ n₁ n₂, succ_mk_succ]; exact ih
State after:
no goals

State before:
case zero_zero
m₁ n₁ : Nat
⊢ (m₁ ⊖ n₁) + (0 ⊖ 0) = m₁ + 0 ⊖ n₁ + 0
Tactic:
rw [zero_mk_zero, Int.add_zero, Nat.add_zero, Nat.add_zero]
State after:
no goals

State before:
case zero_succ
m₁ n₁ n₂ : Nat
a✝ : (m₁ ⊖ n₁) + (0 ⊖ n₂) = m₁ + 0 ⊖ n₁ + n₂
⊢ (m₁ ⊖ n₁) + (0 ⊖ n₂ + 1) = m₁ + 0 ⊖ n₁ + (n₂ + 1)
Tactic:
rw [zero_mk_succ, Nat.add_succ, mk_add_negSucc]
State after:
case zero_succ
m₁ n₁ n₂ : Nat
a✝ : (m₁ ⊖ n₁) + (0 ⊖ n₂) = m₁ + 0 ⊖ n₁ + n₂
⊢ m₁ ⊖ n₁ + n₂ + 1 = m₁ + 0 ⊖ (n₁ + n₂).succ

State before:
case zero_succ
m₁ n₁ n₂ : Nat
a✝ : (m₁ ⊖ n₁) + (0 ⊖ n₂) = m₁ + 0 ⊖ n₁ + n₂
⊢ m₁ ⊖ n₁ + n₂ + 1 = m₁ + 0 ⊖ (n₁ + n₂).succ
Tactic:
rfl
State after:
no goals

State before:
case succ_zero
m₁ n₁ m₂ : Nat
a✝ : (m₁ ⊖ n₁) + (m₂ ⊖ 0) = m₁ + m₂ ⊖ n₁ + 0
⊢ (m₁ ⊖ n₁) + (m₂ + 1 ⊖ 0) = m₁ + (m₂ + 1) ⊖ n₁ + 0
Tactic:
rw [mk_zero, mk_add_ofNat]
State after:
case succ_zero
m₁ n₁ m₂ : Nat
a✝ : (m₁ ⊖ n₁) + (m₂ ⊖ 0) = m₁ + m₂ ⊖ n₁ + 0
⊢ m₁ + (m₂ + 1) ⊖ n₁ = m₁ + (m₂ + 1) ⊖ n₁ + 0

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

State before:
case succ_succ
m₁ n₁ m₂ n₂ : Nat
ih : (m₁ ⊖ n₁) + (m₂ ⊖ n₂) = m₁ + m₂ ⊖ n₁ + n₂
⊢ (m₁ ⊖ n₁) + (m₂ + 1 ⊖ n₂ + 1) = m₁ + (m₂ + 1) ⊖ n₁ + (n₂ + 1)
Tactic:
rw [succ_mk_succ, Nat.add_succ m₁ m₂, Nat.add_succ n₁ n₂, succ_mk_succ]
State after:
case succ_succ
m₁ n₁ m₂ n₂ : Nat
ih : (m₁ ⊖ n₁) + (m₂ ⊖ n₂) = m₁ + m₂ ⊖ n₁ + n₂
⊢ (m₁ ⊖ n₁) + (m₂ ⊖ n₂) = m₁ + m₂ ⊖ n₁ + n₂

State before:
case succ_succ
m₁ n₁ m₂ n₂ : Nat
ih : (m₁ ⊖ n₁) + (m₂ ⊖ n₂) = m₁ + m₂ ⊖ n₁ + n₂
⊢ (m₁ ⊖ n₁) + (m₂ ⊖ n₂) = m₁ + m₂ ⊖ n₁ + n₂
Tactic:
exact ih
State after:
no goals