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

State before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * b = b * a
Tactic:
induction a with
| zero =>
  change 0 * b = a * 0
  rw [zero_mul, mul_zero]
| succ n hn =>
  rw [succ_mul, hn, mul_succ]
State after:
no goals

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

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

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