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

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