∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C] (c d : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft d (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
            c).symm.hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor d).hom c)