∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {F : Type u_8} [inst_2 : FunLike F X Y] [inst_3 : MulActionSemiHomClass F φ X Y],
  MulActionHom.instCoeTCOfMulActionSemiHomClass = { coe := MulActionSemiHomClass.toMulActionHom }