Theorem: Tutorial.zero_add (Nederpelt/Arithmetic.lean)

State before:
n : ℕ
⊢ 0 + n = n
Tactic:
induction n with 
| zero => rfl 
| succ n' ih => 
  rewrite [add_succ, ih] rfl
State after:
no goals

State before:
case zero

⊢ 0 + Nat.zero = Nat.zero
Tactic:
rfl
State after:
no goals

State before:
case succ
n' : ℕ
ih : 0 + n' = n'
⊢ 0 + succ n' = succ n'
Tactic:
rewrite [add_succ, ih]
State after:
case succ
n' : ℕ
ih : 0 + n' = n'
⊢ succ n' = succ n'

State before:
case succ
n' : ℕ
ih : 0 + n' = n'
⊢ succ n' = succ n'
Tactic:
rfl
State after:
no goals