Theorem: SetTheory.one_def (SetTheory/Nat.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
⊢ 1 = {∅}
Tactic:
show ∅ ∪ {∅} = {∅}
State after:
V : Type u_1
inst✝ : Zermelo V
⊢ ∅ ∪ {∅} = {∅}

State before:
V : Type u_1
inst✝ : Zermelo V
⊢ ∅ ∪ {∅} = {∅}
Tactic:
simp
State after:
no goals