mathlib3

6ca1a09b - refactor(order/bounded_order): relax typeclass requirements on `disjoint` and `codisjoint` (#16434)

refactor(order/bounded_order): relax typeclass requirements on `disjoint` and `codisjoint` (#16434) Currently we have two different notions of finset disjointness: * `∀ a ∈ s, a ∉ t`, used by `finset.disj_union` and `finset.disj_Union` * `disjoint s t` (`s ⊓ t ≤ ⊥`), used by almost everything else The second spelling uses `finset.has_inf` which requires decidable equality to compute the intersection. Of course, we don't need to compute the intersection, we just need to say that no element can belong to it. More precisely, decidability of equality is only needed for _decidability_ of disjointness, not to state disjointness in the first place. If were were to change `finset.disj_union` to take a `disjoint` argument, then either: * It would need to be a weird `@disjoint` term with a classical decidable instance. reducing the generality of the lemma. * it would need to gain a `decidable_eq` argument; thus losing much of the benefit it provides over `finset.has_union`! Instead, this PR opts for redefining `disjoint s t` to not require `has_inf`, as `∀ ⦃x⦄, x ≤ s → x ≤ t → x ≤ ⊥`. The analogous change is made to `codisjoint s t` for consistency. As a bonus, the new definition works in cases where there is no unique infimum. The changes in this PR are largely either: * Adjustments to the `disjoint` API to handle the extra generality * Adjustments to proofs that relied on the definitional equality of `disjoint` to use `disjoint.le_bot` or `disjoint_left` * Reordering of finset lemmas to move statements about disjointness earlier in the file where no `decidable_eq` hypothesis is present. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>