mathlib3

852b23b5 - chore(topology,analysis): make the sup metric and norm computable (#16570)

chore(topology,analysis): make the sup metric and norm computable (#16570) To make this work, we replace `max` with `sup` in the implementation (the two are defeq, but the former has stronger typeclass arguments), and add some missing shortcut instances for `ennreal` which are needed for the emetric structure. As a result, we can can now perform useless "computation"s like: ```lean #eval ∥((3 : ℤ), (4 : ℤ))∥ -- real.of_cauchy (sorry /- 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, ... -/) ``` (this isn't totally useless; it's enough to inform the reader that they're not looking at a euclidean norm, which is a common source of confusion)