mathlib

0eb160a5 - feat(data/finset/basic): When `insert` is injective and other lemmas (#11982)

feat(data/finset/basic): When `insert` is injective and other lemmas (#11982) * `insert`/`cons` lemmas for `finset` and `multiset` * `has_ssubset` instance for `multiset` * `finset.sdiff_nonempty` * `disjoint.of_image_finset`, `finset.disjoint_image`, `finset.disjoint_map` * `finset.exists_eq_insert_iff` * `mem` lemmas * change `pred` to `- 1` into the statement of `finset.card_erase_of_mem`