-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ TopCat
X Y : J
f : X ⟶ Y
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 := ⋯ }) :
          (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 := ⋯ } ≫
              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:
exact (a.2 f).symm

Premises used: Eq.symm, Subtype.property