no goals
α : Type u_1
β : Type ?u.16577
γ : Type ?u.16580
inst✝¹ : Fintype α
s✝ t : Finset α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ sᶜ ≠ univ ↔ Finset.Nonempty s
simp [eq_univ_iff_forall, Finset.Nonempty]