-- 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
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
h :
  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)
            (𝟙 (mk (P := fun (x : TopCat) ↦ True) (TopCat.limitCone.{v, u, v} FF).pt trivial) ≫
              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 (α := (↑((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)))

Tactic:
simp only [Functor.const_obj_map]

Premises used: CategoryTheory.Functor.const_obj_map