mathlib3

1955c1cf - feat(data/set/prod): Preimage of `set.pi` (#17534)