no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite s
⊢ Finset.Nonempty (Finite.toFinset h) ↔ Set.Nonempty s
rw [← Finset.coe_nonempty, Finite.coe_toFinset]