#19065)

In the current design of concrete categories in mathlib, there are two sources of `erw`s:

- Def-Eq abuse of `A ⟶ B` and `A →ₐ [R] B`: The type of `A ⟶ B` is by definition `A →ₐ[R] B`, but not at reducible transparency. So it happens that one `rw` lemma transforms a term in a form, where the next `rw` expects `A →ₐ B`. By supplying explicit `show` lines (copying the output of the pretty-printer), Lean correctly re-synthesizes the type to be `A →ₐ B` and the `rw` succeeds. This def-eq abuse hence always causes issues in the case where a lemma from the non-category theoretic part of the library should be applied. An insightful example is the following proof excerpt from current master (proof of `AlgebraCat.adj`):
```lean
import Mathlib.Algebra.Category.AlgebraCat.Basic
open CategoryTheory AlgebraCat
variable {R : Type u} [CommRing R]
set_option pp.analyze true

example : free.{u} R ⊣ forget (AlgebraCat.{u} R) :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun _ _ => (FreeAlgebra.lift _).symm
      homEquiv_naturality_left_symm := by
        intro X Y Z f g
        apply FreeAlgebra.hom_ext
        ext x
        simp only [Equiv.symm_symm, Function.comp_apply, free_map]
        /- Eq (α := Z)
             (((FreeAlgebra.lift R) (f ≫ g) :
               Prefunctor.obj (Functor.toPrefunctor (free R)) X ⟶ Z) (FreeAlgebra.ι R x) : ↑Z) _
        -/
        erw [FreeAlgebra.lift_ι_apply]
        sorry
      homEquiv_naturality_right := sorry }
```
The `simp` lemma `FreeAlgebra.lift_ι_apply` expects an `AlgHom`, but as the `pp.analyze` shows, the type is synthesized as a `⟶`. With a show line before the `erw`, Lean correctly synthesizes the type as an `AlgHom` again and the `rw` succeeds. The solution is to strictly distinguish between `A ⟶ B` and `A →ₐ[R] B`: We define a new `AlgebraCat.Hom` structure with a single field `hom : A →ₐ[R] B`. The above proof is mostly solved by `ext; simp` then, except for the `ext` lemma `FreeAlgebra.hom_ext` not applying. This is because now the type is `AlgebraCat.of R (FreeAlgebra R X) →ₐ[R] _` and Lean can't see through the `AlgebraCat.of` at reducible transparency. Hence the solution is to make `AlgebraCat.of` an `abbrev`. Finally, the proof is `by ext; simp` or even `by aesop`.

- `FunLike`: An intermediate design adapted the changes from the first point, but with keeping a `FunLike` and an `AlgHomClass` instance on `A ⟶ B`. This lead to many additional `coe` lemmas for composition of morphisms, where it mattered which of the three appearing terms of `AlgebraCat` where of the form `AlgebraCat.of R A`. Eric Wieser suggested to replace the `FunLike` by a `CoeFun` which is inlined, so an invocation of `f x` turns into `f.hom x`. This has then worked very smoothly.

So the key points are:
- Homs in concrete categories should be one-field structures to maintain a strict type distinction.
- Use `CoeFun` instead of `FunLike`, since the latter is automatically inlined.
- Make `.of` constructors an `abbrev` to obtain the def-eq `↑(AlgebraCat.of R A) = A` at reducible transparency.

For more details, see the [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Fixing.20the.20.60erw.60.20hell.20around.20concrete.20categories).

This PR follows the approach of #19065 to solve painful definitional equalities problems by forbidding the identification of `A ⟶ B` and `A →ₗ[R] B`. These are not equal reducibly, so tactics get confused if one is replaced by the other.

Currently the PR consists mostly of me playing "type tetris" to get everything to compile again: I haven't looked for which proofs can be cleaned up as a result.

This commit is not quite finished, please see the Zulip thread for more details.

This PR follows the approach of #19065 to solve painful definitional equalities problems by forbidding the identification of `A ⟶ B` and `A →ₗ[R] B`. These are not equal reducibly, so tactics get confused if one is replaced by the other.

Currently the PR consists mostly of me playing "type tetris" to get everything to compile again: I haven't looked for which proofs can be cleaned up as a result.

This commit is not quite finished, please see the Zulip thread for more details.

#19511)

This PR follows the approach of #19065 to solve painful definitional equalities problems by forbidding the identification of `A ⟶ B` and `A →ₗ[R] B`. These are not equal reducibly, so tactics get confused if one is replaced by the other.

There seem to be a few regressions caused by defeq abuse that we were able to get away with previously, but some subtle elaboration differences made it evident. Otherwise the cost is inserting many `.hom`s and `asHom`s.

A few steps that might clean up the diff, but would be too much work to incorporate in this PR:
 * Make the `ext` tactic pick up `TensorProduct.ext` again.
 * Replace the defeq abuse between `(restrictScalars f).obj M` and `M` with explicit maps going back and forth.

Overall quite a few proofs could be cleaned up at the cost of more bookkeeping.



Co-authored-by: Christian Merten <christian@merten.dev>

Following the pattern of #19065, we introduce a `Hom` structure for morphisms in `SemiRingCat`, `CommSemiRingCat`, `RingCat` and `CommRingCat` allowing for many `simp`lified proofs and reducing the need of `erw`.

Besides the additional explicitness in form of `ofHom` and `Hom.hom`, the main regression is friction with the `FunLike` instance from the general `ConcreteCategory` API, causing the need for explicit `rw`s between `f.hom x` and `(forget RingCat).map f x`. This regression can be fixed by replacing the general `ConcreteCategory.instFunLike` by a `CoeFun` (or `FunLike`) instance that is part of the `ConcreteCategory` data.

Co-authored-by: Anne Baanen <anne@anne.mx>



Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>