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

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

State before:
case zero

⊢ add' 0 zero = zero
Tactic:
rw [add']
State after:
no goals

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