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

State before:
m n k : Nat
⊢ (m ⊖ n) * ofNat k = m * k ⊖ n * k
Tactic:
induction m, n with
| zero_zero => rw [Nat.zero_mul, zero_mk_zero, Int.zero_mul]
| zero_succ n => rw [Nat.zero_mul, zero_mk, zero_mk]; rfl
| succ_zero m => rw [Nat.zero_mul, mk_zero, mk_zero]; rfl
| succ_succ m n ih => rw [Nat.succ_mul, Nat.succ_mul, succ_mk_succ, add_mk_add_right]; exact ih
State after:
no goals

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

State before:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) * ofNat k = 0 * k ⊖ n * k
⊢ (0 ⊖ n + 1) * ofNat k = 0 * k ⊖ (n + 1) * k
Tactic:
rw [Nat.zero_mul, zero_mk, zero_mk]
State after:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) * ofNat k = 0 * k ⊖ n * k
⊢ negOfNat (n + 1) * ofNat k = negOfNat ((n + 1) * k)

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

State before:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) * ofNat k = m * k ⊖ 0 * k
⊢ (m + 1 ⊖ 0) * ofNat k = (m + 1) * k ⊖ 0 * k
Tactic:
rw [Nat.zero_mul, mk_zero, mk_zero]
State after:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) * ofNat k = m * k ⊖ 0 * k
⊢ 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 * k
⊢ 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 * k
⊢ (m + 1 ⊖ n + 1) * ofNat k = (m + 1) * k ⊖ (n + 1) * k
Tactic:
rw [Nat.succ_mul, Nat.succ_mul, succ_mk_succ, add_mk_add_right]
State after:
case succ_succ
k m n : Nat
ih : (m ⊖ n) * ofNat k = m * k ⊖ n * k
⊢ (m ⊖ n) * ofNat k = m * k ⊖ n * k

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