∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections],
  CommMonCat.forget₂CreatesLimit F =
    CategoryTheory.createsLimitOfReflectsIso fun c' t =>
      {
        liftedCone :=
          {
            pt :=
              CommMonCat.of
                (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommMonCat))).pt,
            π :=
              {
                app := fun j =>
                  CommMonCat.ofHom (MonCat.limitπMonoidHom (F.comp (CategoryTheory.forget₂ CommMonCat MonCat)) j),
                naturality := ⋯ } },
        validLift :=
          (MonCat.HasLimits.limitConeIsLimit (F.comp (CategoryTheory.forget₂ CommMonCat MonCat))).uniqueUpToIso t,
        makesLimit :=
          CategoryTheory.Limits.IsLimit.ofFaithful (CategoryTheory.forget₂ CommMonCat MonCat)
            (MonCat.HasLimits.limitConeIsLimit (F.comp (CategoryTheory.forget₂ CommMonCat MonCat)))
            (fun x =>
              {
                hom' :=
                  {
                    toFun := fun v =>
                      EquivLike.coe
                        (equivShrink
                          ↑((F.comp (CategoryTheory.forget₂ CommMonCat MonCat)).comp
                                (CategoryTheory.forget MonCat)).sections)
                        ⟨fun j =>
                          ((CategoryTheory.forget MonCat).mapCone
                                  ((CategoryTheory.forget₂ CommMonCat MonCat).mapCone x)).π.app
                            j v,
                          ⋯⟩,
                    map_one' := ⋯, map_mul' := ⋯ } })
            ⋯ }