mathlib

487385a4 - refactor(data/real/basic): make `⊓` and `⊔` computable on reals (#16463)

refactor(data/real/basic): make `⊓` and `⊔` computable on reals (#16463) This also makes `norm` and `dist` computable on `real`, `nnreal`, `rat`, and `int`. From a mathematical point of view that doesn't care about computability, this still contains the (mildly) interesting result that the maximum of two reals is equal to the real produced by taking the elementwise maximum of the two cauchy sequences. This change causes some unpleasant elaboration pain in `modular.lean` for reasons presumably linked to unification of dependent typeclasses. It's not clear to me precisely what the cause if. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>