mathlib3

e60e1f22 - feat(data/real/pointwise): mul distributes over `infi` and `supr` (#12105)