Commit 2021-10-11 07:59 082aa832

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.