-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ TopCat
X Y : J
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj
        (Functor.obj (Functor.const J)
          (of
            (↑{u : (j : J) → (↑(F.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 := carrier) (F.map f) :
                          (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                        (u i) =
                      u j} :
              Type (max u v))))
        X ⟶
      F.obj Y)
    (CategoryTheory.Functor.map
        (Functor.obj (Functor.const J)
          (of
            (↑{u : (j : J) → (↑(F.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 := carrier) (F.map f) :
                          (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                        (u i) =
                      u j} :
              Type (max u v))))
        f ≫
      ofHom
        {
          toFun :=
            fun
              (u :
                (↑{u : (j : J) → (↑(F.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 := carrier) (F.map f) :
                              (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                            (u i) =
                          u j} :
                  Type (max u v))) ↦
            (↑u : (j : J) → (↑(F.obj j) : Type (max u v))) Y,
          continuous_toFun := ⋯ })
    (ofHom
        {
          toFun :=
            fun
              (u :
                (↑{u : (j : J) → (↑(F.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 := carrier) (F.map f) :
                              (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                            (u i) =
                          u j} :
                  Type (max u v))) ↦
            (↑u : (j : J) → (↑(F.obj j) : Type (max u v))) X,
          continuous_toFun := ⋯ } ≫
      F.map f)
have w : ∀
  (a :
    (↑(Functor.obj
          (Functor.obj (Functor.const J)
            (of
              (↑{u : (j : J) → (↑(F.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 := carrier) (F.map f) :
                            (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                          (u i) =
                        u j} :
                Type (max u v))))
          X) :
      Type (max u v))),
  Eq (α := (↑(F.obj Y) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (X :=
            Functor.obj
              (Functor.obj (Functor.const J)
                (of
                  (↑{u : (j : J) → (↑(F.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 := carrier) (F.map f) :
                                (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                              (u i) =
                            u j} :
                    Type (max u v))))
              X)
            (Y := F.obj Y)
            (CategoryTheory.Functor.map
                (Functor.obj (Functor.const J)
                  (of
                    (↑{u : (j : J) → (↑(F.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 := carrier) (F.map f) :
                                  (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                                (u i) =
                              u j} :
                      Type (max u v))))
                f ≫
              ofHom
                {
                  toFun :=
                    fun
                      (u :
                        (↑{u : (j : J) → (↑(F.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 := carrier) (F.map f) :
                                      (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                                    (u i) =
                                  u j} :
                          Type (max u v))) ↦
                    (↑u : (j : J) → (↑(F.obj j) : Type (max u v))) Y,
                  continuous_toFun := sorry }) :
          (a :
              (↑(((Functor.const J).obj
                        (of
                          (↑{u : (j : J) → (↑(F.obj j) : Type (max u v)) |
                                ∀ {i j : J} (f : i ⟶ j),
                                  (ConcreteCategory.hom (F.map f) :
                                        (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                                      (u i) =
                                    u j} :
                            Type (max u v)))).obj
                    X) :
                Type (max u v))) →
            (↑(F.obj Y) : Type (max u v)))
        a :
      (↑(F.obj Y) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (X :=
            Functor.obj
              (Functor.obj (Functor.const J)
                (of
                  (↑{u : (j : J) → (↑(F.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 := carrier) (F.map f) :
                                (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                              (u i) =
                            u j} :
                    Type (max u v))))
              X)
            (Y := F.obj Y)
            (ofHom
                {
                  toFun :=
                    fun
                      (u :
                        (↑{u : (j : J) → (↑(F.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 := carrier) (F.map f) :
                                      (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                                    (u i) =
                                  u j} :
                          Type (max u v))) ↦
                    (↑u : (j : J) → (↑(F.obj j) : Type (max u v))) X,
                  continuous_toFun := sorry } ≫
              F.map f) :
          (a :
              (↑(((Functor.const J).obj
                        (of
                          (↑{u : (j : J) → (↑(F.obj j) : Type (max u v)) |
                                ∀ {i j : J} (f : i ⟶ j),
                                  (ConcreteCategory.hom (F.map f) :
                                        (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                                      (u i) =
                                    u j} :
                            Type (max u v)))).obj
                    X) :
                Type (max u v))) →
            (↑(F.obj Y) : Type (max u v)))
        a :
      (↑(F.obj Y) : Type (max u v)))
Tactic: ext a