awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (goal)
Goal:
P : ProfiniteGrp.{u}
H :
  OpenNormalSubgroup
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
s :
  Set
    (↑((P.diagram.obj H).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
h : IsOpen s
i :
  (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) ⧸
    (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u))
h_1 : i ∈ s
⊢ Set.preimage (β :=
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) ⧸
        (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))
      QuotientGroup.mk {i} =
    Quotient.out i • (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)).carrier
have h : ∀ (x : (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
  Membership.mem (γ :=
      Set (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      (Set.preimage (β :=
        (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) ⧸
          (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))
        QuotientGroup.mk {i})
      x ↔
    x ∈ Quotient.out i • (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)).carrier
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (goal)
Goal:
P : ProfiniteGrp.{u}
H :
  OpenNormalSubgroup
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
s :
  Set
    (↑((P.diagram.obj H).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
h : IsOpen s
i :
  (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) ⧸
    (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u))
h_1 : i ∈ s
x : (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ (↑x : (↑P.toProfinite.toTop : Type u) ⧸ (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u))) = i ↔
    x ∈ Quotient.out i • (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)).carrier
have h : (Quotient.out i)⁻¹ * x ∈ (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)) ↔
  x ∈ Quotient.out i • (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)).carrier
Tactic: nth_rw 1 [← QuotientGroup.out_eq' i, eq_comm, QuotientGroup.eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (goal)
Goal:
P : ProfiniteGrp.{u}
⊢ DenseRange (X :=
    (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    (α := (↑(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))
have apply : ∀
  (U :
    Set
      (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)),
  IsOpen U →
    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: apply dense_iff_inter_open.mpr
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (hypothesis)
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 :
  Subtype.mk (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) spc hspc ∈
    U
⊢ (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 uDefaultSpec₁ : spc ∈ s
Tactic: simp_rw [← hsv, Set.mem_preimage] at uDefaultSpec
Cleared hypotheses: uDefaultSpec
-- 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
⊢ (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 : ∀
  (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
Tactic: rcases (isOpen_pi_iff.mp hsO) _ uDefaultSpec with ⟨J, fJ, hJ1, hJ2⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (hypothesis)
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))
⊢ (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 hM : M.Normal
Tactic: have hM : M.Normal := Subgroup.normal_iInf_normal fun j => j.1.isNormal'
-- 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
⊢ IsOpen (↑M : Set (↑P.toProfinite.toTop : Type u))
have 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)))
Tactic: rw [Subgroup.coe_iInf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (hypothesis)
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
⊢ (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 hMOpen : 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'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (hypothesis)
Goal:
P : ProfiniteGrp.{u}
⊢ 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))
have 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)))
Tactic: have : IsClosed (Set.range P.toLimit) :=
    P.toLimit.hom.continuous_toFun.isClosedMap.isClosed_range
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (goal)
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)))
⊢ 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))
have 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
Tactic: rw [← Set.range_eq_univ, ← closure_eq_iff_isClosed.mpr this,
    Dense.closure_eq (denseRange_toLimit P)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (goal)
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
⊢ 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))
have 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
Tactic: rw [← Set.range_eq_univ, ← closure_eq_iff_isClosed.mpr this,
    Dense.closure_eq (denseRange_toLimit P)]