-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Profinite
j k : J
f : j ⟶ k
⊢ 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
have 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)) sorry))
                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 := sorry,
                            is_hausdorff := sorry, prop := sorry }).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))
                      sorry))
                  j ⟶
                F.obj k) :
          (a :
              (↑(((Functor.const J).obj
                          { toTop := (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop, is_compact := sorry,
                            is_hausdorff := sorry, prop := sorry }).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)))
Tactic: ext ⟨g, p⟩