mathlib

88c79e57 - feat(data/fintype/basic): embeddings of fintypes based on cardinal inequalities (#9346)

feat(data/fintype/basic): embeddings of fintypes based on cardinal inequalities (#9346) From https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/mapping.20a.20fintype.20into.20a.20finset/near/254493754, based on suggestions by @kmill and @eric-wieser and @riccardobrasca.