Theorem: succ_add' (LAMR/Examples/using_lean_as_a_proof_assistant/induction.lean)

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

State before:
case zero
m : ℕ
⊢ add' (succ m) zero = succ (add' m zero)
Tactic:
rw [add', add']
State after:
no goals

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