mathlib3

25a42309 - chore(data/real/basic): cleanup (#8501)

chore(data/real/basic): cleanup (#8501) * use `is_lub` etc in the statement of `real.exists_sup`, rename it to `real.exists_is_lub`; * move parts of the proof of `real.exists_is_lub` around;