Elementary lemmas about finite sets

@[simp]

theorem Finset.ne_empty_iff_nonempty {α : Type u_1} {s : Finset α} : s ≠ ∅ ↔ s.Nonempty