awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
X : Set (↑c.pt : Type u)
⊢ IsOpen X ↔ TopologicalSpace.IsOpen X
have rw : IsOpen X ↔ TopologicalSpace.IsOpen X
Tactic: rw [← coinduced_of_isColimit c hc, isOpen_fold]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
X : Set (↑c.pt : Type u)
rw : IsOpen X ↔ TopologicalSpace.IsOpen X
⊢ IsOpen X ↔ TopologicalSpace.IsOpen X
have rw₁ : IsOpen X ↔ IsOpen X
Tactic: rw [← coinduced_of_isColimit c hc, isOpen_fold]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
X : Set (↑c.pt : Type u)
⊢ TopologicalSpace.IsOpen X ↔
    ∀ (j : J),
      IsOpen (X := (↑(F.obj j) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
          X)
have simp : TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen X
Tactic: simp only [← isOpen_coinduced]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
X : Type u'
inst_1 : TopologicalSpace X
f : (↑c.pt : Type u) → X
⊢ Continuous f ↔
    ∀ (j : J),
      Continuous (X := (↑(F.obj j) : Type u))
        (f ∘
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)))
have simp : (∀ (s : Set X),
    IsOpen s →
      ∀ (j : J),
        IsOpen (X := (↑(F.obj j) : Type u))
          ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (c.ι.app j)) :
              (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            f ⁻¹' s)) ↔
  ∀ (j : J) (s : Set X),
    IsOpen s →
      IsOpen (X := (↑(F.obj j) : Type u))
        (f ∘
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (c.ι.app j)) :
              (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
          s)
Tactic: simp only [continuous_def, isOpen_iff_of_isColimit _ hc]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
X : Type u'
inst_1 : TopologicalSpace X
f : (↑c.pt : Type u) → X
⊢ (∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)) ↔
    ∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)
have mp : (∀ (s : Set X),
    IsOpen s →
      ∀ (j : J),
        IsOpen (X := (↑(F.obj j) : Type u))
          ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (c.ι.app j)) :
              (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            f ⁻¹' s)) →
  ∀ (j : J) (s : Set X),
    IsOpen s →
      IsOpen (X := (↑(F.obj j) : Type u))
        (f ∘
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (c.ι.app j)) :
              (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
          s)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
X : Type u'
inst_1 : TopologicalSpace X
f : (↑c.pt : Type u) → X
mp :
  (∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)) →
    ∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)
⊢ (∀ (s : Set X),
      IsOpen s →
        ∀ (j : J),
          IsOpen (X := (↑(F.obj j) : Type u))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
              f ⁻¹' s)) ↔
    ∀ (j : J) (s : Set X),
      IsOpen s →
        IsOpen (X := (↑(F.obj j) : Type u))
          (f ∘
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (c.ι.app j)) :
                (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            s)
have mpr : (∀ (j : J) (s : Set X),
    IsOpen s →
      IsOpen (X := (↑(F.obj j) : Type u))
        (f ∘
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (c.ι.app j)) :
              (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
          s)) →
  ∀ (s : Set X),
    IsOpen s →
      ∀ (j : J),
        IsOpen (X := (↑(F.obj j) : Type u))
          ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (c.ι.app j)) :
              (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
            f ⁻¹' s)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc :
  IsColimit (F := F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
⊢ Nonempty (IsColimit c) ↔
    Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u)) c.pt.str
      (⨆ (j : J),
        coinduced (X := (↑(F.obj j) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u))
          (F.obj j).str)
have refine : (h :
    Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u)) c.pt.str
      (⨆ (j : J),
        coinduced (X := (↑(F.obj j) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u))
          (F.obj j).str)) →
  IsColimit c
Tactic: refine ⟨fun ⟨hc⟩ ↦ coinduced_of_isColimit _ hc, fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc :
  IsColimit (F := F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
h :
  Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u)) c.pt.str
    (⨆ (j : J),
      coinduced (X := (↑(F.obj j) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u))
        (F.obj j).str)
⊢ IsColimit c
have refine_1 : (coconeOfCoconeForget
      (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
        c)).pt ≅
  c.pt
Tactic: refine .ofIsoColimit (isColimitCoconeOfForget _ hc) (Cocone.ext ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc :
  IsColimit (F := F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
h :
  Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u)) c.pt.str
    (⨆ (j : J),
      coinduced (X := (↑(F.obj j) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u))
        (F.obj j).str)
refine_1 :
  (coconeOfCoconeForget
        (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
          c)).pt ≅
    c.pt
⊢ IsColimit c
have refine_2 : ∀ (j : J),
  (coconeOfCoconeForget
              (Functor.mapCocone
                (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)).ι.app
        j ≫
      Iso.hom
        (isoOfHomeo
          (let __Equiv :
            (↑(coconeOfCoconeForget
                      (Functor.mapCocone
                        (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                        c)).pt :
                Type u) ≃
              (↑c.pt : Type u) :=
            Equiv.refl
              (↑(coconeOfCoconeForget
                      (Functor.mapCocone
                        (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                        c)).pt :
                Type u);
          { toEquiv := __Equiv, continuous_toFun := sorry, continuous_invFun := sorry })) =
    c.ι.app j
Tactic: refine .ofIsoColimit (isColimitCoconeOfForget _ hc) (Cocone.ext ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
⊢ HasColimit F ↔
    Small.{u, max u v}
      (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)).ColimitType
have rw : HasColimit F ↔ HasColimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
Tactic: rw [← Types.hasColimit_iff_small_colimitType]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
⊢ HasColimit F ↔
    HasColimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
have mp : HasColimit F → HasColimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
mp :
  HasColimit F →
    HasColimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
⊢ HasColimit F ↔
    HasColimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
have mpr : HasColimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) → HasColimit F
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J_1 : Type v
inst : Category.{w, v} J_1
F_1 : CategoryTheory.Functor.{w, u, v, u + 1} J_1 TopCat
J : Type v
inst_1 : Category.{v_1, v} J
inst_2 : Small.{u, v} J
F : CategoryTheory.Functor.{v_1, u, v, u + 1} J TopCat
⊢ HasColimit F
have rw : Small.{u, max u v}
  (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)).ColimitType
Tactic: rw [hasColimit_iff_small_colimitType]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
X : TopCat
⊢ instTopologicalSpacePEmpty =
    induced
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (isInitialPEmpty.to X)) :
        (a : (↑(of PEmpty.{u_1 + 1}) : Type u_1)) → (↑X : Type u_1))
      X.str
have a : ∀ (x : Set PEmpty.{u_1 + 1}), IsOpen x ↔ IsOpen x
Tactic: ext
-- 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
⊢ 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 : 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)
Tactic: convert! IsTopologicalBasis.iInf_induced hT fun j (x : C.pt) => C.π.app j x using 1
-- 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)
⊢ 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₁ : 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}
Tactic: convert! IsTopologicalBasis.iInf_induced hT fun j (x : C.pt) => C.π.app j x using 1
-- 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
⊢ 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}
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: ext U0