mathlib3

976b261a - feat(data/{multiset,finset}/basic): card_erase_eq_ite (#9185)

feat(data/{multiset,finset}/basic): card_erase_eq_ite (#9185) A generic theorem about the cardinality of a `finset` or `multiset` with an element erased. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>