-- 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
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 := ⋯ }) :
            (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)))
⊢ 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)

Tactic:
ext a