Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(data/finset/basic): add card_insert_eq_ite (#10209)
Adds the lemma `card_insert_eq_ite` combining the functionality of `card_insert_of_not_mem` and `card_insert_of_mem`, analogous to how `card_erase_eq_ite`.
- Loading branch information