coe type linter

Stream: mathlib4

[Johan Commelin]

Just had a discussion with Mario, inspired by @Ruben Van de Veldes https://github.com/leanprover-community/mathlib4/pull/1426/files#r1064671784

Given the way Lean4 handles coes, the underlying function should have the literal same type as the type the coe claims to have. Not just something defeq to it. So Ruben's move/fix should become a general pattern.

Mario says this is something we can lint against. If someone knows how to write that linter, please contribute!