no goals
α : Type u_1
β : Type ?u.35142
γ : Type ?u.35145
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ s ⊆ {a} ↔ s = ∅ ∨ s = {a}
rw [← coe_subset, coe_singleton, Set.subset_singleton_iff_eq, coe_eq_empty, coe_eq_singleton]