-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
U :
  Set
    (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
s :
  Set
    ((j :
        OpenNormalSubgroup
          (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) →
      (↑((P.diagram.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 :
                OpenNormalSubgroup
                  (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)) →
              (↑((P.diagram.obj j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)) ↦
        x ∈ limitConePtAux P.diagram) ⁻¹'
      s =
    U
spc :
  (j :
      OpenNormalSubgroup
        (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) →
    (↑((P.diagram.obj j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
hspc : spc ∈ limitConePtAux P.diagram
uDefaultSpec : spc ∈ s
J :
  Finset
    (OpenNormalSubgroup
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
fJ :
  (a :
      OpenNormalSubgroup
        (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) →
    Set
      (↑((P.diagram.obj a).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 :
  (↑J : Set (OpenNormalSubgroup (↑P.toProfinite.toTop : Type u))).pi (α :=
      fun
        (a :
          OpenNormalSubgroup
            (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
              Type u)) ↦
      (↑((P.diagram.obj a).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
      fJ ⊆
    s
M : Subgroup
  (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) :=
  ⨅ (j : ↥J),
    (↑(↑j : OpenNormalSubgroup (↑P.toProfinite.toTop : Type u)).toOpenSubgroup :
      Subgroup (↑P.toProfinite.toTop : Type u))
hM : M.Normal
hMOpen : IsOpen (↑M : Set (↑P.toProfinite.toTop : Type u))
m : OpenNormalSubgroup
  (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) :=
  { toSubgroup := M, isOpen' := hMOpen, isNormal' := ⋯ }
rcases :
  ∀
    (origin :
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (horigin :
      (QuotientGroup.mk' M : (a : (↑P.toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u) ⧸ M) origin =
        spc m),
    (U ∩
        Set.range (ι :=
          (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          (⇑(Hom.hom P.toLimit) :
            (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u))).Nonempty
⊢ (U ∩
      Set.range (ι :=
        (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        (⇑(Hom.hom P.toLimit) :
          (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u))).Nonempty

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

Premises used: QuotientGroup.mk'_surjective