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

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

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

State before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ 0 * 0 = 0
Tactic:
rw [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 : 0 * n = 0
⊢ 0 * succ n = 0
Tactic:
rw [mul_succ, hn, add_zero]
State after:
no goals