mathlib

9dfe6490 - feat(data/{set,finset}/prod): lemmas about disjoint and intersections (#17496)