Theorem: Set.mem_singleton (WTA.lean)

State before:
α✝ : Type u_1
a : α✝
⊢ a ∈ singleton a
Tactic:
simp [singleton, Membership.mem]
State after:
no goals