mathlib3

2865d8c2 - refactor(data/set/prod): add notation class for set-like product (#11300)

refactor(data/set/prod): add notation class for set-like product (#11300) This PR adds notation class `has_set_prod` for product of sets and subobjects. I also add an instance for `set`s. Later I want to migrate `finset`s and `sub*` product to this notation class.