∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] (X Y : CategoryTheory.Functor C D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X.functorHom Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X.functorHom Y)
          (CategoryTheory.Functor.natTransEquiv.symm (CategoryTheory.CategoryStruct.id Y)))
        {
          app := fun x x_1 =>
            match x_1 with
            | (f, g) => CategoryTheory.Functor.HomObj.comp f g,
          naturality := ⋯ }) =
    CategoryTheory.CategoryStruct.id (X.functorHom Y)