scoping `SMul ℝ≥0∞ ?A` related instances

Stream: mathlib4

[Jireh Loreaux]

Can we scope all the instances in this file? We don't have any of the hypotheses in Mathlib: @loogle |- SMul ENNReal ?_

And it slows down type class inference in the more common scenario when we want to get an ℝ≥0 instance from the one for ℝ.

[loogle]

:shrug: nothing found

[Eric Wieser]

The instance is used by

import Mathlib

open NNReal ENNReal

#synth Module ℝ≥0 (ℝ≥0∞ × ℝ≥0∞)

[Eric Wieser]

These come from my !3#7846

[Eric Wieser]

I was hoping I had written a nice explanation there of why the instances go this way around, but alas

[Jireh Loreaux]

I claim it makes sense to scope that instance to the ENNReal namespace.

[Eric Wieser]

I claim that scoping instances isn't really a good pattern in general, as I think it means you can get into a state mid-proof where the instance is in the goal view, but the lemmas about it won't apply because the instance can't be re-synthesized

[Eric Wieser]

(things like ComplexOrder seem just about ok because we scoped them due to confusing semantics in the first place)

[Floris van Doorn]

We can at least lower the priority of these instances, so that the Real instances will be tried first.