chore(data/set/pairwise): split (#17880)
This PR will split most of the lemmas in `data.set.pairwise` which are independent of the `data.set.lattice`. It makes a lot of files no longer depend on `data.set.lattice`.
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/315072418)
mathlib4 PR: https://github.com/leanprover-community/mathlib4/pull/1184
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
