Commit 2023-03-31 22:20 5e526d18
View on Github →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.