This changes nothing about the definition of ring categories except upgrading the `HasForget` instance to `ConcreteCategory`. This PR is intended mostly as an experiment to contrast with #20815 and figure out why that one has a disappointing benchmark outcome.

This is a step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980

This PR adds a `ConcreteCategory` instance for the categories of rings: `SemiRingCat`, `RingCat`, `CommSemiRingCat` and `CommRingCat`. It also replaces the `Hom.hom` structure projection with an alias for `ConcreteCategory.hom`. The latter requires a few fixes downstream where things get mistakenly unfolded (especially involving `ModuleCat.restrictScalars`) or where `rw` doesn't see through the definitional equality `ConcreteCategory.hom (ConcreteCategory.ofHom f) = f`. Finally, a few places where the proof works around the old `forget` <-> `FunLike` mismatch, and needs updating.

I have not tried to look for code that can be cleaned up now, only at what broke. I want to get started on cleanup when the other concrete category instances are in.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

* origin/master: (294 commits)
  feat: equalizers and coequalizers in the category of ind-objects (#21139)
  doc: turn more links to Stacks into `@[stacks]` tags (#21135)
  feat(Asymptotics): prove `IsLittleOTVS.add` (#20578)
  feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062)
  chore: import Std in Mathlib.lean (#21126)
  feat(Data/Matroid/Circuit): fundamental circuits and extensionality  (#21145)
  feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140)
  feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109)
  feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042)
  doc: fixed notation error in customizing category composition (#21132)
  feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143)
  chore(SupIndep): speedup the `Decidable` instance (#21114)
  fix(CI): use `Elab.async=false` for late importers workflow (#21147)
  feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687)
  feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921)
  feat(Algebra): `Pi.single_induction` (#21141)
  chore(BigOperators/Fin): golf a proof (#21131)
  feat: generalize tangent cone lemmas to TVS (#20859)
  feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136)
  refactor: unapply matrix lemmas (#21091)
  chore(Algebra/Category): `erw` -> `rw` (#21130)
  feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128)
  feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125)
  feat: PSum of finite sorts is finite (#20285)
  feat: inequality on the integral of a convex function of a RN derivative (#21093)
  feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058)
  chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317)
  feat: a `RelHom` preserves directedness (#20080)
  feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677)
  chore(Data/Matrix/PEquiv): clean up names (#21108)
  feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815)
  feat: define Descriptive.Tree (#18763)
  chore(Data/Complex/Exponential): split trig functions to new file (#21075)
  feat(Logic/IsEmpty/Relator): empty on sides (#20319)
  feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121)
  feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661)
  feat(RingTheory/LaurentSeries): add algebraEquiv (#21004)
  chore(SetTheory/Game/Impartial): golf two proofs (#21074)
  feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047)
  feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023)
  feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994)
  feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970)
  feat(RingTheory/Artinian): `IsUnit a` iff `a ∈ R⁰` for an artinian ring `R` (#21084)
  feat: separating set in the category of ind-objects (#21082)
  feat: derivWithin lemmas (#21092)
  chore(Fintype): golf a proof (#21113)
  chore: golf using `funext₂` (#21106)
  chore(Algebra/Group/Submonoid/Operations): move instances to new file (#21067)
  doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations (#21101)
  doc(ComputeDegree): typos (#21095)
  ...

* polynomial-sequences: (308 commits)
  Use the lemma we already added.
  Minor reordering.
  This is true even for the trivial ring.
  Also add the lt versions and the other inj lemma.
  Also add the basis ne versions.
  This seems also like it should be simp.
  Back to sorry free.
  And the natDegree version.
  feat: equalizers and coequalizers in the category of ind-objects (#21139)
  doc: turn more links to Stacks into `@[stacks]` tags (#21135)
  feat(Asymptotics): prove `IsLittleOTVS.add` (#20578)
  feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062)
  chore: import Std in Mathlib.lean (#21126)
  feat(Data/Matroid/Circuit): fundamental circuits and extensionality  (#21145)
  feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140)
  feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109)
  feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042)
  doc: fixed notation error in customizing category composition (#21132)
  feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143)
  chore(SupIndep): speedup the `Decidable` instance (#21114)
  fix(CI): use `Elab.async=false` for late importers workflow (#21147)
  feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687)
  feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921)
  feat(Algebra): `Pi.single_induction` (#21141)
  chore(BigOperators/Fin): golf a proof (#21131)
  feat: generalize tangent cone lemmas to TVS (#20859)
  feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136)
  refactor: unapply matrix lemmas (#21091)
  chore(Algebra/Category): `erw` -> `rw` (#21130)
  feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128)
  feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125)
  feat: PSum of finite sorts is finite (#20285)
  feat: inequality on the integral of a convex function of a RN derivative (#21093)
  feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058)
  chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317)
  feat: a `RelHom` preserves directedness (#20080)
  feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677)
  chore(Data/Matrix/PEquiv): clean up names (#21108)
  feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815)
  feat: define Descriptive.Tree (#18763)
  chore(Data/Complex/Exponential): split trig functions to new file (#21075)
  feat(Logic/IsEmpty/Relator): empty on sides (#20319)
  feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121)
  feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661)
  feat(RingTheory/LaurentSeries): add algebraEquiv (#21004)
  chore(SetTheory/Game/Impartial): golf two proofs (#21074)
  feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047)
  feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023)
  feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994)
  feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970)
  ...