Theorem: LeanDemo.zero_add (LeanMeetup/Demo01.lean)

State before:
⊢ ∀ (x : Nat), 0 + x = x
Tactic:
intro x
State after:
x : Nat
⊢ 0 + x = x

State before:
x : Nat
⊢ 0 + x = x
Tactic:
induction x
State after:
case zero

⊢ 0 + zero = zero

case succ
n✝ : Nat
n_ih✝ : 0 + n✝ = n✝
⊢ 0 + succ n✝ = succ n✝

State before:
⊢ 0 + zero = zero
Tactic:
case zero         => 
  rfl
State after:
no goals

State before:
x' : Nat
ih : 0 + x' = x'
⊢ 0 + succ x' = succ x'
Tactic:
case succ x' ih   =>
  rw [add_succ, ih]
State after:
no goals

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

State before:
x' : Nat
ih : 0 + x' = x'
⊢ 0 + succ x' = succ x'
Tactic:
rw [add_succ, ih]
State after:
no goals