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

State before:
m₁ n₁ m₂ n₂ : Nat
⊢ (m₁ ⊖ n₁) * (m₂ ⊖ n₂) = m₁ * m₂ + n₁ * n₂ ⊖ m₁ * n₂ + n₁ * m₂
Tactic:
induction m₂, n₂ with
| zero_zero => simp only [Nat.zero_mul, Nat.mul_zero, Nat.add_zero, Nat.zero_add, zero_mk_zero, Int.mul_zero]
| zero_succ n₂ => simp only [Nat.zero_mul, Nat.mul_zero, Nat.add_zero, Nat.zero_add, zero_mk_succ, mk_mul_negSucc]
| succ_zero m₂ => simp only [Nat.zero_mul, Nat.mul_zero, Nat.add_zero, Nat.zero_add, succ_mk_zero, mk_mul_ofNat, Nat.mul_comm]
| succ_succ m₂ n₂ ih => simp only [Nat.mul_succ, Nat.succ_mul]; rw [succ_mk_succ, Nat.add_add_add_comm _ m₁ _ n₁, Nat.add_add_add_comm _ m₁ _ n₁, add_mk_add_right]; exact ih
State after:
no goals

State before:
case zero_zero
m₁ n₁ : Nat
⊢ (m₁ ⊖ n₁) * (0 ⊖ 0) = m₁ * 0 + n₁ * 0 ⊖ m₁ * 0 + n₁ * 0
Tactic:
simp only [Nat.zero_mul, Nat.mul_zero, Nat.add_zero, Nat.zero_add, zero_mk_zero, Int.mul_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₂ + n₁ * 0
⊢ (m₁ ⊖ n₁) * (0 ⊖ n₂ + 1) = m₁ * 0 + n₁ * (n₂ + 1) ⊖ m₁ * (n₂ + 1) + n₁ * 0
Tactic:
simp only [Nat.zero_mul, Nat.mul_zero, Nat.add_zero, Nat.zero_add, zero_mk_succ, mk_mul_negSucc]
State after:
no goals

State before:
case succ_zero
m₁ n₁ m₂ : Nat
a✝ : (m₁ ⊖ n₁) * (m₂ ⊖ 0) = m₁ * m₂ + n₁ * 0 ⊖ m₁ * 0 + n₁ * m₂
⊢ (m₁ ⊖ n₁) * (m₂ + 1 ⊖ 0) = m₁ * (m₂ + 1) + n₁ * 0 ⊖ m₁ * 0 + n₁ * (m₂ + 1)
Tactic:
simp only [Nat.zero_mul, Nat.mul_zero, Nat.add_zero, Nat.zero_add, succ_mk_zero, mk_mul_ofNat, Nat.mul_comm]
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₂ + n₁ * m₂
⊢ (m₁ ⊖ n₁) * (m₂ + 1 ⊖ n₂ + 1) = m₁ * (m₂ + 1) + n₁ * (n₂ + 1) ⊖ m₁ * (n₂ + 1) + n₁ * (m₂ + 1)
Tactic:
simp only [Nat.mul_succ, Nat.succ_mul]
State after:
case succ_succ
m₁ n₁ m₂ n₂ : Nat
ih : (m₁ ⊖ n₁) * (m₂ ⊖ n₂) = m₁ * m₂ + n₁ * n₂ ⊖ m₁ * n₂ + n₁ * m₂
⊢ (m₁ ⊖ n₁) * (m₂ + 1 ⊖ n₂ + 1) = m₁ * m₂ + m₁ + (n₁ * n₂ + n₁) ⊖ m₁ * n₂ + m₁ + (n₁ * m₂ + n₁)

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

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