mathlib3

0b5f0a2d - feat(data/finset/basic): add ite_subset_union, inter_subset_ite for finset (#10586)

feat(data/finset/basic): add ite_subset_union, inter_subset_ite for finset (#10586) Just a couple of lemmas to simplify expressions involving ite and union / inter on finsets, note that this is not related to `set.ite`. From flt-regular.