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

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

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

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