-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
Goal:
G : GrpCat
P : ProfiniteGrp.{u}
f :
  G ⟶
    GrpCat.of (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
X Y :
  OpenNormalSubgroup
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
g : X ⟶ Y
⊢ CategoryTheory.Functor.map
        (Functor.obj
          (Functor.const
            (OpenNormalSubgroup
              (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)))
          (limitCone (diagram G)).pt)
        g ≫
      (limitCone (diagram G)).π.app (preimage f Y) ≫ ofFiniteGrpHom (quotientMap f Y) =
    ((limitCone (diagram G)).π.app (preimage f X) ≫ ofFiniteGrpHom (quotientMap f X)) ≫ P.diagram.map g
have hf : ∀
  (x :
    (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
      (↑((((diagram G ⋙
                    forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
                      (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                          Type u) →ₜ*
                        (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                          Type u))
                      (CC := fun (X : ProfiniteGrp.{u}) ↦
                      (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                        Type u))
                      Profinite (FD :=
                      fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                      C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                        (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                          Type u)))
                      (CD := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))) ⋙
                  profiniteToCompHaus) ⋙
                compHausToTop).obj
            j) :
        Type u))
  (hx :
    Membership.mem (γ :=
      Set
        ((j : FiniteIndexNormalSubgroup (↑G : Type u)) →
          (↑((((diagram G ⋙
                        forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
                          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                              Type u) →ₜ*
                            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                              Type u))
                          (CC := fun (X : ProfiniteGrp.{u}) ↦
                          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                            Type u))
                          Profinite (FD :=
                          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                              Type u),
                            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                              Type u)))
                          (CD :=
                          fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                            Type u))) ⋙
                      profiniteToCompHaus) ⋙
                    compHausToTop).obj
                j) :
            Type u)))
      {u :
        (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
          (↑((((diagram G ⋙
                        forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
                          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                              Type u) →ₜ*
                            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                              Type u))
                          (CC := fun (X : ProfiniteGrp.{u}) ↦
                          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                            Type u))
                          Profinite (FD :=
                          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                              Type u),
                            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                              Type u)))
                          (CD :=
                          fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                            Type u))) ⋙
                      profiniteToCompHaus) ⋙
                    compHausToTop).obj
                j) :
            Type u) |
        ∀ {i j : FiniteIndexNormalSubgroup (↑G : Type u)} (f : i ⟶ j),
          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  ((((diagram G ⋙
                            forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
                              (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u) →ₜ*
                                (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u))
                              (CC := fun (X : ProfiniteGrp.{u}) ↦
                              (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                Type u))
                              Profinite (FD :=
                              fun
                                (x1 x2 :
                                  CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u),
                                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u)))
                              (CD :=
                              fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                Type u))) ⋙
                          profiniteToCompHaus) ⋙
                        compHausToTop).map
                    f) :
                (a :
                    (↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj
                          i) :
                      Type u)) →
                  (↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) :
                    Type u))
              (u i) =
            u j}
      x),
  Eq (α :=
    (↑((P.diagram.obj Y).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    ((Hom.hom
            (CategoryTheory.Functor.map
                (Functor.obj
                  (Functor.const
                    (OpenNormalSubgroup
                      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                        Type u)))
                  (limitCone (diagram G)).pt)
                g ≫
              (limitCone (diagram G)).π.app (preimage f Y) ≫ ofFiniteGrpHom (quotientMap f Y)) :
          (a :
              (↑(((Functor.const (OpenNormalSubgroup (↑P.toProfinite.toTop : Type u))).obj
                            (limitCone (diagram G)).pt).obj
                        X).toProfinite.toTop :
                Type u)) →
            (↑(P.diagram.obj Y).toProfinite.toTop : Type u))
        (Subtype.mk (p :=
          fun
            (x :
              (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
                (↑((((diagram G ⋙
                              forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u) →ₜ*
                                  (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u))
                                (CC := fun (X : ProfiniteGrp.{u}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u))
                                Profinite (FD :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u),
                                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u)))
                                (CD :=
                                fun
                                  (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u))) ⋙
                            profiniteToCompHaus) ⋙
                          compHausToTop).obj
                      j) :
                  Type u)) ↦
          Membership.mem (γ :=
            Set
              ((j : FiniteIndexNormalSubgroup (↑G : Type u)) →
                (↑((((diagram G ⋙
                              forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u) →ₜ*
                                  (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u))
                                (CC := fun (X : ProfiniteGrp.{u}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u))
                                Profinite (FD :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u),
                                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u)))
                                (CD :=
                                fun
                                  (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u))) ⋙
                            profiniteToCompHaus) ⋙
                          compHausToTop).obj
                      j) :
                  Type u)))
            {u :
              (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
                (↑((((diagram G ⋙
                              forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u) →ₜ*
                                  (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u))
                                (CC := fun (X : ProfiniteGrp.{u}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u))
                                Profinite (FD :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u),
                                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u)))
                                (CD :=
                                fun
                                  (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u))) ⋙
                            profiniteToCompHaus) ⋙
                          compHausToTop).obj
                      j) :
                  Type u) |
              ∀ {i j : FiniteIndexNormalSubgroup (↑G : Type u)} (f : i ⟶ j),
                (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier)
                        ((((diagram G ⋙
                                  forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
                                    (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                        Type u) →ₜ*
                                      (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                        Type u))
                                    (CC := fun (X : ProfiniteGrp.{u}) ↦
                                    (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                      Type u))
                                    Profinite (FD :=
                                    fun
                                      (x1 x2 :
                                        CompHausLike fun (X : TopCat.{u}) ↦
                                          TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                    C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                                            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                        Type u),
                                      (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                                            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                        Type u)))
                                    (CD :=
                                    fun
                                      (X :
                                        CompHausLike fun (X : TopCat.{u}) ↦
                                          TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                    (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                                          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                      Type u))) ⋙
                                profiniteToCompHaus) ⋙
                              compHausToTop).map
                          f) :
                      (a :
                          (↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙
                                    compHausToTop).obj
                                i) :
                            Type u)) →
                        (↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙
                                  compHausToTop).obj
                              j) :
                          Type u))
                    (u i) =
                  u j}
            x)
          x hx) :
      (↑((P.diagram.obj Y).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
    ((Hom.hom (((limitCone (diagram G)).π.app (preimage f X) ≫ ofFiniteGrpHom (quotientMap f X)) ≫ P.diagram.map g) :
          (a :
              (↑(((Functor.const (OpenNormalSubgroup (↑P.toProfinite.toTop : Type u))).obj
                            (limitCone (diagram G)).pt).obj
                        X).toProfinite.toTop :
                Type u)) →
            (↑(P.diagram.obj Y).toProfinite.toTop : Type u))
        (Subtype.mk (p :=
          fun
            (x :
              (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
                (↑((((diagram G ⋙
                              forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u) →ₜ*
                                  (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u))
                                (CC := fun (X : ProfiniteGrp.{u}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u))
                                Profinite (FD :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u),
                                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u)))
                                (CD :=
                                fun
                                  (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u))) ⋙
                            profiniteToCompHaus) ⋙
                          compHausToTop).obj
                      j) :
                  Type u)) ↦
          Membership.mem (γ :=
            Set
              ((j : FiniteIndexNormalSubgroup (↑G : Type u)) →
                (↑((((diagram G ⋙
                              forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u) →ₜ*
                                  (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u))
                                (CC := fun (X : ProfiniteGrp.{u}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u))
                                Profinite (FD :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u),
                                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u)))
                                (CD :=
                                fun
                                  (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u))) ⋙
                            profiniteToCompHaus) ⋙
                          compHausToTop).obj
                      j) :
                  Type u)))
            {u :
              (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
                (↑((((diagram G ⋙
                              forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u) →ₜ*
                                  (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u))
                                (CC := fun (X : ProfiniteGrp.{u}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u))
                                Profinite (FD :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u),
                                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                    Type u)))
                                (CD :=
                                fun
                                  (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                  Type u))) ⋙
                            profiniteToCompHaus) ⋙
                          compHausToTop).obj
                      j) :
                  Type u) |
              ∀ {i j : FiniteIndexNormalSubgroup (↑G : Type u)} (f : i ⟶ j),
                (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier)
                        ((((diagram G ⋙
                                  forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
                                    (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                        Type u) →ₜ*
                                      (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                        Type u))
                                    (CC := fun (X : ProfiniteGrp.{u}) ↦
                                    (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                                          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                      Type u))
                                    Profinite (FD :=
                                    fun
                                      (x1 x2 :
                                        CompHausLike fun (X : TopCat.{u}) ↦
                                          TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                    C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                                            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                        Type u),
                                      (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                                            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                        Type u)))
                                    (CD :=
                                    fun
                                      (X :
                                        CompHausLike fun (X : TopCat.{u}) ↦
                                          TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                                    (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                                          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                      Type u))) ⋙
                                profiniteToCompHaus) ⋙
                              compHausToTop).map
                          f) :
                      (a :
                          (↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙
                                    compHausToTop).obj
                                i) :
                            Type u)) →
                        (↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙
                                  compHausToTop).obj
                              j) :
                          Type u))
                    (u i) =
                  u j}
            x)
          x hx) :
      (↑((P.diagram.obj Y).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
Tactic: ext ⟨x, hx⟩