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

State before:
m n k : Nat
⊢ (m ⊖ n) * -[k+1] = n * (k + 1) ⊖ m * (k + 1)
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, mk_zero]; rfl
| succ_zero m => rw [Nat.zero_mul, mk_zero, zero_mk]; 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) * -[k+1] = 0 * (k + 1) ⊖ 0 * (k + 1)
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) * -[k+1] = n * (k + 1) ⊖ 0 * (k + 1)
⊢ (0 ⊖ n + 1) * -[k+1] = (n + 1) * (k + 1) ⊖ 0 * (k + 1)
Tactic:
rw [Nat.zero_mul, zero_mk, mk_zero]
State after:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) * -[k+1] = n * (k + 1) ⊖ 0 * (k + 1)
⊢ negOfNat (n + 1) * -[k+1] = ofNat ((n + 1) * (k + 1))

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

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

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

State before:
case succ_succ
k m n : Nat
ih : (m ⊖ n) * -[k+1] = n * (k + 1) ⊖ m * (k + 1)
⊢ (m + 1 ⊖ n + 1) * -[k+1] = (n + 1) * (k + 1) ⊖ (m + 1) * (k + 1)
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) * -[k+1] = n * (k + 1) ⊖ m * (k + 1)
⊢ (m ⊖ n) * -[k+1] = n * (k + 1) ⊖ m * (k + 1)

State before:
case succ_succ
k m n : Nat
ih : (m ⊖ n) * -[k+1] = n * (k + 1) ⊖ m * (k + 1)
⊢ (m ⊖ n) * -[k+1] = n * (k + 1) ⊖ m * (k + 1)
Tactic:
exact ih
State after:
no goals