∀ {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)) (j : J),
  ((CategoryTheory.Mon.forget C).mapCone (CategoryTheory.Mon.limitCone F)).π.app j =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl ((CategoryTheory.Mon.forget C).mapCone (CategoryTheory.Mon.limitCone F)).pt).hom
      ((CategoryTheory.Limits.limit.cone (F.comp (CategoryTheory.Mon.forget C))).π.app j)