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

State before:
⊢ 2 = succ 1
Tactic:
rfl
State after:
no goals