Commit 2021-11-08 11:43 b4a5b013
View on Github →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.