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

State before:
m n : ℕ
⊢ mul (Nat.succ m) n = add (mul m n) n
Tactic:
induction n with
| zero       => rfl
| succ n' ih => simp only [add, add_succ, add_assoc, mul, ih]
State after:
no goals

State before:
case zero
m : ℕ
⊢ mul (Nat.succ m) Nat.zero = add (mul m Nat.zero) Nat.zero
Tactic:
rfl
State after:
no goals

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