coe_fn vs CoeFun

Stream: mathlib4

[Winston Yin]

There are a few lemmas in Logic.Equiv.Defs that refer to coe_fn. Should we rename them to CoeFun? For example, coe_fn_injective -> coeFun_injective.

[Gabriel Ebner]

I believe the function symbol here is FunLike.coe, so it should be coe_injective.

[Gabriel Ebner]

But maybe we should rename FunLike.coe (or use a different definition for the result of the coercion).