mathlib

f29755b9 - refactor(data/set/pairwise): generalize `pairwise_disjoint` to `semilattice_inf_bot` (#9670)

refactor(data/set/pairwise): generalize `pairwise_disjoint` to `semilattice_inf_bot` (#9670) `set.pairwise_disjoint` was only defined for `set (set α)`. Now, it's defined for `set α` where `semilattice_inf_bot α`. I also * move it to `data.set.pairwise` because it's really not about `set` anymore. * drop the `set` namespace. * add more general elimination rules and rename the current one to `elim_set`.