refactor: review the simps projections of OneHom, MulHom, MonoidHom

[YaelDillies]

Make simps generate coe_concreteHom rather thanconcreteHom_apply.

From FLT

---

In fact, I would love to have both the coe_ and _apply projections simultaneously and also to not have to specify simps (config := .asFn)) every single time we want to generate the coe_ projection, but simps seems to not be able to do that? cc @fpvandoorn
I must say, after four years of working on mathlib, I still don't understand how one is supposed to use simps.

[github-actions]

PR summary a8e1e42677

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ coeToMulHom
+ coeToOneHom
+ coe_toMulHom
+ coe_toOneHom
+++ Simps.coe
+++ coe_mk
+++ ext
+++ mk_coe
+++ toFun_eq_coe
- MonoidHom.coeToMulHom
- MonoidHom.coeToOneHom
- MonoidHom.coe_comp
- MonoidHom.coe_copy
- MonoidHom.coe_mk
- MonoidHom.ext
- MonoidHom.mk_coe
- MonoidHom.toFun_eq_coe
- MonoidHom.toMulHom_coe
- MonoidHom.toOneHom_coe
- MulHom.coe_comp
- MulHom.coe_copy
- MulHom.coe_mk
- MulHom.ext
- MulHom.mk_coe
- MulHom.toFun_eq_coe
- OneHom.coe_comp
- OneHom.coe_copy
- OneHom.coe_mk
- OneHom.ext
- OneHom.mk_coe
- OneHom.toFun_eq_coe
-+-+ coe_inclusion

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[fpvandoorn]

Yes, the state of simps is not ideal. I don't have time to develop it further, but there are some unintuitive behaviors and useful missing features.
You cannot specify configuration options in initialize_simps_projections, although this has been requested before. I added #19895 as a tracking issue.

You can do what you want in a verbose way:

-- the `-apply` means that `simps` doesn't generate this lemma by default
initialize_simps_projections OneHom (toFun → coe, as_prefix coe, toFun → apply, -apply)


-- the second `simps` call generates the `apply` lemma anyway
@[simps -fullyApplied, simps apply]
def something : OneHom _ _

Once #19895 is implemented you could enable both by default (this will generate 2^n lemmas if you have n nested OneHoms in your conclusion).