feat(data/set/n_ary): Distributivity of `∩` (#17924)
`set.image2 f` for `injective2 f` distributes over intersection.
Also move the required results from `data.set.prod` to `data.set.n_ary`. As a bonus, this makes quite a few files not depend on `data.set.n_ary` anymore and matches the import direction for the corresponding `finset` files.
