mathlib3

feat(data/finset): monotone bijection from fin k

#2163

Merged