Commit 2020-05-16 14:49 c81be77b

feat(data/finset) Another finset disjointness lemma (#2698) I couldn't find this anywhere, and I wanted it. Naming question: this is "obviously" called disjoint_filter, except there's already a lemma with that name. I know I've broken one of the rules of using simp here ("don't do it at the beginning"), but this proof is much longer than I'd have thought would be necessary so I'm rather expecting someone to hop in with a one-liner.