-- 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' := ⋯ }
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
a :
  OpenNormalSubgroup
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
a_in_J : a ∈ (↑J : Set (OpenNormalSubgroup (↑P.toProfinite.toTop : Type u)))
M_to_Na : m ⟶ a := LE.le.hom ⋯
h :
  Membership.mem (α := (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (P.toFiniteQuotientFunctor.obj a)) (fJ a)
    ((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)) (P.toFiniteQuotientFunctor.map M_to_Na) :
          (a_1 : (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (P.toFiniteQuotientFunctor.obj m)) →
            (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (P.toFiniteQuotientFunctor.obj a))
        (spc m) :
      (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (P.toFiniteQuotientFunctor.obj a))
⊢ Membership.mem (α := (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (P.toFiniteQuotientFunctor.obj a)) (fJ a)
    ((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)) (P.toFiniteQuotientFunctor.map M_to_Na) :
          (a_1 : (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (P.toFiniteQuotientFunctor.obj m)) →
            (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (P.toFiniteQuotientFunctor.obj a))
        ((QuotientGroup.mk' M : (a : (↑P.toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u) ⧸ M) origin) :
      (fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (P.toFiniteQuotientFunctor.obj a))

Tactic:
rw [horigin]