-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Cofiltered (goal)
Goal:
J : Type v
inst : Category.{w, v} J
inst_1 : IsCofiltered.{w, v} J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set (↑(F.obj j) : Type (max u v)))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set (↑(F.obj i) : Type (max u v))), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat :
  ∀ (i j : J) (f : i ⟶ j) (V : Set (↑(F.obj j) : Type (max u v))) (_hV : V ∈ T 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))) ⁻¹'
        V ∈
      T i
U0 : Set (↑C.pt : Type (max u v))
h :
  Membership.mem (γ := Set (Set (↑C.pt : Type (max u v))))
      {U : Set (↑C.pt : Type (max u v)) |
        ∃ (j : J),
          ∃ V ∈ T j,
            U =
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                      (CC := carrier) (C.π.app j)) :
                  (a : (↑(((Functor.const J).obj C.pt).obj j) : Type (max u v))) → (↑(F.obj j) : Type (max u v))) ⁻¹'
                V}
      U0 →
    Membership.mem (γ := Set (Set (↑C.pt : Type (max u v))))
      {S : Set (↑C.pt : Type (max u v)) |
        ∃ (U : (i : J) → Set (↑(F.obj i) : Type (max u v))) (F_1 : Finset J),
          (∀ i ∈ F_1, U i ∈ T i) ∧
            S =
              ⋂ i ∈ F_1,
                (fun (x : (↑C.pt : Type (max u v))) ↦
                    (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                          (CC := carrier) (C.π.app i) :
                        (a : (↑(((Functor.const J).obj C.pt).obj i) : Type (max u v))) → (↑(F.obj i) : Type (max u v)))
                      x) ⁻¹'
                  U i}
      U0
⊢ Membership.mem (γ := Set (Set (↑C.pt : Type (max u v))))
      {U : Set (↑C.pt : Type (max u v)) |
        ∃ (j : J),
          ∃ V ∈ T j,
            U =
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                      (CC := carrier) (C.π.app j)) :
                  (a : (↑(((Functor.const J).obj C.pt).obj j) : Type (max u v))) → (↑(F.obj j) : Type (max u v))) ⁻¹'
                V}
      U0 ↔
    Membership.mem (γ := Set (Set (↑C.pt : Type (max u v))))
      {S : Set (↑C.pt : Type (max u v)) |
        ∃ (U : (i : J) → Set (↑(F.obj i) : Type (max u v))) (F_1 : Finset J),
          (∀ i ∈ F_1, U i ∈ T i) ∧
            S =
              ⋂ i ∈ F_1,
                (fun (x : (↑C.pt : Type (max u v))) ↦
                    (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                          (CC := carrier) (C.π.app i) :
                        (a : (↑(((Functor.const J).obj C.pt).obj i) : Type (max u v))) → (↑(F.obj i) : Type (max u v)))
                      x) ⁻¹'
                  U i}
      U0
have h₁ : Membership.mem (γ := Set (Set (↑C.pt : Type (max u v))))
    {S : Set (↑C.pt : Type (max u v)) |
      ∃ (U : (i : J) → Set (↑(F.obj i) : Type (max u v))) (F_1 : Finset J),
        (∀ i ∈ F_1, U i ∈ T i) ∧
          S =
            ⋂ i ∈ F_1,
              (fun (x : (↑C.pt : Type (max u v))) ↦
                  (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                        (CC := carrier) (C.π.app i) :
                      (a : (↑(((Functor.const J).obj C.pt).obj i) : Type (max u v))) → (↑(F.obj i) : Type (max u v)))
                    x) ⁻¹'
                U i}
    U0 →
  Membership.mem (γ := Set (Set (↑C.pt : Type (max u v))))
    {U : Set (↑C.pt : Type (max u v)) |
      ∃ (j : J),
        ∃ V ∈ T j,
          U =
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                    carrier) (C.π.app j)) :
                (a : (↑(((Functor.const J).obj C.pt).obj j) : Type (max u v))) → (↑(F.obj j) : Type (max u v))) ⁻¹'
              V}
    U0
Tactic: constructor