mathlib3

0c0ee7b0 - refactor(data/set/pairwise): Make arguments of `set.pairwise` semi-implicit (#10740)

refactor(data/set/pairwise): Make arguments of `set.pairwise` semi-implicit (#10740) The previous definition was `∀ x ∈ s, ∀ y ∈ s, x ≠ y → r x y`. It now is `∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → x ≠ y → r x y`. The explicitness resulted in a lot of useless `_` and general pain using `set.pairwise`, `set.pairwise_disjoint`, `zorn.chain`, `is_antichain`...