Theorem: LoVe.BackwardProofs.mul_add (LoVe/Lectures/LoVe03_BackwardProofs_Demo.lean)

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

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

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

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