-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem mul_add : ∀ a b c : Int, a * (b + c) = a * b + a * c
  | (m:Nat), (n:Nat), (k:Nat) => by simp [Nat.left_distrib]
  | (m:Nat), (n:Nat), -[k+1]  => by
    simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl
  | (m:Nat), -[n+1],  (k:Nat) => by
    simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl
  | (m:Nat), -[n+1],  -[k+1]  => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]
  | -[m+1],  (n:Nat), (k:Nat) => by simp [Nat.mul_comm]; rw [← Nat.right_distrib, Nat.mul_comm]
  | -[m+1],  (n:Nat), -[k+1]  => by
    simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl
  | -[m+1],  -[n+1],  (k:Nat) => by simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl
  | -[m+1],  -[n+1],  -[k+1]  => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]

Proof state:
m n k : Nat
⊢ -[m+1] * (↑n + ↑k) = -[m+1] * ↑n + -[m+1] * ↑k

Tactic:
simp [Nat.mul_comm]

Result:
m n k : Nat
⊢ negOfNat ((n + k) * (m + 1)) = negOfNat (n * (m + 1) + k * (m + 1))

Proof state:
m n k : Nat
⊢ ↑m * (↑n + -[k+1]) = ↑m * ↑n + ↑m * -[k+1]

Tactic:
simp [negOfNat_eq_subNatNat_zero]

Result:
m n k : Nat
⊢ subNatNat (m * n) (m * (k + 1)) = ↑(m * n) + subNatNat 0 (m * (k + 1))

Proof state:
m n k : Nat
⊢ subNatNat ((m + 1) * (k + 1)) ((m + 1) * n) = subNatNat 0 ((m + 1) * n) + ↑((m + 1) * (k + 1))

Tactic:
rw [Int.add_comm, ← subNatNat_add]

Result:
m n k : Nat
⊢ subNatNat ((m + 1) * (k + 1)) ((m + 1) * n) = subNatNat ((m + 1) * (k + 1) + 0) ((m + 1) * n)

Proof state:
m n k : Nat
⊢ ↑m * (↑n + ↑k) = ↑m * ↑n + ↑m * ↑k

Tactic:
simp [Nat.left_distrib]

Result:
no goals

Proof state:
m n k : Nat
⊢ subNatNat (m * k) (m * (n + 1)) = subNatNat (m * k + 0) (m * (n + 1))

Tactic:
rfl

Result:
no goals

Proof state:
m n k : Nat
⊢ negOfNat ((n + k) * (m + 1)) = negOfNat (n * (m + 1) + k * (m + 1))

Tactic:
rw [← Nat.right_distrib, Nat.mul_comm]

Result:
no goals

Proof state:
m n k : Nat
⊢ -[m+1] * (-[n+1] + ↑k) = -[m+1] * -[n+1] + -[m+1] * ↑k

Tactic:
simp [negOfNat_eq_subNatNat_zero]

Result:
m n k : Nat
⊢ subNatNat ((m + 1) * (n + 1)) ((m + 1) * k) = ↑((m + 1) * (n + 1)) + subNatNat 0 ((m + 1) * k)

Proof state:
m n k : Nat
⊢ ↑m * (-[n+1] + -[k+1]) = ↑m * -[n+1] + ↑m * -[k+1]

Tactic:
simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]

Result:
no goals

Proof state:
m n k : Nat
⊢ subNatNat ((m + 1) * (k + 1)) ((m + 1) * n) = subNatNat ((m + 1) * (k + 1) + 0) ((m + 1) * n)

Tactic:
rfl

Result:
no goals

Proof state:
m n k : Nat
⊢ subNatNat ((m + 1) * (n + 1)) ((m + 1) * k) = ↑((m + 1) * (n + 1)) + subNatNat 0 ((m + 1) * k)

Tactic:
rw [← subNatNat_add]

Result:
m n k : Nat
⊢ subNatNat ((m + 1) * (n + 1)) ((m + 1) * k) = subNatNat ((m + 1) * (n + 1) + 0) ((m + 1) * k)

Proof state:
m n k : Nat
⊢ -[m+1] * (↑n + -[k+1]) = -[m+1] * ↑n + -[m+1] * -[k+1]

Tactic:
simp [negOfNat_eq_subNatNat_zero]

Result:
m n k : Nat
⊢ subNatNat ((m + 1) * (k + 1)) ((m + 1) * n) = subNatNat 0 ((m + 1) * n) + ↑((m + 1) * (k + 1))

Proof state:
m n k : Nat
⊢ subNatNat (m * k) (m * (n + 1)) = subNatNat 0 (m * (n + 1)) + ↑(m * k)

Tactic:
rw [Int.add_comm, ← subNatNat_add]

Result:
m n k : Nat
⊢ subNatNat (m * k) (m * (n + 1)) = subNatNat (m * k + 0) (m * (n + 1))

Proof state:
m n k : Nat
⊢ ↑m * (-[n+1] + ↑k) = ↑m * -[n+1] + ↑m * ↑k

Tactic:
simp [negOfNat_eq_subNatNat_zero]

Result:
m n k : Nat
⊢ subNatNat (m * k) (m * (n + 1)) = subNatNat 0 (m * (n + 1)) + ↑(m * k)

Proof state:
m n k : Nat
⊢ subNatNat (m * n) (m * (k + 1)) = ↑(m * n) + subNatNat 0 (m * (k + 1))

Tactic:
rw [← subNatNat_add]

Result:
m n k : Nat
⊢ subNatNat (m * n) (m * (k + 1)) = subNatNat (m * n + 0) (m * (k + 1))

Proof state:
m n k : Nat
⊢ subNatNat ((m + 1) * (n + 1)) ((m + 1) * k) = subNatNat ((m + 1) * (n + 1) + 0) ((m + 1) * k)

Tactic:
rfl

Result:
no goals

Proof state:
m n k : Nat
⊢ -[m+1] * (-[n+1] + -[k+1]) = -[m+1] * -[n+1] + -[m+1] * -[k+1]

Tactic:
simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]

Result:
no goals

Proof state:
m n k : Nat
⊢ subNatNat (m * n) (m * (k + 1)) = subNatNat (m * n + 0) (m * (k + 1))

Tactic:
rfl

Result:
no goals