This is based on discussion in the Zulip thread
https://leanprover.zulipchat.com/stream/287929-mathlib4/topic/Ring.20is.20determined.20by.20Semiring.

Note that this commit introduce `sorry`s into the codebase. It is a WIP.

Prove `Semiring.ext` and `Semiring.ext_iff` lemmas, as well as that
`Semiring.toNonUnitalSemiring` and `Semiring.toNonAssocSemiring` are
injective.

Prove the injectivity lemma in terms of the `ext` lemma, as the former
goes through showing that `h_add` and `h_mul` hold anyway.

Prove that `NonAssocSemiring.toNonUnitalNonAssocSemiring` is
injective.

Prove an `ext` lemma and use it to show that
`NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` is injective as
well as an `ext_iff` lemma.

…emiring`

Show that `NonUnitalNonAssocSemiring.toDistrib` is injective.

One exception: leave the `h` in `fun h ↦` in `ext_iff` proofs,
for (marginally) more readability.

Prove that `Semiring.toNonAssocSemiring` is injective.

For each of the three typeclasses, state the `ext` lemma with a
sorried proof and prove the consequences (injectivity and `ext_iff`
lemmas).

Highlight the locations in the file where something mathematically
non-trivial is proved: namely that some operation is determined by
others. (There are essentially only two such.)

Change `a`, `b` to `x`, `y` in accordance with
https://leanprover-community.github.io/contribute/style.html#variable-conventions.

Additionally, remove an unnecessary `'` from a variable `inst`.

Realise that it is now 2024 :).

Co-authored-by: Riccardo Brasca <[email protected]>

Fix typo in module header describing file.

Co-authored-by: Eric Wieser <[email protected]>

This is in accordance with the discussion in the thread
#9511 (comment).

Leave the `Add(Comm)MonoidWithOne` and `Add(Comm)GroupWithOne`
extensionality lemmas in `Mathlib/Algebra/Ring/Ext.lean` for now.

This resolves comments #9511 (comment)
and #9511 (comment).

Co-authored-by: Anne Baanen <[email protected]>

WARNING: this commit is NOT error-free.

WARNING: this commit is NOT error-free.

WARNING: this commit is NOT error-free.

Based on #9511 (comment).

Based on review suggestions https://github.com/leanprover-community/mathlib4/pull/9511/files#r1574231108, https://github.com/leanprover-community/mathlib4/pull/9511/files#r1574232858.

Co-authored-by: Anne Baanen <[email protected]>

…-rings

Specifically, replace `← Int.coe_nat_eq` with `Int.ofNat_eq_coe`.