feat(data/{set,finset}/pointwise): `a • t ⊆ s • t` (#18697)
Eta expansion in the lemma statements is deliberate, to make the left and right lemmas more similar and allow further rewrites.
Also additivise `finset.bUnion_smul_finset`, fix the name of `finset.smul_finset_mem_smul_finset` to `finset.smul_mem_smul_finset`, move `image2_swap`/`image₂_swap` further up the file to let them be used in earlier proofs.
