awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
X Y Z : GrpCat
f : X ⟶ Y
g : Y ⟶ Z
h :
  Eq (α :=
    X ⟶
      Functor.obj
        (forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →ₜ*
            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          (CC := fun (X : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
        (ProfiniteCompletion.completion Z))
    (ProfiniteCompletion.eta X ≫
      CategoryTheory.Functor.map
        (forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →ₜ*
            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          (CC := fun (X : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
        (ProfiniteCompletion.lift ((f ≫ g) ≫ ProfiniteCompletion.eta Z)))
    (ProfiniteCompletion.eta X ≫
      CategoryTheory.Functor.map
        (forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →ₜ*
            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          (CC := fun (X : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
        (ProfiniteCompletion.lift (f ≫ ProfiniteCompletion.eta Y) ≫
          ProfiniteCompletion.lift (g ≫ ProfiniteCompletion.eta Z)))
⊢ ProfiniteCompletion.lift ((f ≫ g) ≫ ProfiniteCompletion.eta Z) =
    ProfiniteCompletion.lift (f ≫ ProfiniteCompletion.eta Y) ≫ ProfiniteCompletion.lift (g ≫ ProfiniteCompletion.eta Z)

Tactic:
apply ProfiniteCompletion.lift_unique

Premises used: ProfiniteGrp.ProfiniteCompletion.lift_unique
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
P : ProfiniteGrp.{u}
f :
  G ⟶
    GrpCat.of (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ (fun (f : completion G ⟶ P) ↦
        (eta G ≫
            CategoryTheory.Functor.map
              (forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u) →ₜ*
                  (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u))
                (CC := fun (X : ProfiniteGrp.{u}) ↦
                (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u))
                GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
              f :
          G ⟶
            GrpCat.of
              (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)))
      ((fun
            (f :
              G ⟶
                GrpCat.of
                  (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)) ↦
          lift f)
        f) =
    f

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
apply :
  ∀
    (i :
      OpenNormalSubgroup
        (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
    Continuous (Y :=
      (↑((P.diagram.obj i).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
      fun
        (a :
          (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
      Function.comp (β :=
        (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u))
        (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))
        (⇑P.toLimitFun : (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u)) a i
⊢ Continuous (X :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (Y :=
    (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    (⇑P.toLimitFun : (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u))

Tactic:
apply continuous_induced_rng.mpr (continuous_pi _)

Premises used: Iff.mpr, continuous_pi, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
H :
  OpenNormalSubgroup
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
isOpen_preimage :
  ∀
    (s :
      Set
        (↑((P.diagram.obj H).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)),
    IsOpen s →
      IsOpen (X :=
        (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        ((fun
              (a :
                (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)) ↦
            (↑a : (↑P.toProfinite.toTop : Type u) ⧸ (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))) ⁻¹'
          s)
⊢ Continuous (Y :=
    (↑((P.diagram.obj H).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    fun
      (a : (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
    (↑a : (↑P.toProfinite.toTop : Type u) ⧸ (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))

Tactic:
apply Continuous.mk

Premises used: Continuous.mk
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
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)
isOpen_preimage :
  IsOpen s →
    IsOpen (X :=
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      ((fun
            (a :
              (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)) ↦
          (↑a : (↑P.toProfinite.toTop : Type u) ⧸ (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))) ⁻¹'
        s)
⊢ IsOpen s →
    IsOpen (X :=
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      ((fun
            (a :
              (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)) ↦
          (↑a : (↑P.toProfinite.toTop : Type u) ⧸ (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))) ⁻¹'
        s)

Tactic:
_
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
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
isOpen_preimage :
  IsOpen.{u} (X :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (⋃ y ∈ 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 {y})
⊢ IsOpen (X :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((fun
          (a :
            (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
              Type u)) ↦
        (↑a : (↑P.toProfinite.toTop : Type u) ⧸ (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)))) ⁻¹'
      s)

Tactic:
rw [← (Set.biUnion_preimage_singleton QuotientGroup.mk s)]

Premises used: Set.biUnion_preimage_singleton, QuotientGroup.mk
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
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
⊢ IsOpen.{u} (X :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (⋃ y ∈ 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 {y})

Tactic:
isOpen_iUnion (fun i ↦ isOpen_iUnion (fun _ ↦ ?_))

Premises used: isOpen_iUnion
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
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
isOpen_preimage :
  ∀ i ∈ s,
    IsOpen (X :=
      (↑(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})
⊢ IsOpen.{u} (X :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (⋃ y ∈ 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 {y})

Tactic:
refine isOpen_iUnion (fun i ↦ isOpen_iUnion (fun _ ↦ ?_))

Premises used: isOpen_iUnion
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
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
⊢ IsOpen (Quotient.out i • (↑H.toOpenSubgroup : Subgroup (↑P.toProfinite.toTop : Type u)).carrier)

Tactic:
IsOpen.leftCoset H.toOpenSubgroup.isOpen' (Quotient.out i)

Premises used: Quotient.out, IsOpen.leftCoset, OpenSubgroup.isOpen', OpenNormalSubgroup.toOpenSubgroup
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
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_1 : 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_2 : i ∈ s
h :
  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
⊢ IsOpen (X :=
    (↑(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})

Tactic:
convert! IsOpen.leftCoset H.toOpenSubgroup.isOpen' (Quotient.out i)

Premises used: Quotient.out, IsOpen.leftCoset, OpenSubgroup.isOpen', OpenNormalSubgroup.toOpenSubgroup
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
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_1 : 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_2 : i ∈ s
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
⊢ 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

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
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_1 : 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_2 : i ∈ s
x : (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
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
⊢ (↑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

Tactic:
nth_rw 1 [← QuotientGroup.out_eq' i, eq_comm, QuotientGroup.eq]

Premises used: QuotientGroup.out_eq', QuotientGroup.eq, eq_comm
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
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)
⊢ (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:
Iff.symm (Set.mem_smul_set_iff_inv_smul_mem)

Premises used: Set.mem_smul_set_iff_inv_smul_mem, Iff.symm
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
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)
⊢ (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:
exact Iff.symm (Set.mem_smul_set_iff_inv_smul_mem)

Premises used: Set.mem_smul_set_iff_inv_smul_mem, Iff.symm
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
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
⊢ 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))

Tactic:
apply dense_iff_inter_open.mpr

Premises used: Iff.mpr, dense_iff_inter_open
-- 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 :
  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
⊢ spc ∈ s

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

Premises used: Set.mem_preimage