-- 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
⊢ 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)

Tactic:
funext fun x => (x.2 f).symm

Premises used: funext, Eq.symm, Subtype.property