refactor(data/real/basic): golf the ring instance

[eric-wieser]

This makes a number of changes:

• It avoids the use of refine_struct to define real.comm_ring. This is useful for porting, as that tactic no longer exists. The new proof is also very simple.
• It provides some missing lemmas about pow and smul linking to cauchy sequences
• It redefines has_smul and has_pow on real in a way that is compatible with cauchy sequences. This:
  • makes the pow and smul lemmas above easier
  • means we only need a single smul lemma rather than separate nsmul, zsmul, qsmul lemmas.
  • makes ((2 / 3 : ℚ) • 3 : ℝ) "computable" since it doesn't go through real.division_ring any more
  • has some minor downsides: pow_zero, rat.smul_def, and zpow_coe_nat are no longer true by definition. The proofs this breaks are already changed as of #18136.

---

• [x] depends on: #18118
• [x] depends on: #18129
• [x] depends on: #18156
• [x] depends on: #18225

[bors[bot]]

:v: eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[rwbarton]

I'm a bit confused: is the has_pow instance changing (up to defeq) or not? If so then why?

[eric-wieser]

I'm a bit confused: is the has_pow instance changing (up to defeq) or not?

Yes; the new definition is "elementwise power on the cauchy sequence"

If so then why?

Mainly because it makes the proof easier. Do you feel strongly about the defeqs listed in #18136 being useful?

Note that #18156 is a bugfix for pi.has_pow independently of this PR; ring broke on real not because I changed the defeq of has_pow, but because I changed the syntactic instance that was found.

[rwbarton]

Yes, I think it is definitely better to have a useful definition of ^ than to save a few lines in the internals of real.

[eric-wieser]

I can restore the old has_pow then; it's the has_smul defeq change that's more useful anyway.

[rwbarton]

I suggest we abandon this given that it seems to work better in Lean 4 to use a CommRing instance like the present mathlib 3 one.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#18118~~
• ~~leanprover-community/mathlib#18129~~
• ~~leanprover-community/mathlib#18156~~
• ~~leanprover-community/mathlib#18225~~ By Dependent Issues (🤖). Happy coding!