theorem Set.mem_singleton_iff._simp_1
theorem Set.mem_singleton_iff._simp_1: ∀ {α : Type u} {a b : α}, Membership.mem (singleton b) a = (a = b)
theorem Set.mem_singleton_iff._simp_1
theorem Set.mem_singleton_iff._simp_1: ∀ {α : Type u} {a b : α}, Membership.mem (singleton b) a = (a = b)