-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
i j : J
f : i ⟶ j
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' := ⋯, 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) }.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)
⊢ {
      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

Tactic:
congr