∀ {J : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_1, u_2} C] [inst_2 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.Functor J (CategoryTheory.Mon C))
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (hc : CategoryTheory.Limits.IsLimit c)
  (j : J),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft c.pt
          (hc.lift
            { pt := CategoryTheory.MonoidalCategoryStruct.tensorUnit C,
              π := { app := fun X => CategoryTheory.MonObj.one, naturality := ⋯ } }))
        (hc.lift
          { pt := CategoryTheory.MonoidalCategoryStruct.tensorObj c.1 c.1,
            π :=
              {
                app := fun X =>
                  CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.MonoidalCategoryStruct.tensorHom (c.π.app X) (c.π.app X)) CategoryTheory.MonObj.mul,
                naturality := ⋯ } }))
      (c.π.app j) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor c.pt).hom (c.π.app j)