no goals
α : Type u_1
β : Type ?u.154891
s t : Set α
a b x y : α
f : α → β
inst✝ : Nonempty α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s ≤ 1 ↔ ∃ x, s ⊆ {x}
simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one_iff_subset_singleton,
  Finite.toFinset_subset, Finset.coe_singleton]