∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max u_1 u_2})
  (cone : CategoryTheory.Limits.Cone F),
  (TopCat.Hom.hom
          ((Profinite.limitConeIsLimit (F.comp (CategoryTheory.forget₂ ProfiniteGrp.{max u_2 u_1} Profinite))).lift
              ((CategoryTheory.forget₂ ProfiniteGrp.{max u_2 u_1} Profinite).mapCone cone)).hom).toFun
      1 =
    1