-- 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
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
this :
  Eq (α :=
    (↑((((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
          (preimage f Y)) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (((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
              (preimage f X))
            ((((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
              (LE.le.hom ⋯)) :
          (a :
              (↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj
                    (preimage f X)) :
                Type u)) →
            (↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj
                  (preimage f Y)) :
              Type u))
        (x (preimage f X)) :
      (↑((((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
            (preimage f Y)) :
        Type u))
    (x (preimage f Y) :
      (↑((((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
            (preimage f Y)) :
        Type u))
hf :
  ∀ (t : (↑G : Type u))
    (ht :
      Eq (α := (↑G : Type u) ⧸ (preimage f X).toSubgroup) (↑t : (↑G : Type u) ⧸ (preimage f X).toSubgroup)
        (x (preimage f X))),
    Eq (α :=
      (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u))
        (FiniteGrp.of
          ((↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) ⧸
            (↑Y.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
              fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (quotientMap f Y) :
            (a :
                (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u))
                  (FiniteGrp.of ((↑G : Type u) ⧸ (preimage f Y).toSubgroup))) →
              (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u))
                (FiniteGrp.of
                  ((↑P.toProfinite.toTop : Type u) ⧸ (↑Y.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))))
          (x (preimage f Y)) :
        (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u))
          (FiniteGrp.of
            ((↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u) ⧸
              (↑Y.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))))
      ((Hom.hom (P.diagram.map g) :
            (a : (↑(P.diagram.obj X).toProfinite.toTop : Type u)) → (↑(P.diagram.obj Y).toProfinite.toTop : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u))
                (CC := fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (quotientMap f X) :
              (a :
                  (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u))
                    (FiniteGrp.of ((↑G : Type u) ⧸ (preimage f X).toSubgroup))) →
                (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u))
                  (FiniteGrp.of
                    ((↑P.toProfinite.toTop : Type u) ⧸ (↑X.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))))
            (x (preimage f X))) :
        (↑((P.diagram.obj Y).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u))
⊢ Eq (α :=
    (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u))
      (FiniteGrp.of
        ((↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) ⧸
          (↑Y.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
            fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (quotientMap f Y) :
          (a :
              (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u))
                (FiniteGrp.of ((↑G : Type u) ⧸ (preimage f Y).toSubgroup))) →
            (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u))
              (FiniteGrp.of
                ((↑P.toProfinite.toTop : Type u) ⧸ (↑Y.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))))
        (x (preimage f Y)) :
      (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u))
        (FiniteGrp.of
          ((↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) ⧸
            (↑Y.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))))
    ((Hom.hom (P.diagram.map g) :
          (a : (↑(P.diagram.obj X).toProfinite.toTop : Type u)) → (↑(P.diagram.obj Y).toProfinite.toTop : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
              fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (quotientMap f X) :
            (a :
                (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u))
                  (FiniteGrp.of ((↑G : Type u) ⧸ (preimage f X).toSubgroup))) →
              (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u))
                (FiniteGrp.of
                  ((↑P.toProfinite.toTop : Type u) ⧸ (↑X.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))))
          (x (preimage f X))) :
      (↑((P.diagram.obj Y).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))

Tactic:
obtain ⟨t, ht⟩ : ∃ g : G, QuotientGroup.mk g = x (preimage f X) :=
        QuotientGroup.mk_surjective (x (preimage f X))

Premises used: QuotientGroup.mk_surjective, ProfiniteGrp.ProfiniteCompletion.preimage