∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J Profinite)
  (s : CategoryTheory.Limits.Cone F) (j : J),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.InducedCategory.homMk
        ((CompHaus.limitConeIsLimit (F.comp profiniteToCompHaus)).lift (profiniteToCompHaus.mapCone s)).hom)
      ((Profinite.limitCone F).π.app j) =
    s.π.app j