mathlib

7db6ca99 - test({data/{finset,set},order/filter}/pointwise): Ensure priority of the `ℕ` and `ℤ` actions (#14166)

test({data/{finset,set},order/filter}/pointwise): Ensure priority of the `ℕ` and `ℤ` actions (#14166) Each of `set`, `finset`, `filter` creates (non propeq) diamonds with the fundamental `ℕ` and `ℤ` actions because of instances of the form `has_scalar α β → has_scalar α (set β)`. For example, `{2, 3}^2` could well be `{4, 9}` or `{4, 6, 9}`. The instances involved are all too important to be discarded, so we decide to live with the diamonds but give priority to the `ℕ` and `ℤ` actions. The reasoning for the priority is that those can't easily be spelled out, while the derived actions can. For example, `s.image ((•) 2)` easily replaces `2 • s`. Incidentally, additive combinatorics uses extensively the `ℕ` action. This PR adds both a library note and tests to ensure this stays the case. It also fixes the additive `set` and `filter` versions, which were not conforming to the test.