-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
X_1 Y_1 Z : Type u
inst : Group X_1
inst_1 : TopologicalSpace X_1
inst_2 : IsTopologicalGroup X_1
inst_3 : CompactSpace X_1
inst_4 : TotallyDisconnectedSpace X_1
inst_5 : Group Y_1
inst_6 : TopologicalSpace Y_1
inst_7 : IsTopologicalGroup Y_1
inst_8 : CompactSpace Y_1
inst_9 : TotallyDisconnectedSpace Y_1
inst_10 : Group Z
inst_11 : TopologicalSpace Z
inst_12 : IsTopologicalGroup Z
inst_13 : CompactSpace Z
inst_14 : TotallyDisconnectedSpace Z
X Y : ProfiniteGrp.{u_1}
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget₂ ProfiniteGrp.{u_1} (FC := fun (X Y : ProfiniteGrp.{u_1}) ↦
        (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
            Type u_1) →ₜ*
          (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
            Type u_1))
        (CC := fun (X : ProfiniteGrp.{u_1}) ↦
        (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1))
        Profinite (FD :=
        fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
        C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1),
          (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))
        (CD := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))
      X)
    (CategoryTheory.Functor.map
      (forget₂ ProfiniteGrp.{u_1} (FC := fun (X Y : ProfiniteGrp.{u_1}) ↦
        (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
            Type u_1) →ₜ*
          (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
            Type u_1))
        (CC := fun (X : ProfiniteGrp.{u_1}) ↦
        (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1))
        Profinite (FD :=
        fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
        C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1),
          (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))
        (CD := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))
      f)
i : Functor.obj
    (forget₂ ProfiniteGrp.{u_1} (FC := fun (X Y : ProfiniteGrp.{u_1}) ↦
      (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1) →ₜ*
        (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1))
      (CC := fun (X : ProfiniteGrp.{u_1}) ↦
      (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
        Type u_1))
      Profinite (FD :=
      fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
      C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1),
        (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))
      (CD := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))
    X ≅
  Functor.obj
    (forget₂ ProfiniteGrp.{u_1} (FC := fun (X Y : ProfiniteGrp.{u_1}) ↦
      (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1) →ₜ*
        (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1))
      (CC := fun (X : ProfiniteGrp.{u_1}) ↦
      (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
        Type u_1))
      Profinite (FD :=
      fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
      C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1),
        (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))
      (CD := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget₂ ProfiniteGrp.{u_1} (FC := fun (X Y : ProfiniteGrp.{u_1}) ↦
        (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
            Type u_1) →ₜ*
          (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
            Type u_1))
        (CC := fun (X : ProfiniteGrp.{u_1}) ↦
        (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1))
        Profinite (FD :=
        fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
        C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1),
          (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))
        (CD := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))
      f)
e : (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
    Type u_1) ≃ₜ*
  (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1) :=
  let __src := CompHausLike.homeoOfIso (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) i;
  { toEquiv := __src.toEquiv, map_mul' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsIso f

Tactic:
(ContinuousMulEquiv.toProfiniteGrpIso e).isIso_hom

Premises used: ContinuousMonoidHom.toContinuousMonoidHom, MonoidHomClass.toMonoidHom, ProfiniteGrp.ContinuousMulEquiv.toProfiniteGrpIso, CategoryTheory.Iso.isIso_hom