Reduce the diff of #11203

…atCast`

Reduce the diff of #11203

These lemmas are needed to define the semifield structure on `NNRat`, hence I am repurposing `Algebra.Order.Field.Defs` from avoiding a timeout (which I believe was solved long ago) to avoiding to import random stuff in the definition of the semifield structure on `NNRat` (although this PR doesn't actually reduce imports there, it will be in a later PR).

Reduce the diff of #11203

Reduce the diff of #11203

Reduce the diff of #11203

by declaring them all in `where` style with implicit type assumptions and `inst` prefix

Here to reduce the diff from #11203

Among other things, change the `nsmul`, `zsmul`, `qsmul` fields to have `n`/`q` come before `x`, because this matches the lemmas we want to write about them. It would be preferrable to perform the same changes to the `AddMonoid`/`AddGroup`-like typeclasses, but this is impossible with the current `to_additive` framework, so instead I have inserted some `Function.swap` at the interface between `AddMonoid`/`AddGroup` and `Ring`/`Field`.

Reduce the diff of #11203

Soon, there will be `NNRat` analogs of the `Rat` fields in the definition of `Field`. `NNRat` is less nicely a structure than `Rat`, hence there is a need to reduce the dependency of `Field` on the internals of `Rat`.

This PR achieves this by restating `Field.ratCast_mk'` in terms of `Rat.num`, `Rat.den`. This requires fixing a few downstream instances.

Reduce the diff of #11203.




Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

…atCast` (#11499)

This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy.

Reduce the diff of #11203

`Rat` has a long history in (and before) mathlib and as such its development is full of cruft. Now that `NNRat` is a thing, there is a need for the theory of `Rat` to be mimickable to yield the theory of `NNRat`, which is not currently the case.

Broadly, this PR aims at mirroring the `Rat` and `NNRat` declarations. It achieves this by:
* Relying more on `Rat.num` and `Rat.den`, and less on the structure representation of `Rat`
* Abandoning the vestigial `Rat.Nonneg` (which was replaced in Std by a new development of the order on `Rat`)
* Renaming many `Rat` lemmas with dubious names. This creates quite a lot of conflicts with Std lemmas, whose names are themselves dubious. I am priming the relevant new mathlib names and leaving TODOs to fix the Std names.
* Handling most of the `Rat` porting notes

Reduce the diff of #11203