mathlib3

7951ed37 - feat(data/finset/basic): add lemmas about filter and (co)disjoint (#17296)

feat(data/finset/basic): add lemmas about filter and (co)disjoint (#17296) This generalizes `finset.filter_inter_filter_neg_eq` to when the sets are different, and then further to when the propositions are not complementary but only disjoint. A similar story is true of the `union` lemma.