∀ {C : Type u_5} [inst : CategoryTheory.Category.{u_6, u_5} C] {D : Type u_3}
  [inst_1 : CategoryTheory.Category.{u_1, u_3} D] (E : Type u_4) [inst_2 : CategoryTheory.Category.{u_2, u_4} E]
  [inst_3 : CategoryTheory.MonoidalCategory E] (F : CategoryTheory.Functor C D) (X : CategoryTheory.Functor D E),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (((CategoryTheory.Functor.whiskeringLeft C D E).obj F).obj X)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C E))).hom
        (((CategoryTheory.Functor.whiskeringLeft C D E).obj F).obj X))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Iso.refl
            (CategoryTheory.MonoidalCategoryStruct.tensorObj
              (((CategoryTheory.Functor.whiskeringLeft C D E).obj F).obj
                (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor D E)))
              (((CategoryTheory.Functor.whiskeringLeft C D E).obj F).obj X))).hom
        (((CategoryTheory.Functor.whiskeringLeft C D E).obj F).map
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom))