Implicit function added by Lean unnecessarily

Stream: new members

[Gabin Kolly]

In the pull request #21270, I have a lint error during the build. It is because of this theorem:

@[simp]
theorem eqToHom_comp_apply (h : M = N) (h' : N = P) (m : M) :
    (eqToHom h') (eqToHom h m) = eqToHom (h.trans h') m := sorry

The error is a simp normal form error, apparently because the left hand side simplifies from

  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom h'))
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom h)) m)

to

  (CategoryTheory.eqToHom h') ((CategoryTheory.eqToHom h) m)

which is what I've written!
So Lean adds this hom function implicitly, and then I have an error because it is not necessary and is simplified by the simp tactic. What is the best way to ensure that it does not happen? I tried to add a type coercion, but it does not change anything:

@[simp]
theorem eqToHom_comp_apply (h : M = N) (h' : N = P) (m : M) :
    (eqToHom h' : N → P) ((eqToHom h : M → N) m) = eqToHom (h.trans h') m :=

[Kyle Miller]

The ConcreteCategory's CoeFun instance is docs#CategoryTheory.ConcreteCategory.instCoeFunHomForallToType, and it's what's inserting the hom function.

Your simp lemmas docs#ConcreteCategory.hom_def is then what makes this not be in simp normal form. I don't think that can be a simp lemma given the way ConcreteCategory is set up.