∀ (G : GrpCat) (P : ProfiniteGrp.{u_1}) (f : G ⟶ GrpCat.of ↑P.toProfinite.toTop),
  (fun f =>
        CategoryTheory.CategoryStruct.comp (ProfiniteGrp.ProfiniteCompletion.eta G)
          ((CategoryTheory.forget₂ ProfiniteGrp.{u_1} GrpCat).map f))
      ((fun f => ProfiniteGrp.ProfiniteCompletion.lift f) f) =
    f