Commit 2022-09-20 07:09 560891c4

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.