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.
