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

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

State before:
x y : Nat
⊢ x + succ y = succ (x + y)
Tactic:
rfl
State after:
no goals