mathlib

080cbe2f - feat(data/set/fintype): Add `to_finset_nonempty`. (#16925)

feat(data/set/fintype): Add `to_finset_nonempty`. (#16925) We have `finset.nonempty_coe` and `finite.nonempty_to_finset`, but we don't have this for fintypes. This PR adds this lemma.