no goals
n m k : Nat
⊢ n * (m + k) = n * m + n * k
induction n generalizing m k with
| zero      => repeat rw [Nat.zero_mul]
| succ n ih => simp [succ_mul, ih]; rw [Nat.add_assoc, Nat.add_assoc (n*m)]; apply congrArg; apply Nat.add_left_comm
no goals
case zero
m k : Nat
⊢ zero * (m + k) = zero * m + zero * k
repeat rw [Nat.zero_mul]
case succ
n : Nat
ih : ∀ (m k : Nat), n * (m + k) = n * m + n * k
m k : Nat
⊢ n * m + n * k + (m + k) = n * m + m + (n * k + k)
case succ
n : Nat
ih : ∀ (m k : Nat), n * (m + k) = n * m + n * k
m k : Nat
⊢ succ n * (m + k) = succ n * m + succ n * k
simp [succ_mul, ih]
case succ
n : Nat
ih : ∀ (m k : Nat), n * (m + k) = n * m + n * k
m k : Nat
⊢ n * m + (n * k + (m + k)) = n * m + (m + (n * k + k))
case succ
n : Nat
ih : ∀ (m k : Nat), n * (m + k) = n * m + n * k
m k : Nat
⊢ n * m + n * k + (m + k) = n * m + m + (n * k + k)
rw [Nat.add_assoc, Nat.add_assoc (n*m)]
case succ.h
n : Nat
ih : ∀ (m k : Nat), n * (m + k) = n * m + n * k
m k : Nat
⊢ n * k + (m + k) = m + (n * k + k)
case succ
n : Nat
ih : ∀ (m k : Nat), n * (m + k) = n * m + n * k
m k : Nat
⊢ n * m + (n * k + (m + k)) = n * m + (m + (n * k + k))
apply congrArg
no goals
case succ.h
n : Nat
ih : ∀ (m k : Nat), n * (m + k) = n * m + n * k
m k : Nat
⊢ n * k + (m + k) = m + (n * k + k)
apply Nat.add_left_comm