refactor: drop most CoeFun instances

[urkud]

If we define a CoeFun instance instead of a FunLike instance, then Lean unfolds the definition. We don't want this, at least until we find a way to make it work with *HomClasses or find an equally convenient machinery.

• depends on: [Merged by Bors] - Feat: add a FunLike and an EmbeddingLike instance #1488

[kbuzzard]

My guess is that stuff like this will make simp work more like it works in Lean 3. Obviously we don't want to start refactoring mathlib4 before we've ported mathlib3 but these changes look pretty innocuous to me.

[digama0]

Ping @gebner . At first glance this seems incorrect - we just need to make sure that any CoeFun instances are wrapped in functions with the @[coe] attribute. (PS: I'm on holiday this week and I'm probably not going to be spending much time on lean.)

[urkud]

@digama0 Lean 4 does not unfold FunLike.coe, so ((f : M →* N) : M → N) unfolds to FunLike.coe f, not to f.toFun. This allows us to use generic lemmas like map_add, map_sum etc.
In master, ((o : OrderIso α β) : α → β) unfolds to something ugly (AFAIR, it's FunLike.coe o.toOrderEmbedding.toEmbedding but I'm not sure). Of course, we can drop FunLike.coe and unfold it to o.toFun but this will be o.toEquiv.toFun, not just OrderIso.toFun o. This means that we'll need to replicate, e.g., lemmas about OrderEmbedding.
Similarly, without FunLike, ((f : M →* N) : M → N) is f.toOneHom.toFun and there is no clear way to apply MulHom.map_mul here.

An alternative approach is to have something like (non-dependent version for simplicity):

structure BundledHom (α β : Type _) (p : (α → β) → Sort _) [∀ f, Subsingleton (p f)] :=
(toFun : α → β)
(prop : p toFun)

with generic BundledHom.ext etc. Here p takes values in Sort _ to allow finsupp, equiv etc.

[eric-wieser]

Is there a reason this lemma moved? Does this order make it more or less similar to lean3?

[eric-wieser]

Should this have a #noalign or porting comment?

[gebner]

At first glance this seems incorrect - we just need to make sure that any CoeFun instances are wrapped in functions with the @[coe] attribute. (PS: I'm on holiday this week and I'm probably not going to be spending much time on lean.)

I think this PR is the right choice. If we want to have FunLike (and now is probably not the right time to explore other designs) then FunLike.coe should be the unique function symbol we use for hom-to-fun coercion.

[digama0]

Okay, I retract my concern then.

[urkud]

I'll merge master and go over minor concerns tomorrow.

[urkud]

For some reason, the coercion of a MulEquiv gets unfolded. I don't know why.

[semorrison]

This PR/issue depends on:

• [Merged by Bors] - Feat: add a FunLike and an EmbeddingLike instance #1488
  By Dependent Issues (🤖). Happy coding!

[urkud]

All the good parts were moved to other PRs and merged, so I'm closing this one.