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

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

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