mathlib3

24b50bfc - chore(data/finset/basic): move `disjoint` proofs earlier (#16436)

chore(data/finset/basic): move `disjoint` proofs earlier (#16436) This avoids repeating work for `disj_union`, and takes the stance that `disjoint` is part of the lattice API. Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>