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

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

State before:
case zero
n : ℕ
⊢ mul Nat.zero n = mul n Nat.zero
Tactic:
simp only [mul, mul_zero]
State after:
no goals

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

State before:
case succ
n m' : ℕ
ih : mul m' n = mul n m'
⊢ add (mul n m') n = mul n (Nat.succ m')
Tactic:
ac_rfl
State after:
no goals