mathlib

b4a5b013 - feat(data/finset/basic): add card_insert_eq_ite (#10209)

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`.