-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
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' := ⋯ }
origin : (↑G : Type u)
horigin : (QuotientGroup.mk' M : (a : (↑G : Type u)) → (↑G : Type u) ⧸ M) origin = spc m
⊢ etaFn G origin ∈ U
have h : Membership.mem (γ :=
  Set
    (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
  (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)
  (etaFn G origin)
Tactic: rw [← hsv]