Theorem: N.mul_add (LeanTeaching/TD/TD02_sol.lean)

State before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * (b + c) = a * b + a * c
Tactic:
induction b with
| zero =>
  change a * (0 + c) = a * 0 + a * c
  rw [zero_add, mul_zero, zero_add]
| succ n hn =>
  rw [succ_add, mul_succ, hn, mul_succ, add_assoc, add_comm (a*c), add_assoc]
State after:
no goals

State before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * (zero + c) = a * zero + a * c
Tactic:
change a * (0 + c) = a * 0 + a * c
State after:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * (0 + c) = a * 0 + a * c

State before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * (0 + c) = a * 0 + a * c
Tactic:
rw [zero_add, mul_zero, zero_add]
State after:
no goals

State before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : a * (n + c) = a * n + a * c
⊢ a * (succ n + c) = a * succ n + a * c
Tactic:
rw [succ_add, mul_succ, hn, mul_succ, add_assoc, add_comm (a*c), add_assoc]
State after:
no goals