∀ {X : Type u} [inst : Group X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalGroup X] [inst_3 : CompactSpace X]
  [inst_4 : TotallyDisconnectedSpace X],
  ProfiniteGrp.ofHom (ContinuousMonoidHom.id X) = CategoryTheory.CategoryStruct.id (ProfiniteGrp.of X)