no goals
α : Type u_1
β : Type ?u.272209
γ : Type ?u.272212
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b : α
s : Finset α
a : α
⊢ erase s a = ∅ ↔ s = ∅ ∨ s = {a}
rw [← sdiff_singleton_eq_erase, sdiff_eq_empty_iff_subset, subset_singleton_iff]