implicit argument agony

Stream: general

[Scott Morrison]

I would like to write

@[simp] lemma map_id (F : (C × D) ⥤ E) (X : C) (Y : D) :
  F.map (𝟙 X, 𝟙 Y) = 𝟙 (F.obj (X, Y)) :=
F.map_id (X, Y)

(complete context here), but I get an error message

type mismatch at application
  prod.mk (𝟙 X)
term
  𝟙 X
has type
  X ⟶ X
but is expected to have type
  ?m_1.fst ⟶ ?m_1.fstLean

and so have to write the rather unpleasant

@[simp] lemma map_id (F : (C × D) ⥤ E) (X : C) (Y : D) :
  @category_theory.functor.map _ _ _ _ F (X, Y) (X, Y) (𝟙 X, 𝟙 Y) = 𝟙 (F.obj (X, Y)) :=
F.map_id (X, Y)

Anyone have ideas to help the elaborator along, here?

[Kenny Lau]

(term : type)

[Scott Morrison]

I've tried that, but can't get anything to work. Did you have a specific suggestion?

[Kenny Lau]

no, sorry

[Chris Hughes]

@[simp] lemma map_id (F : (C × D) ⥤ E) (X : C) (Y : D) :
  F.map ((𝟙 X, 𝟙 Y) : (X, Y) ⟶ (X, Y)) = 𝟙 (F.obj (X, Y)) :=
F.map_id (X, Y)

[Scott Morrison]

Thank you. :-) I should have managed that one...