∀ {C : Type u_1} {D : Type u_3} [inst : CategoryTheory.Groupoid C] [inst_1 : CategoryTheory.Category.{u_2, u_3} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.LeftRigidCategory D]
  (F : CategoryTheory.Functor C D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft F
        {
          app := fun x =>
            η_
              ({ obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (CategoryTheory.inv f), map_id := ⋯,
                    map_comp := ⋯ }.obj
                x)
              (F.obj x),
          naturality := ⋯ })
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator F
            { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (CategoryTheory.inv f), map_id := ⋯,
              map_comp := ⋯ }
            F).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          {
            app := fun x =>
              ε_
                ({ obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (CategoryTheory.inv f), map_id := ⋯,
                      map_comp := ⋯ }.obj
                  x)
                (F.obj x),
            naturality := ⋯ }
          F)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor F).hom
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor F).inv