-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
cone : Limits.Cone F
m : cone.pt ⟶ (limitCone.{u, v} F).pt
h : ∀ (j : J), m ≫ (limitCone.{u, v} F).π.app j = cone.π.app j
⊢ Eq (α :=
    Functor.obj
        (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))))
        cone.pt ⟶
      Functor.obj
        (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))))
        (limitCone.{u, v} F).pt)
    (CategoryTheory.Functor.map
      (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))))
      m)
    (CategoryTheory.Functor.map
      (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))))
      (ofHom
        (let __src :
          C((↑((Limits.Cone.pt (F :=
                      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))))
                      (Functor.mapCone
                        (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))))
                        cone)).toTop
                  (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
              Type (max v u)),
            (↑((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))) :=
          TopCat.Hom.hom
            (InducedCategory.Hom.hom
              ((Profinite.limitConeIsLimit
                    (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))))).lift
                (Functor.mapCone
                  (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))))
                  cone)));
        { toFun := __src.toFun, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ })))

Tactic:
simpa using (Profinite.limitConeIsLimit (F ⋙ (forget₂ ProfiniteGrp Profinite))).uniq
      ((forget₂ ProfiniteGrp Profinite).mapCone cone) ((forget₂ ProfiniteGrp Profinite).map m)
      (fun j ↦ congrArg (forget₂ ProfiniteGrp Profinite).map (h j))

Premises used: congrArg, CategoryTheory.Functor.comp, ProfiniteGrp, Profinite.limitConeIsLimit, CategoryTheory.Functor.map, CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.forget₂, Profinite, CategoryTheory.Functor.mapCone