[Merged by Bors] - chore: make instSMulRealComplex scoped

[MichaelStollBayreuth]

This scopes and moves to Complex.SMul the instance instSMulRealComplex.
Rationale: This instance is used in Data.Complex.{Basic|Module} to bootstrap SMul instances from the reals, but afterwards, instances SMul R ℂ should not need to rely on that (rather be obtained via Algebra R ℂ, for example). This speeds up the two mentioned files a bit (in fact, it reverts a slow-down caused by reducing the instance priority in #12070) and does not seem to have any adverse effects.

I think this is a cleaner solution compared to just reducing the instance priority.

See here on Zulip.

---

[MichaelStollBayreuth]

!bench

[leanprover-bot]

Here are the benchmark results for commit 3fc1b49.
There were no significant changes against commit 0129c03.

[MichaelStollBayreuth]

There is a positive effect on Mathlib.Data.Complex.{Basic|Module} (and also overall):

Mathlib.Data.Complex.Basic instructions 30,567 Mrd. -1,919 Mrd. -6,278 % 28,648 Mrd.
Mathlib.Data.Complex.Module instructions 101,03 Mrd. -6,104 Mrd. -6,042 % 94,926 Mrd.
build instructions 111,658 Bio. -13,731 Mrd. -0,012 % 111,644 Bio.
(Mrd. = 10⁹, Bio. = 10¹²)

This is likely caused by the instance now being top of the pile in these files, where it is really needed (but is not present outside).

[mattrobball]

Does scoping an instance actually do anything?

[MichaelStollBayreuth]

Does scoping an instance actually do anything?

Yes:

import Mathlib

variable (a b : ℂ)

#check a ≤ b -- failed to synthesize instance LE ℂ

open scoped ComplexOrder

#check a ≤ b -- a ≤ b : Prop

[mattrobball]

I had a previous experiment where I tried to retroactively scope some parent projections which didn't work. But the problem was the instance erasure and not the scoping.

I think scoped instances are a very good idea as another lever to guide typeclass synthesis.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style