mathlib3

feat(data/set/finite): remove exists_finset_of_finite

#1782

Merged