awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rcases :
  ∀
    (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),
    (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
⊢ (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 (isOpen_pi_iff.mp hsO) _ uDefaultSpec with ⟨J, fJ, hJ1, hJ2⟩

Premises used: isOpen_pi_iff, Iff.mp
-- 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))
⊢ M.Normal

Tactic:
have hM : M.Normal := Subgroup.normal_iInf_normal fun j => j.1.isNormal'
-- 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
rw :
  IsOpen.{u} (X :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (⋂ (i : ↥J),
      (↑(↑(↑i : OpenNormalSubgroup (↑P.toProfinite.toTop : Type u)).toOpenSubgroup :
            Subgroup (↑P.toProfinite.toTop : Type u)) :
        Set (↑P.toProfinite.toTop : Type u)))
⊢ IsOpen (↑M : Set (↑P.toProfinite.toTop : Type u))

Tactic:
rw [Subgroup.coe_iInf]

Premises used: Subgroup.coe_iInf
-- 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
⊢ IsOpen.{u} (X :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (⋂ (i : ↥J),
      (↑(↑(↑i : OpenNormalSubgroup (↑P.toProfinite.toTop : Type u)).toOpenSubgroup :
            Subgroup (↑P.toProfinite.toTop : Type u)) :
        Set (↑P.toProfinite.toTop : Type u)))

Tactic:
isOpen_iInter_of_finite fun i => i.1.1.isOpen'

Premises used: isOpen_iInter_of_finite, OpenSubgroup.isOpen', OpenNormalSubgroup.toOpenSubgroup, Subtype.val
-- 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
⊢ IsOpen.{u} (X :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (⋂ (i : ↥J),
      (↑(↑(↑i : OpenNormalSubgroup (↑P.toProfinite.toTop : Type u)).toOpenSubgroup :
            Subgroup (↑P.toProfinite.toTop : Type u)) :
        Set (↑P.toProfinite.toTop : Type u)))

Tactic:
exact isOpen_iInter_of_finite fun i => i.1.1.isOpen'

Premises used: isOpen_iInter_of_finite
-- 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
⊢ IsOpen (↑M : Set (↑P.toProfinite.toTop : Type u))

Tactic:
have hMOpen : IsOpen (M : Set P) := by
    rw [Subgroup.coe_iInf]
    exact isOpen_iInter_of_finite fun i => i.1.1.isOpen'
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
⊢ IsClosed (X :=
    (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type 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)))

Tactic:
have : IsClosed (Set.range P.toLimit) :=
    P.toLimit.hom.continuous_toFun.isClosedMap.isClosed_range
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
this :
  IsClosed (X :=
    (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type 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)))
rw :
  Eq (α :=
    Set
      (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type 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)))
    Set.univ
rw₁ :
  Eq (α :=
    Set
      (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
    (closure
      (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))))
    Set.univ
rw₂ rw₃ :
  Eq.{u + 1} (α :=
    Set
      (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
    Set.univ Set.univ
⊢ Function.Surjective (α :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (β :=
    (↑((limit P.diagram).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))

Tactic:
rw [← Set.range_eq_univ, ← closure_eq_iff_isClosed.mpr this,
    Dense.closure_eq (denseRange_toLimit P)]

Premises used: Iff.mpr, Set.range_eq_univ, closure_eq_iff_isClosed, ProfiniteGrp.denseRange_toLimit, Dense.closure_eq
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
rw : ∀ x ∈ (Hom.hom P.toLimit).ker, x = 1
⊢ Function.Injective (α :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (β :=
    (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    (⇑(Hom.hom P.toLimit).toMonoidHom :
      (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u))

Tactic:
rw [← MonoidHom.ker_eq_bot_iff, Subgroup.eq_bot_iff_forall]

Premises used: Subgroup.eq_bot_iff_forall, MonoidHom.ker_eq_bot_iff
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
x : (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h : x ∈ (Hom.hom P.toLimit).ker
by_contra : ∀ (xne1 : ¬x = 1), False
⊢ x = 1

Tactic:
by_contra xne1
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
x : (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h : x ∈ (Hom.hom P.toLimit).ker
xne1 : ¬x = 1
rcases :
  ∀
    (H :
      OpenNormalSubgroup
        (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (hH : (↑H : Set (↑P.toProfinite.toTop : Type u)) ⊆ {x}ᶜ), False
⊢ False

Tactic:
rcases exist_openNormalSubgroup_sub_open_nhds_of_one (isOpen_compl_singleton)
    (Set.mem_compl_singleton_iff.mpr fun a => xne1 a.symm) with ⟨H, hH⟩

Premises used: Iff.mpr, isOpen_compl_singleton, Set.mem_compl_singleton_iff, ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one, Eq.symm
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
x : (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h : x ∈ (Hom.hom P.toLimit).ker
xne1 : ¬x = 1
H :
  OpenNormalSubgroup
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hH : (↑H : Set (↑P.toProfinite.toTop : Type u)) ⊆ {x}ᶜ
⊢ False

Tactic:
hH ((QuotientGroup.eq_one_iff x).mp (congrFun (Subtype.val_inj.mpr h) H)) rfl

Premises used: Iff.mpr, Subtype.val_inj, congrFun, Iff.mp, QuotientGroup.eq_one_iff, rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
x : (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h : x ∈ (Hom.hom P.toLimit).ker
xne1 : ¬x = 1
H :
  OpenNormalSubgroup
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hH : (↑H : Set (↑P.toProfinite.toTop : Type u)) ⊆ {x}ᶜ
⊢ False

Tactic:
exact hH ((QuotientGroup.eq_one_iff x).mp (congrFun (Subtype.val_inj.mpr h) H)) rfl

Premises used: Iff.mpr, Subtype.val_inj, congrFun, Iff.mp, QuotientGroup.eq_one_iff, rfl