∀ {J : Type u_3} [inst : CategoryTheory.SmallCategory J] {C : Type u_2} [inst_1 : CategoryTheory.Category.{u_1, u_2} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_3 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.Functor J (CategoryTheory.Mon C)) (s : CategoryTheory.Limits.Cone F) (h : J),
  CategoryTheory.CategoryStruct.comp
      {
        hom :=
          CategoryTheory.Limits.limit.lift (F.comp (CategoryTheory.Mon.forget C))
            ((CategoryTheory.Mon.forget C).mapCone s),
        isMonHom_hom := ⋯ }
      ((CategoryTheory.Mon.limitCone F).π.app h) =
    s.π.app h