∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat),
  CommGrpCat.forget_createsLimit F =
    CategoryTheory.createsLimitOfNatIso
      (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ CommGrpCat GrpCat).comp (CategoryTheory.forget GrpCat)))