[Merged by Bors] - feat(data/finset): add finset.erase_none
#9630
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
option.to_finset
andfinset.insert_none
to a new filedata.finset.option
; redefine the latter in terms offinset.cons
;finset.erase_none
, prove lemmas about it;finset.prod_cons
,finset.sum_cons
,finset.coe_cons
,finset.cons_subset_cons
,finset.card_cons
;finset.subtype_mono
andfinset.bUnion_congr
;set.insert_subset_insert_iff
;@[simp]
tofinset.map_subset_map
;finset.map_embedding
to anorder_embedding
;@[simps]
toequiv.option_is_some_equiv
andfunction.embedding.some
;