mathlib3

5491c592 - feat(data/fintype/basic): add lemmas about finsets and cardinality (#5886)

feat(data/fintype/basic): add lemmas about finsets and cardinality (#5886) Add lemmas about finsets and cardinality. Part of #5695 in order to prove Hall's marriage theorem. Coauthors: @kmill @b-mehta