[Merged by Bors] - feat(logic/embedding): use simps

[fpvandoorn]

Some lemmas are slightly reformulated, and have a worse name. But they are (almost) never typed explicitly, since they are simp lemmas (even the occurrences in other files probably came from squeeze_simp).

---

[jcommelin]

Hmmm, I really like simps! Would it be possible to have the new names use coe instead of to_fun? Because, when I see a simp-lemma whose name ends in to_fun I assume that it is a lemma that turns f.to_fun into a coerced (f : _ → _).

Or will this require ugly hackery?

[fpvandoorn]

I'm glad it is useful!

I've been thinking about custom naming of simps.

Just renaming a projection should not be a problem. The nontrivial thing is to decide on the syntax to (1) do this automatically every time and (2) do this once for a specific simps attribute (if we want that).
An even easier thing to do is to is just to rename all projections that are coercions coe (and have no further control over it).

However, there are still questions like

• do we want the lemma name coe_foo or foo_coe? The former seems more standard in mathlib, but the latter is probably be more standard for all projections not named coe.
• What to do with multiple projections. For example, the following lemma generated by simps came up in [Merged by Bors] - fix(simps): use coercion for algebra morphisms #4155:

fixed_points.to_alg_hom_to_fun_to_fun : ∀ (G : Type u) (F : Type v) [_inst_4 : group G] [_inst_5 : field F]
[_inst_6 : faithful_mul_semiring_action G F] (g : G) (a : F), ⇑(⇑(to_alg_hom G F) g) a = g • a

If we rename the projections, this might become fixed_points.to_alg_hom_coe_coe. There is already an option to only use the last projection name, so that it would become fixed_points.to_alg_hom_coe. That is satisfactory in this case, but in other cases you might want more freedom (if projection X and then Y is applied, I want the name to be foo_Z instead of foo_X_Y).

[fpvandoorn]

I think this PR can still be merged, and then I'll change the naming scheme for simps in a later PR.

[semorrison]

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed:

• Build mathlib

[bryangingechen]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests