awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
Goal:
G : GrpCat
U :
  Set
    (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
s :
  Set
    ((j : FiniteIndexNormalSubgroup (↑G : Type u)) →
      (↑(((diagram G).obj j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
hsO : IsOpen s
hsv :
  Subtype.val (p :=
        fun
          (x :
            (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
              (↑(((diagram G).obj j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)) ↦
        x ∈ limitConePtAux (diagram G)) ⁻¹'
      s =
    U
spc :
  (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
    (↑(((diagram G).obj j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec :
  (↑(Subtype.mk (p :=
          fun
            (x :
              (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
                (↑(((diagram G).obj j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)) ↦
          x ∈ limitConePtAux (diagram G)) spc hspc) :
      (j : FiniteIndexNormalSubgroup (↑G : Type u)) → (↑((diagram G).obj j).toProfinite.toTop : Type u)) ∈
    s
J : Finset (FiniteIndexNormalSubgroup (↑G : Type u))
fJ :
  (a : FiniteIndexNormalSubgroup (↑G : Type u)) →
    Set
      (↑(((diagram G).obj a).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
hJ1 :
  ∀ a ∈ J,
    IsOpen (fJ a) ∧
      (↑(Subtype.mk (p :=
                fun
                  (x :
                    (j : FiniteIndexNormalSubgroup (↑G : Type u)) →
                      (↑(((diagram G).obj j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                        Type u)) ↦
                x ∈ limitConePtAux (diagram G)) spc hspc) :
            (j : FiniteIndexNormalSubgroup (↑G : Type u)) → (↑((diagram G).obj j).toProfinite.toTop : Type u))
          a ∈
        fJ a
hJ2 :
  (↑J : Set (FiniteIndexNormalSubgroup (↑G : Type u))).pi (α := fun (a : FiniteIndexNormalSubgroup (↑G : Type u)) ↦
      (↑(((diagram G).obj a).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
      fJ ⊆
    s
M : Subgroup (↑G : Type u) := ⨅ (j : ↥J), (↑j : FiniteIndexNormalSubgroup (↑G : Type u)).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup (↑G : Type u) := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : (↑G : Type u)
horigin : (QuotientGroup.mk' M : (a : (↑G : Type u)) → (↑G : Type u) ⧸ M) origin = spc m
⊢ etaFn G origin ∈ U ∩ Set.range (etaFn G)
have h : etaFn G origin ∈ U
Tactic: refine ⟨?_, origin, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
Goal:
G : GrpCat
P : ProfiniteGrp.{u}
f g : completion G ⟶ P
h :
  Eq (α :=
    G ⟶
      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))
        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)
    (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))
        g)
⊢ f = g
have hf : ∀
  (x :
    (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)),
  Eq (α := (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((Hom.hom f : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u)) x :
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((Hom.hom g : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u)) x :
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
Goal:
G : GrpCat
P : ProfiniteGrp.{u}
f g : completion G ⟶ P
h :
  Eq (α :=
    G ⟶
      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))
        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)
    (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))
        g)
x :
  (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
⊢ Eq (α :=
    (x :
        (↑((completion G).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 f) : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u))
    (⇑(Hom.hom g) : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u))
have hf : Eq (α :=
  (↑G : Type u) →
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
  ((⇑(Hom.hom f) : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u)) ∘ etaFn G)
  ((⇑(Hom.hom g) : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u)) ∘ etaFn G)
Tactic: refine (denseRange (G := G)).equalizer f.hom.continuous_toFun g.hom.continuous_toFun ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
Goal:
G : GrpCat
P : ProfiniteGrp.{u}
f g : completion G ⟶ P
h :
  Eq (α :=
    G ⟶
      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))
        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)
    (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))
        g)
x :
  (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
⊢ Eq (α :=
    (↑G : Type u) →
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((⇑(Hom.hom f) : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u)) ∘ etaFn G)
    ((⇑(Hom.hom g) : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u)) ∘ etaFn G)
have hf : ∀ (y : (↑G : Type u)),
  Eq (α := (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (((⇑(Hom.hom f) : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u)) ∘ etaFn G)
      y)
    (((⇑(Hom.hom g) : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u)) ∘ etaFn G)
      y)
Tactic: funext y
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
Goal:
G : GrpCat
⊢ ProfiniteCompletion.lift (𝟙 G ≫ ProfiniteCompletion.eta G) = 𝟙 (ProfiniteCompletion.completion G)
have h : Eq (α :=
  G ⟶
    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 G))
  (ProfiniteCompletion.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))
      (ProfiniteCompletion.lift (𝟙 G ≫ ProfiniteCompletion.eta G)))
  (ProfiniteCompletion.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))
      (𝟙 (ProfiniteCompletion.completion G)))
Tactic: apply ProfiniteCompletion.lift_unique
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
Goal:
X Y Z : GrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ ProfiniteCompletion.lift ((f ≫ g) ≫ ProfiniteCompletion.eta Z) =
    ProfiniteCompletion.lift (f ≫ ProfiniteCompletion.eta Y) ≫ ProfiniteCompletion.lift (g ≫ ProfiniteCompletion.eta Z)
have 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)))
Tactic: apply ProfiniteCompletion.lift_unique
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (goal)
Goal:
P : ProfiniteGrp.{u}
⊢ 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))
have 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
Tactic: apply continuous_induced_rng.mpr (continuous_pi _)
-- 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)
⊢ 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)))
have 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)
Tactic: apply Continuous.mk
-- 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
⊢ 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)
have 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})
Tactic: rw [← (Set.biUnion_preimage_singleton QuotientGroup.mk s)]
-- 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
⊢ 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})
have 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})
Tactic: refine isOpen_iUnion (fun i ↦ isOpen_iUnion (fun _ ↦ ?_))
-- 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
⊢ 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})
have 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
Tactic: convert! IsOpen.leftCoset H.toOpenSubgroup.isOpen' (Quotient.out i)