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

Tactic:
ext ⟨x, hx⟩