∀ {D : Type u_2} {C : Type u_4} [inst : CategoryTheory.Groupoid D] [inst_1 : CategoryTheory.Category.{u_3, u_4} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (F G : CategoryTheory.Functor D C) ⦃X Y : D⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.id (CategoryTheory.Functor D C)).obj G).map f)
      ((CategoryTheory.ihom.coev (F.obj Y)).app (G.obj Y)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev (F.obj X)).app (G.obj X))
      ((((CategoryTheory.MonoidalCategory.tensorLeft F).comp F.closedIhom).obj G).map f)