-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Profinite
j k : J
f : j ⟶ k
h :
  ∀ (g : (j : J) → (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v)))
    (p :
      Membership.mem (γ := Set ((j : J) → (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v))))
        {u : (j : J) → (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v)) |
          ∀ {i j : J} (f : i ⟶ j),
            (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                    TopCat.carrier) (((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f) :
                  (a : (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj i) : Type (max u v))) →
                    (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v)))
                (u i) =
              u j}
        g),
    Eq (α :=
      (↑((F.obj k).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
      ((ConcreteCategory.hom (FC :=
              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))))
              (CC := 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)))
              (CategoryTheory.Functor.map
                  (Functor.obj (Functor.const J)
                    (mk (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))
                      ((CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).pt.toTop (P := fun (x : TopCat) ↦ True))
                      ⋯))
                  f ≫
                InducedCategory.homMk ((CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).π.app k).hom) :
            (a :
                (↑(((Functor.const J).obj
                            { toTop := (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop, is_compact := ⋯,
                              is_hausdorff := ⋯, prop := ⋯ }).obj
                        j).toTop :
                  Type (max u v))) →
              (↑(F.obj k).toTop : Type (max u v)))
          (Subtype.mk (p :=
            fun (x : (j : J) → (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v))) ↦
            Membership.mem (γ :=
              Set ((j : J) → (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v))))
              {u : (j : J) → (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v)) |
                ∀ {i j : J} (f : i ⟶ j),
                  (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                          (CC := TopCat.carrier) (((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f) :
                        (a : (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj i) : Type (max u v))) →
                          (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v)))
                      (u i) =
                    u j}
              x)
            g p) :
        (↑((F.obj k).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
      ((@ConcreteCategory.hom _ _
              (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))))
              (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)))
              (fun (X Y : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                (ContinuousMap.instFunLike :
                  FunLike
                    C((↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)),
                      (↑(Y.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)))
                    (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v))
                    (↑(Y.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v))))
              _ _ (F.obj k)
              (InducedCategory.homMk ((CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).π.app j).hom ≫ F.map f :
                Functor.obj
                    (Functor.obj (Functor.const J)
                      (mk (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))
                        ((CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).pt.toTop (P := fun (x : TopCat) ↦ True))
                        ⋯))
                    j ⟶
                  F.obj k) :
            (a :
                (↑(((Functor.const J).obj
                            { toTop := (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop, is_compact := ⋯,
                              is_hausdorff := ⋯, prop := ⋯ }).obj
                        j).toTop :
                  Type (max u v))) →
              (↑(F.obj k).toTop : Type (max u v)))
          (Subtype.mk (p :=
            fun (x : (j : J) → (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v))) ↦
            Membership.mem (γ :=
              Set ((j : J) → (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v))))
              {u : (j : J) → (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v)) |
                ∀ {i j : J} (f : i ⟶ j),
                  (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                          (CC := TopCat.carrier) (((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f) :
                        (a : (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj i) : Type (max u v))) →
                          (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v)))
                      (u i) =
                    u j}
              x)
            g p) :
        (↑((F.obj k).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
⊢ CategoryTheory.Functor.map
        (Functor.obj (Functor.const J)
          (mk (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))
            ((CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).pt.toTop (P := fun (x : TopCat) ↦ True)) ⋯))
        f ≫
      InducedCategory.homMk ((CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).π.app k).hom =
    InducedCategory.homMk ((CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).π.app j).hom ≫ F.map f

Tactic:
ext ⟨g, p⟩