awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
⊢ IsTopologicalGroup
    (↑((Profinite.limitCone.{v, u}
                (F ⋙
                  forget₂ ProfiniteGrp.{max u v} (FC := fun (X Y : ProfiniteGrp.{max u v}) ↦
                    (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)) →ₜ*
                      (↑(Y.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)))
                    (CC := fun (X : ProfiniteGrp.{max u v}) ↦
                    (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v)))
                    Profinite (FD :=
                    fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)),
                      (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v))))
                    (CD := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v))))).pt.toTop
          (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
      Type (max v u))

Tactic:
inferInstanceAs (IsTopologicalGroup (limitConePtAux F))

Premises used: _private.0.ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap._proof_1
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
j : J
⊢ Continuous (Y :=
    (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
      Type (max u v)))
    fun
      (x :
        (↑((Functor.obj
                    (Functor.obj (Functor.const J)
                      (ofProfinite
                        (Profinite.limitCone.{v, u}
                            (F ⋙
                              forget₂ ProfiniteGrp.{max u v} (FC := fun (X Y : ProfiniteGrp.{max u v}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                    Type (max u v)) →ₜ*
                                  (↑(Y.toProfinite.toTop (P := fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                    Type (max u v)))
                                (CC := fun (X : ProfiniteGrp.{max u v}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                  Type (max u v)))
                                Profinite (FD :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                    Type (max u v)),
                                  (↑(x2.toTop (P := fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                    Type (max u v))))
                                (CD :=
                                fun
                                  (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                                (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                  Type (max u v))))).pt))
                    j).toProfinite.toTop
              (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
          Type (max u v))) ↦
    (↑x :
        (j : J) →
          (↑((((F ⋙ forget₂ ProfiniteGrp.{max u v} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) :
            Type (max u v)))
      j

Tactic:
(continuous_apply j).comp (continuous_iff_le_induced.mpr fun U a => a)

Premises used: Iff.mpr, Continuous.comp, continuous_iff_le_induced, continuous_apply
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
j : J
⊢ Continuous (Y :=
    (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
      Type (max u v)))
    fun
      (x :
        (↑((Functor.obj
                    (Functor.obj (Functor.const J)
                      (ofProfinite
                        (Profinite.limitCone.{v, u}
                            (F ⋙
                              forget₂ ProfiniteGrp.{max u v} (FC := fun (X Y : ProfiniteGrp.{max u v}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                    Type (max u v)) →ₜ*
                                  (↑(Y.toProfinite.toTop (P := fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                    Type (max u v)))
                                (CC := fun (X : ProfiniteGrp.{max u v}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                  Type (max u v)))
                                Profinite (FD :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                    Type (max u v)),
                                  (↑(x2.toTop (P := fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                    Type (max u v))))
                                (CD :=
                                fun
                                  (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                                (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                  Type (max u v))))).pt))
                    j).toProfinite.toTop
              (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
          Type (max u v))) ↦
    (↑x :
        (j : J) →
          (↑((((F ⋙ forget₂ ProfiniteGrp.{max u v} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) :
            Type (max u v)))
      j

Tactic:
exact (continuous_apply j).comp (continuous_iff_le_induced.mpr fun U a => a)

Premises used: Iff.mpr, Continuous.comp, continuous_iff_le_induced, continuous_apply
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
⊢ CompactSpace ↥(limitConePtAux.{u, v} F)

Tactic:
inferInstanceAs (CompactSpace (Profinite.limitCone (F ⋙ (forget₂ ProfiniteGrp Profinite))).pt)

Premises used: Set.Mem, inferInstanceAs, setOf, CategoryTheory.Functor.comp, ProfiniteGrp, CategoryTheory.Limits.Cone.pt, CompactSpace, CategoryTheory.forget₂, Profinite, TopCat.carrier, CompHausLike.toTop, Profinite.limitCone
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
x y :
  (↑((limit.{u, v} F).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max v u)))) :
    Type (max v u))
hxy :
  ∀ (j : J),
    (↑x : (j : J) → (↑(F.obj j).toProfinite.toTop : Type (max u v))) j =
      (↑y : (j : J) → (↑(F.obj j).toProfinite.toTop : Type (max u v))) j
⊢ x = y

Tactic:
Subtype.ext (funext hxy)

Premises used: funext, Subtype.ext
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
j : J
⊢ Eq (α :=
    (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
      Type (max u v)))
    ((↑1 : (j : J) → (↑(F.obj j).toProfinite.toTop : Type (max u v))) j) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
x y :
  (↑((limit.{u, v} F).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max v u)))) :
    Type (max v u))
j : J
⊢ (↑(x * y) : (j : J) → (↑(F.obj j).toProfinite.toTop : Type (max u v))) j =
    (↑x : (j : J) → (↑(F.obj j).toProfinite.toTop : Type (max u v))) j *
      (↑y : (j : J) → (↑(F.obj j).toProfinite.toTop : Type (max u v))) j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : ContinuousMul G
H K : OpenNormalSubgroup G
h : H ≤ K
⊢ H.toFiniteIndexNormalSubgroup ≤ K.toFiniteIndexNormalSubgroup

Tactic:
fun _ hx ↦ h hx

Premises used: Set.Mem
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : ContinuousMul G
H K : OpenNormalSubgroup G
h : H.toFiniteIndexNormalSubgroup = K.toFiniteIndexNormalSubgroup
a :
  Eq.{u_1 + 1} (α := Subgroup G) ((fun (H : OpenNormalSubgroup G) ↦ (↑H.toOpenSubgroup : Subgroup G)) H)
    ((fun (H : OpenNormalSubgroup G) ↦ (↑H.toOpenSubgroup : Subgroup G)) K)
⊢ H = K

Tactic:
apply toSubgroup_injective

Premises used: OpenNormalSubgroup.toSubgroup_injective
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : ContinuousMul G
H K : OpenNormalSubgroup G
h : H.toFiniteIndexNormalSubgroup = K.toFiniteIndexNormalSubgroup
⊢ Eq.{u_1 + 1} (α := Subgroup G) ((fun (H : OpenNormalSubgroup G) ↦ (↑H.toOpenSubgroup : Subgroup G)) H)
    ((fun (H : OpenNormalSubgroup G) ↦ (↑H.toOpenSubgroup : Subgroup G)) K)

Tactic:
congrArg (fun L : FiniteIndexNormalSubgroup G ↦ (L : Subgroup G)) h

Premises used: FiniteIndexNormalSubgroup.toSubgroup, congrArg
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : ContinuousMul G
H K : OpenNormalSubgroup G
h : H.toFiniteIndexNormalSubgroup = K.toFiniteIndexNormalSubgroup
⊢ Eq.{u_1 + 1} (α := Subgroup G) ((fun (H : OpenNormalSubgroup G) ↦ (↑H.toOpenSubgroup : Subgroup G)) H)
    ((fun (H : OpenNormalSubgroup G) ↦ (↑H.toOpenSubgroup : Subgroup G)) K)

Tactic:
exact congrArg (fun L : FiniteIndexNormalSubgroup G ↦ (L : Subgroup G)) h

Premises used: FiniteIndexNormalSubgroup.toSubgroup, congrArg
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
H : FiniteIndexNormalSubgroup (↑G : Type u)
h :
  ∀ (x : (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u)) (x : (↑G : Type u)),
    Eq (α := (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
              fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (X := FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)) (Y :=
              FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup))
              (FiniteGrp.ofHom (QuotientGroup.map H.toSubgroup H.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯)) :
            (a : (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u)) →
              (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
          (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup) : (↑G : Type u) → (↑G : Type u) → Prop) x) :
        (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
              fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (𝟙 (FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup))) :
            (a : (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u)) →
              (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
          (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup) : (↑G : Type u) → (↑G : Type u) → Prop) x) :
        (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
⊢ FiniteGrp.ofHom (QuotientGroup.map H.toSubgroup H.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯) =
    𝟙 (FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup))

Tactic:
ext ⟨x⟩
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
H : FiniteIndexNormalSubgroup (↑G : Type u)
x_1 : (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u)
x : (↑G : Type u)
⊢ Eq (α := (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
            fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (X := FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)) (Y :=
            FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup))
            (FiniteGrp.ofHom (QuotientGroup.map H.toSubgroup H.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯)) :
          (a : (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u)) →
            (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
        (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup) : (↑G : Type u) → (↑G : Type u) → Prop) x) :
      (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
            fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (𝟙 (FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup))) :
          (a : (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u)) →
            (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
        (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup) : (↑G : Type u) → (↑G : Type u) → Prop) x) :
      (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
X Y Z : FiniteIndexNormalSubgroup (↑G : Type u)
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (x : (↑(FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)).toGrp : Type u)) (x : (↑G : Type u)),
    Eq (α := (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
              fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (X := FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)) (Y :=
              FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup))
              (FiniteGrp.ofHom (QuotientGroup.map X.toSubgroup Z.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯)) :
            (a : (↑(FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)).toGrp : Type u)) →
              (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
          (Quot.mk (⇑(QuotientGroup.leftRel X.toSubgroup) : (↑G : Type u) → (↑G : Type u) → Prop) x) :
        (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
              fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (X := FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)) (Y :=
              FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup))
              (CategoryStruct.comp (Y := FiniteGrp.of ((↑G : Type u) ⧸ Y.toSubgroup))
                (FiniteGrp.ofHom (QuotientGroup.map X.toSubgroup Y.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯))
                (FiniteGrp.ofHom (QuotientGroup.map Y.toSubgroup Z.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯))) :
            (a : (↑(FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)).toGrp : Type u)) →
              (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
          (Quot.mk (⇑(QuotientGroup.leftRel X.toSubgroup) : (↑G : Type u) → (↑G : Type u) → Prop) x) :
        (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
⊢ Eq (α := FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup) ⟶ FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup))
    (FiniteGrp.ofHom (QuotientGroup.map X.toSubgroup Z.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯))
    (CategoryStruct.comp (Y := FiniteGrp.of ((↑G : Type u) ⧸ Y.toSubgroup))
      (FiniteGrp.ofHom (QuotientGroup.map X.toSubgroup Y.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯))
      (FiniteGrp.ofHom (QuotientGroup.map Y.toSubgroup Z.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯)))

Tactic:
ext ⟨x⟩
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
X Y Z : FiniteIndexNormalSubgroup (↑G : Type u)
f : X ⟶ Y
g : Y ⟶ Z
x_1 : (↑(FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)).toGrp : Type u)
x : (↑G : Type u)
⊢ Eq (α := (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
            fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (X := FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)) (Y :=
            FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup))
            (FiniteGrp.ofHom (QuotientGroup.map X.toSubgroup Z.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯)) :
          (a : (↑(FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)).toGrp : Type u)) →
            (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
        (Quot.mk (⇑(QuotientGroup.leftRel X.toSubgroup) : (↑G : Type u) → (↑G : Type u) → Prop) x) :
      (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
            fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (X := FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)) (Y :=
            FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup))
            (CategoryStruct.comp (Y := FiniteGrp.of ((↑G : Type u) ⧸ Y.toSubgroup))
              (FiniteGrp.ofHom (QuotientGroup.map X.toSubgroup Y.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯))
              (FiniteGrp.ofHom (QuotientGroup.map Y.toSubgroup Z.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯))) :
          (a : (↑(FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)).toGrp : Type u)) →
            (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
        (Quot.mk (⇑(QuotientGroup.leftRel X.toSubgroup) : (↑G : Type u) → (↑G : Type u) → Prop) x) :
      (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
rw :
  (∀ (a : (↑G : Type u)),
      Eq (α :=
          (↑(GrpCat.of
                (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)) :
            Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  GrpCat.carrier) (eta G) :
                (a : (↑G : Type u)) → (↑(GrpCat.of (↑(completion G).toProfinite.toTop : Type u)) : Type u))
              a :
            (↑(GrpCat.of
                  (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)) :
              Type u))
          (1 :
            (↑(GrpCat.of
                  (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)) :
              Type u)) →
        a = 1) ↔
    ∀ (g : (↑G : Type u)), (∀ (H : FiniteIndexNormalSubgroup (↑G : Type u)), g ∈ H) → g = 1
⊢ Mono (eta G) ↔ Group.ResiduallyFinite.{u} (↑G : Type u)

Tactic:
rw [GrpCat.mono_iff_injective, injective_iff_map_eq_one,
    Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup]

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

Tactic:
forall_congr' fun g ↦ imp_congr_left ?_

Premises used: imp_congr_left, forall_congr'