-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
i j : J
f : i ⟶ j
⊢ {
      hom' :=
        {
          toFun :=
            fun
              (x :
                (↑((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 u v))) ↦
            (↑x :
                (j : J) →
                  (↑(compHausToTop.obj
                        (profiniteToCompHaus.obj ((forget₂ ProfiniteGrp.{max u v} Profinite).obj (F.obj j)))) :
                    Type (max u v)))
              j,
          map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ :
          (↑((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 u v)) →ₜ*
            (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
              Type (max u v)) } :
      (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).Hom
        (F.obj j) } =
    {
        hom' :=
          {
            toFun :=
              fun
                (x :
                  (↑((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 u v))) ↦
              (↑x :
                  (j : J) →
                    (↑(compHausToTop.obj
                          (profiniteToCompHaus.obj ((forget₂ ProfiniteGrp.{max u v} Profinite).obj (F.obj j)))) :
                      Type (max u v)))
                i,
            map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ :
            (↑((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 u v)) →ₜ*
              (↑((F.obj i).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                Type (max u v)) } :
        (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).Hom
          (F.obj i) } ≫
      F.map f
have e_hom' : Eq (α :=
  (↑((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 u v)) →
    (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
      Type (max u v)))
  (fun
      (x :
        (↑((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 u v))) ↦
    (↑x :
        (j : J) →
          (↑(compHausToTop.obj (profiniteToCompHaus.obj ((forget₂ ProfiniteGrp.{max u v} Profinite).obj (F.obj j)))) :
            Type (max u v)))
      j)
  fun
    (x :
      (↑((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).toProfinite.toTop
            (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
        Type (max u v))) ↦
  ((F.map f).hom'.toMonoidHom :
      (a : (↑(F.obj i).toProfinite.toTop : Type (max u v))) → (↑(F.obj j).toProfinite.toTop : Type (max u v)))
    (({
              hom' :=
                {
                  toFun :=
                    fun
                      (x :
                        (↑((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 u v))) ↦
                    (↑x :
                        (j : J) →
                          (↑(compHausToTop.obj
                                (profiniteToCompHaus.obj ((forget₂ ProfiniteGrp.{max u v} Profinite).obj (F.obj j)))) :
                            Type (max u v)))
                      i,
                  map_one' := sorry, map_mul' := sorry, continuous_toFun := sorry :
                  (↑((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 u v)) →ₜ*
                    (↑((F.obj i).toProfinite.toTop (P := fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v)) } :
              (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).Hom
                (F.obj i) }.hom'.toMonoidHom :
        (a :
            (↑(ofProfinite (Profinite.limitCone (F ⋙ forget₂ ProfiniteGrp.{max u v} Profinite)).pt).toProfinite.toTop :
              Type (max u v))) →
          (↑(F.obj i).toProfinite.toTop : Type (max u v)))
      x)
Tactic: congr