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

State before:
m n : ℕ
⊢ add m n = add n m
Tactic:
induction n with
| zero       => simp [add, add_zero]
| succ n' ih => simp [add, add_succ, ih]
State after:
no goals

State before:
case zero
m : ℕ
⊢ add m Nat.zero = add Nat.zero m
Tactic:
simp [add, add_zero]
State after:
no goals

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