-- 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
⊢ IsClosed (X := (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
    (⋂ (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})
have h : ∀ (i_1 : i ⟶ j),
  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 i_1) :
            (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}
Tactic: apply isClosed_iInter