awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
refine :
  ∀ (g : (↑G : Type u)),
    Eq (α :=
        (↑(GrpCat.of
              (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)) :
          Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                GrpCat.carrier) (eta G) :
              (a : (↑G : Type u)) → (↑(GrpCat.of (↑(completion G).toProfinite.toTop : Type u)) : Type u))
            g :
          (↑(GrpCat.of
                (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)) :
            Type u))
        (1 :
          (↑(GrpCat.of
                (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)) :
            Type u)) ↔
      ∀ (H : FiniteIndexNormalSubgroup (↑G : Type u)), g ∈ H
⊢ (∀ (a : (↑G : Type u)),
      Eq (α :=
          (↑(GrpCat.of
                (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)) :
            Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  GrpCat.carrier) (eta G) :
                (a : (↑G : Type u)) → (↑(GrpCat.of (↑(completion G).toProfinite.toTop : Type u)) : Type u))
              a :
            (↑(GrpCat.of
                  (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)) :
              Type u))
          (1 :
            (↑(GrpCat.of
                  (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)) :
              Type u)) →
        a = 1) ↔
    ∀ (g : (↑G : Type u)), (∀ (H : FiniteIndexNormalSubgroup (↑G : Type u)), g ∈ H) → g = 1

Tactic:
refine forall_congr' fun g ↦ imp_congr_left ?_

Premises used: imp_congr_left, forall_congr'
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
g : (↑G : Type u)
rw :
  (∀ (x : FiniteIndexNormalSubgroup (↑G : Type u)),
      Eq.{u + 1} (α :=
        (↑(((diagram G).obj x).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u))
        ((↑((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    GrpCat.carrier) (eta G) :
                  (a : (↑G : Type u)) → (↑(GrpCat.of (↑(completion G).toProfinite.toTop : Type u)) : Type u))
                g) :
            (j : FiniteIndexNormalSubgroup (↑G : Type u)) → (↑((diagram G).obj j).toProfinite.toTop : Type u))
          x)
        ((↑1 : (j : FiniteIndexNormalSubgroup (↑G : Type u)) → (↑((diagram G).obj j).toProfinite.toTop : Type u)) x)) ↔
    ∀ (H : FiniteIndexNormalSubgroup (↑G : Type u)), g ∈ H
⊢ Eq (α :=
      (↑(GrpCat.of
            (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
              Type u)) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := GrpCat.carrier)
              (eta G) :
            (a : (↑G : Type u)) → (↑(GrpCat.of (↑(completion G).toProfinite.toTop : Type u)) : Type u))
          g :
        (↑(GrpCat.of
              (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)) :
          Type u))
      (1 :
        (↑(GrpCat.of
              (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)) :
          Type u)) ↔
    ∀ (H : FiniteIndexNormalSubgroup (↑G : Type u)), g ∈ H

Tactic:
rw [Subtype.ext_iff, funext_iff]

Premises used: funext_iff, Subtype.ext_iff
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
g : (↑G : Type u)
⊢ (∀ (x : FiniteIndexNormalSubgroup (↑G : Type u)),
      Eq.{u + 1} (α :=
        (↑(((diagram G).obj x).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u))
        ((↑((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    GrpCat.carrier) (eta G) :
                  (a : (↑G : Type u)) → (↑(GrpCat.of (↑(completion G).toProfinite.toTop : Type u)) : Type u))
                g) :
            (j : FiniteIndexNormalSubgroup (↑G : Type u)) → (↑((diagram G).obj j).toProfinite.toTop : Type u))
          x)
        ((↑1 : (j : FiniteIndexNormalSubgroup (↑G : Type u)) → (↑((diagram G).obj j).toProfinite.toTop : Type u)) x)) ↔
    ∀ (H : FiniteIndexNormalSubgroup (↑G : Type u)), g ∈ H

Tactic:
forall_congr' fun H ↦ QuotientGroup.eq_one_iff g

Premises used: forall_congr', QuotientGroup.eq_one_iff
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
g : (↑G : Type u)
⊢ (∀ (x : FiniteIndexNormalSubgroup (↑G : Type u)),
      Eq.{u + 1} (α :=
        (↑(((diagram G).obj x).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u))
        ((↑((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    GrpCat.carrier) (eta G) :
                  (a : (↑G : Type u)) → (↑(GrpCat.of (↑(completion G).toProfinite.toTop : Type u)) : Type u))
                g) :
            (j : FiniteIndexNormalSubgroup (↑G : Type u)) → (↑((diagram G).obj j).toProfinite.toTop : Type u))
          x)
        ((↑1 : (j : FiniteIndexNormalSubgroup (↑G : Type u)) → (↑((diagram G).obj j).toProfinite.toTop : Type u)) x)) ↔
    ∀ (H : FiniteIndexNormalSubgroup (↑G : Type u)), g ∈ H

Tactic:
exact forall_congr' fun H ↦ QuotientGroup.eq_one_iff g

Premises used: forall_congr', QuotientGroup.eq_one_iff
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
⊢ Function.Injective (etaFn G) ↔ Group.ResiduallyFinite.{u} (↑G : Type u)

Tactic:
(GrpCat.mono_iff_injective (eta G)).symm.trans (mono_eta_iff_residuallyFinite G)

Premises used: ProfiniteGrp.ProfiniteCompletion.eta, GrpCat.mono_iff_injective, ProfiniteGrp.ProfiniteCompletion.mono_eta_iff_residuallyFinite, ProfiniteGrp.ProfiniteCompletion.etaFn, Iff.trans, Iff.symm
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
apply :
  ∀
    (U :
      Set
        (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)),
    IsOpen U → U.Nonempty → (U ∩ Set.range (etaFn G)).Nonempty
⊢ DenseRange (etaFn G)

Tactic:
apply dense_iff_inter_open.mpr

Premises used: Iff.mpr, dense_iff_inter_open
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
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 ∈
    U
⊢ (↑(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

Tactic:
rw [← hsv, Set.mem_preimage] at uDefaultSpec

Premises used: Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
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
rcases :
  ∀ (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),
    (U ∩ Set.range (etaFn G)).Nonempty
⊢ (U ∩ Set.range (etaFn G)).Nonempty

Tactic:
rcases (isOpen_pi_iff.mp hsO) _ uDefaultSpec with ⟨J, fJ, hJ1, hJ2⟩

Premises used: isOpen_pi_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
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
⊢ M.Normal

Tactic:
have hM : M.Normal := Subgroup.normal_iInf_normal fun j => inferInstance
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
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
hf : ∀ (i : ↥J), (↑i : FiniteIndexNormalSubgroup (↑G : Type u)).FiniteIndex
⊢ M.FiniteIndex

Tactic:
apply Subgroup.finiteIndex_iInf

Premises used: Subgroup.finiteIndex_iInf
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
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
⊢ ∀ (i : ↥J), (↑i : FiniteIndexNormalSubgroup (↑G : Type u)).FiniteIndex

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
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
⊢ M.FiniteIndex

Tactic:
have hMFinite : M.FiniteIndex := by
    apply Subgroup.finiteIndex_iInf
    infer_instance