mathlib3

68cc4218 - feat(data/finset/basic): `finset.to_list_eq_singleton_iff` (#18236)

feat(data/finset/basic): `finset.to_list_eq_singleton_iff` (#18236) We add the finset analog of `multiset.to_list_eq_singleton_iff`. Mathlib4 pair: https://github.com/leanprover-community/mathlib4/pull/1726