mathlib3

ee607111 - feat(data/finset/basic): product, bUnion, sdiff lemmas (#8321)