mathlib3

acab4f94 - feat(algebra/pointwise): add preimage_smul and generalize a couple of assumptions (#8600)