-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
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
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))
⊢ 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

Tactic:
ext ⟨x, hx⟩