-- 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
a : FiniteIndexNormalSubgroup (↑G : Type u)
a_in_J : a ∈ (↑J : Set (FiniteIndexNormalSubgroup (↑G : Type u)))
M_to_Na : m ⟶ a := LE.le.hom ⋯
⊢ (↑(etaFn G origin) :
        (j : FiniteIndexNormalSubgroup (↑G : Type u)) → (↑((diagram G).obj j).toProfinite.toTop : Type u))
      a ∈
    fJ a
have h : Membership.mem (α :=
  (fun (a : FiniteIndexNormalSubgroup (↑G : Type u)) ↦
      (↑(((diagram G).obj a).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
    a)
  (fJ a)
  ((Hom.hom ((diagram G).map M_to_Na) :
        (a_1 : (↑((diagram G).obj m).toProfinite.toTop : Type u)) → (↑((diagram G).obj a).toProfinite.toTop : Type u))
      ((↑(etaFn G origin) :
          (j : FiniteIndexNormalSubgroup (↑G : Type u)) → (↑((diagram G).obj j).toProfinite.toTop : Type u))
        m) :
    (↑(((diagram G).obj a).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
Tactic: rw [← (etaFn G origin).property M_to_Na]