-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
this :
  Eq (α := Set ((j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
    {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
      ∀ {i j : J} (f : i ⟶ j),
        (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))) (F.map f) :
              (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
            (u i) =
          u j}
    (⋂ (i : J),
      ⋂ (j : J),
        ⋂ (f : i ⟶ j),
          {u : (j : J) → (↑((F.obj j).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))) (F.map f) :
                  (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
                (u i) =
              u j})
i j : J
f : i ⟶ j
h :
  Continuous (Y :=
    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
      (F.obj j))
    fun (y : (j : J) → (↑((F.obj j).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))) (F.map f) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
      (y i)
⊢ IsClosed (X := (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
    {u : (j : J) → (↑((F.obj j).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))) (F.map f) :
            (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
              (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
          (u i) =
        u j}
have h₁ : Continuous (Y :=
  (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
    (F.obj j))
  fun (y : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) ↦ y j
Tactic: apply isClosed_eq