Theorem: LoVe.BackwardProofs.mul_zero (LoVe/Labs/Lab2Solution.lean)

State before:
n : ℕ
⊢ mul 0 n = 0
Tactic:
induction n with
| zero       => rfl
| succ n' ih => simp only [mul, ih]
State after:
no goals

State before:
case zero

⊢ mul 0 Nat.zero = 0
Tactic:
rfl
State after:
no goals

State before:
case succ
n' : ℕ
ih : mul 0 n' = 0
⊢ mul 0 (Nat.succ n') = 0
Tactic:
simp only [mul, ih]
State after:
no goals