-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
U :
  Set
    (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
s :
  Set
    ((j : FiniteIndexNormalSubgroup (↑G : Type u)) →
      (↑(((diagram G).obj j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
hsO : IsOpen s
hsv :
  Subtype.val (p :=
        fun
          (x :
            (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
              (↑(((diagram G).obj j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)) ↦
        x ∈ limitConePtAux (diagram G)) ⁻¹'
      s =
    U
spc :
  (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
    (↑(((diagram G).obj j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec :
  (↑(Subtype.mk (p :=
          fun
            (x :
              (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
                (↑(((diagram G).obj j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)) ↦
          x ∈ limitConePtAux (diagram G)) spc hspc) :
      (j : FiniteIndexNormalSubgroup (↑G : Type u)) → (↑((diagram G).obj j).toProfinite.toTop : Type u)) ∈
    s
J : Finset (FiniteIndexNormalSubgroup (↑G : Type u))
fJ :
  (a : FiniteIndexNormalSubgroup (↑G : Type u)) →
    Set
      (↑(((diagram G).obj a).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
hJ1 :
  ∀ a ∈ J,
    IsOpen (fJ a) ∧
      (↑(Subtype.mk (p :=
                fun
                  (x :
                    (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
                      (↑(((diagram G).obj j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                        Type u)) ↦
                x ∈ limitConePtAux (diagram G)) spc hspc) :
            (j : FiniteIndexNormalSubgroup (↑G : Type u)) → (↑((diagram G).obj j).toProfinite.toTop : Type u))
          a ∈
        fJ a
hJ2 :
  (↑J : Set (FiniteIndexNormalSubgroup (↑G : Type u))).pi (α := fun (a : FiniteIndexNormalSubgroup (↑G : Type u)) ↦
      (↑(((diagram G).obj a).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
      fJ ⊆
    s
M : Subgroup (↑G : Type u) := ⨅ (j : ↥J), (↑j : FiniteIndexNormalSubgroup (↑G : Type u)).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup (↑G : Type u) := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
rcases :
  ∀ (origin : (↑G : Type u)) (horigin : (QuotientGroup.mk' M : (a : (↑G : Type u)) → (↑G : Type u) ⧸ M) origin = spc m),
    (U ∩ Set.range (etaFn G)).Nonempty
⊢ (U ∩ Set.range (etaFn G)).Nonempty

Tactic:
rcases QuotientGroup.mk'_surjective M (spc m) with ⟨origin, horigin⟩

Premises used: QuotientGroup.mk'_surjective