-- 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
h :
  Eq (α := TopologicalSpace (↑C.pt : Type (max u v))) C.pt.str
    (⨅ (i : J),
      induced (Y := (↑(F.obj i) : Type (max u v)))
        (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)
        (F.obj i).str)
h₁ h₂ :
  Eq (α := 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}
    {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}
⊢ IsTopologicalBasis (α := (↑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}
have h₃ : ∀ (U0 : Set (↑C.pt : Type (max u v))),
  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
Tactic: classical
  convert! IsTopologicalBasis.iInf_induced hT fun j (x : C.pt) => C.π.app j x using 1
  · exact induced_of_isLimit C hC
  ext U0
  constructor
  · rintro ⟨j, V, hV, rfl⟩
    let U : ∀ i, Set (F.obj i) := fun i => if h : i = j then by rw [h]; exact V else Set.univ
    refine ⟨U, {j}, ?_, ?_⟩
    · simp only [Finset.mem_singleton]
      rintro i rfl
      simpa [U]
    · simp [U]
  · rintro ⟨U, G, h1, h2⟩
    obtain ⟨j, hj⟩ := IsCofiltered.inf_objs_exists G
    let g : ∀ e ∈ G, j ⟶ e := fun _ he => (hj he).some
    let Vs : J → Set (F.obj j) := fun e => if h : e ∈ G then F.map (g e h) ⁻¹' U e else Set.univ
    let V : Set (F.obj j) := ⋂ (e : J) (_he : e ∈ G), Vs e
    refine ⟨j, V, ?_, ?_⟩
    · -- An intermediate claim used to apply induction along `G : Finset J` later on.
      have :
        ∀ (S : Set (Set (F.obj j))) (E : Finset J) (P : J → Set (F.obj j)) (_univ : Set.univ ∈ S)
          (_inter : ∀ A B : Set (F.obj j), A ∈ S → B ∈ S → A ∩ B ∈ S)
          (_cond : ∀ (e : J) (_he : e ∈ E), P e ∈ S), (⋂ (e) (_he : e ∈ E), P e) ∈ S := by
        intro S E
        induction E using Finset.induction_on with
        | empty =>
          intro P he _hh
          simpa
        | insert a E _ha hh1 =>
          intro hh2 hh3 hh4 hh5
          rw [Finset.set_biInter_insert]
          refine hh4 _ _ (hh5 _ (Finset.mem_insert_self _ _)) (hh1 _ hh3 hh4 ?_)
          intro e he
          exact hh5 e (Finset.mem_insert_of_mem he)
      -- use the intermediate claim to finish off the goal using `univ` and `inter`.
      refine this _ _ _ (univ _) (inter _) ?_
      intro e he
      dsimp [Vs]
      rw [dif_pos he]
      exact compat j e (g e he) (U e) (h1 e he)
    · -- conclude...
      rw [h2]
      change _ = (C.π.app j) ⁻¹' ⋂ (e : J) (_ : e ∈ G), Vs e
      rw [Set.preimage_iInter]
      apply congrArg
      ext1 e
      rw [Set.preimage_iInter]
      apply congrArg
      ext1 he
      simp [Vs, dif_pos he, ← Set.preimage_comp, ← coe_comp]