-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (goal)
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' := ⋯ }
⊢ (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
have 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
Tactic: rcases QuotientGroup.mk'_surjective M (spc m) with ⟨origin, horigin⟩