feat(data/finset): add `finset.erase_none` (#9630)
* move `option.to_finset` and `finset.insert_none` to a new file `data.finset.option`; redefine the latter in terms of `finset.cons`;
* define `finset.erase_none`, prove lemmas about it;
* add `finset.prod_cons`, `finset.sum_cons`, `finset.coe_cons`, `finset.cons_subset_cons`, `finset.card_cons`;
* add `finset.subtype_mono` and `finset.bUnion_congr`;
* add `set.insert_subset_insert_iff`;
* add `@[simp]` to `finset.map_subset_map`;
* upgrade `finset.map_embedding` to an `order_embedding`;
* add `@[simps]` to `equiv.option_is_some_equiv` and `function.embedding.some`;
* golf some proofs.
