mathlib3

e1847377 - feat(data/real/ennreal): Add `to_real_{min, sup, inf}` (#16233)

feat(data/real/ennreal): Add `to_real_{min, sup, inf}` (#16233) This adds `to_real_min` to match `to_real_max`, and adds `inf` and `sup` spellings of these lemmas. Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>