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

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