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 basic support for `ConcreteCategory` to the `elementwise` attribute and elaborator: it still uses `HasForget` when a fresh instance is needed, but now will replace the `forget`-based operations with `ConcreteCategory`-based ones. So as long as there is only a `HasForget` instance, or no instance at all, in scope, `elementwise` will behave the same. But when there is a `ConcreteCategory` instance, all the `(forget C).obj X`es turn into `ToType X` and `(forget C).map f`s turn into `hom f`.

In the future, when we have replaced enough `HasForget` instances with `ConcreteCategory`, we can apply the changes from the branch `redesign-ConcreteCategory` to make `elementwise` use `ConcreteCategory` when it creates fresh instances.

* polynomial-sequences: (149 commits)
  Aha, here's how to get Lean to stop showing S.elems' in the infoview.
  Try satisfying the linter gods again.
  Probably enough initial tidying to send the PR.
  Kill more temporary names.
  Touch more natDegree.
  Does protected satisfy the docstring linter?
  Bit shorter.
  More
  Quiet linters.
  Remove redundant imports.
  Copyright header and more twiddling.
  Rename lemma to 'degree_smul_of_leadingCoeff_rightRegular' and split out
  feat(Polynomial): polynomial sequences are bases for R[X]
  chore(Dynamics/PeriodicPts): don't import `MonoidWithZero` (#20765)
  chore(Associated): split out `Ring` results (#20737)
  feat(AlgebraicGeometry): flat morphisms of schemes (#19790)
  feat(AlgebraicGeometry): scheme-theoretic fibre (#19427)
  chore: split Mathlib.Analysis.Asymptotics.Asymptotics (#20785)
  doc: typo (#20829)
  feat(CategoryTheory): condition for an induced functor between comma categories to be final  (#20139)
  feat(1000.yaml): allow statements of theorems also (#20637)
  feat(Algebra/Homology/Embedding): homology of truncGE' (#19570)
  chore: cleanup many porting notes in Combinatorics (#20823)
  chore: eliminate porting notes about `deriving Fintype` (#20820)
  feat(Algebra/Lie): a Lie algebra is solvable iff it is solvable after faithfully flat base change (#20808)
  feat: define bases of root pairings (#20667)
  feat(Tactic): basic ConcreteCategory support for elementwise (#20811)
  feat(CategoryTheory): define unbundled `ConcreteCategory` class  (#20810)
  chore(CategoryTheory): rename `ConcreteCategory` to `HasForget` (#20809)
  feat: `CommSemiring (NonemptyInterval ℚ≥0)` (#20783)
  chore(yaml_check.py): re-format (#20807)
  feat: elementary estimate for Real.log (#20766)
  feat: definition of linear topologies (#14990)
  feat(RingTheory): flatness over a semiring (#19115)
  feat(Algebra/Homology/Embedding): the canonical truncation truncLE (#19550)
  feat(Algebra/Homology/Embedding): API for the homology of an extension of homological complex (#19203)
  feat(Algebra/Ring): `RingEquiv.piUnique` (#20794)
  feat(RingTheory/LocalRing): add instance `Unique (MaximalSpectrum R)` for a local ring `R` (#20801)
  chore(GroupExtension/Defs): define `Section` and redefine `Splitting` (#20802)
  chore: restore `def` to `adicCompletion` (#20796)
  refactor: rename `UniqueContinuousFunctionalCalculus` to `ContinuousMap.UniqueHom` (#20643)
  feat(Algebra/Homology/Embedding): the morphism from a complex to its `truncGE` truncation (#19544)
  chore(Mathlib/Computability/TuringMachine): split file (#20790)
  feat(Data/Finset/Card): add `InjOn` and `SurjOn` versions of finset cardinality lemmas (#20753)
  feat(Order/WellFoundedSet): add convenience constructors for IsWF and IsPWO for WellFoundedLT types (#20752)
  feat(Set/Finite): a set is finite if its image and fibers are finite (#20751)
  chore: cleanup .gitignore files (#20795)
  feat(Topology/Group/Profinite):  Profinite group is limit of finite group (#16992)
  feat(Combinatorics/SimpleGraph): vertices in cycles (#20602)
  CI: merge `bot_fix_style` actions (#20789)
  ...