awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
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
j : J
V : Set (↑(F.obj j) : Type (max u v))
hV : V ∈ T j
i : J
h : i = j
⊢ Set (↑(F.obj j) : Type (max u v))

Tactic:
exact V
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
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
j : J
V : Set (↑(F.obj j) : Type (max u v))
hV : V ∈ T j
U : (i : J) → Set (↑(F.obj i) : Type (max u v)) := fun (i : J) ↦ if h : i = j then Eq.mpr ⋯ V else Set.univ
⊢ 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}
    ((⇑(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)

Tactic:
⟨U, {j}, ?_, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Singleton.singleton
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
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
j : J
V : Set (↑(F.obj j) : Type (max u v))
hV : V ∈ T j
U : (i : J) → Set (↑(F.obj i) : Type (max u v)) := fun (i : J) ↦ if h : i = j then Eq.mpr ⋯ V else Set.univ
h : ∀ (i : J), Membership.mem (γ := Finset J) {j} i → U i ∈ T i
h₁ :
  Eq (α := Set (↑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 j)) :
        (a : (↑(((Functor.const J).obj C.pt).obj j) : Type (max u v))) → (↑(F.obj j) : Type (max u v))) ⁻¹'
      V)
    (⋂ (i : J),
      ⋂ (_ : Membership.mem (γ := Finset J) {j} i),
        (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)
⊢ 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}
    ((⇑(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)

Tactic:
refine ⟨U, {j}, ?_, ?_⟩
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
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
j : J
V : Set (↑(F.obj j) : Type (max u v))
hV : V ∈ T j
U : (i : J) → Set (↑(F.obj i) : Type (max u v)) := fun (i : J) ↦ if h : i = j then Eq.mpr ⋯ V else Set.univ
h : ∀ (i : J), i = j → U i ∈ T i
⊢ ∀ (i : J), Membership.mem (γ := Finset J) {j} i → U i ∈ T i

Tactic:
simp only [Finset.mem_singleton]

Premises used: Finset.mem_singleton
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
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
i : J
V : Set (↑(F.obj i) : Type (max u v))
hV : V ∈ T i
U : (i : J) → Set (↑(F.obj i) : Type (max u v)) := fun (i_1 : J) ↦ if h : i_1 = i then Eq.mpr ⋯ V else Set.univ
⊢ U i ∈ T i

Tactic:
simpa [U]
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
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
j : J
V : Set (↑(F.obj j) : Type (max u v))
hV : V ∈ T j
U : (i : J) → Set (↑(F.obj i) : Type (max u v)) := fun (i : J) ↦ if h : i = j then Eq.mpr ⋯ V else Set.univ
⊢ Eq (α := Set (↑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 j)) :
        (a : (↑(((Functor.const J).obj C.pt).obj j) : Type (max u v))) → (↑(F.obj j) : Type (max u v))) ⁻¹'
      V)
    (⋂ (i : J),
      ⋂ (_ : Membership.mem (γ := Finset J) {j} i),
        (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:
simp [U]
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
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))
U : (i : J) → Set (↑(F.obj i) : Type (max u v))
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 :
  U0 =
    ⋂ i ∈ G,
      (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
h :
  ∀ (j : J) (hj : ∀ {X : J}, X ∈ G → Nonempty.{w + 1} (j ⟶ X)),
    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))))
    {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:
obtain ⟨j, hj⟩ := IsCofiltered.inf_objs_exists G

Premises used: CategoryTheory.IsCofiltered.inf_objs_exists
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
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))
U : (i : J) → Set (↑(F.obj i) : Type (max u v))
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 :
  U0 =
    ⋂ i ∈ G,
      (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
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty.{w + 1} (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun (x : J) (he : x ∈ G) ↦ ⋯.some
Vs : J → Set (↑(F.obj j) : Type (max u v)) :=
  fun (e : J) ↦
    if h : e ∈ G then
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (F.map (g e h))) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj e) : Type (max u v))) ⁻¹'
        U e
    else Set.univ
V : Set (↑(F.obj j) : Type (max u v)) := ⋂ e ∈ G, Vs e
⊢ 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:
⟨j, V, ?_, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
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))
U : (i : J) → Set (↑(F.obj i) : Type (max u v))
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 :
  U0 =
    ⋂ i ∈ G,
      (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
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty.{w + 1} (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun (x : J) (he : x ∈ G) ↦ ⋯.some
Vs : J → Set (↑(F.obj j) : Type (max u v)) :=
  fun (e : J) ↦
    if h : e ∈ G then
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (F.map (g e h))) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj e) : Type (max u v))) ⁻¹'
        U e
    else Set.univ
V : Set (↑(F.obj j) : Type (max u v)) := ⋂ e ∈ G, Vs e
h : V ∈ T j
h₁ :
  U0 =
    (⇑(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
⊢ 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:
refine ⟨j, V, ?_, ?_⟩
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
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))
U : (i : J) → Set (↑(F.obj i) : Type (max u v))
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 :
  U0 =
    ⋂ i ∈ G,
      (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
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty.{w + 1} (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun (x : J) (he : x ∈ G) ↦ ⋯.some
Vs : J → Set (↑(F.obj j) : Type (max u v)) :=
  fun (e : J) ↦
    if h : e ∈ G then
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (F.map (g e h))) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj e) : Type (max u v))) ⁻¹'
        U e
    else Set.univ
V : Set (↑(F.obj j) : Type (max u v)) := ⋂ e ∈ G, Vs e
S : Set (Set (↑(F.obj j) : Type (max u v)))
P : J → Set (↑(F.obj j) : Type (max u v))
he : Set.univ ∈ S
_hh : ∀ (A B : Set (↑(F.obj j) : Type (max u v))), A ∈ S → B ∈ S → A ∩ B ∈ S
⊢ ∀ (_cond : ∀ (e : J) (_he : Membership.mem (γ := Finset J) ∅ e), P e ∈ S),
    ⋂ (e : J), ⋂ (_ : Membership.mem (γ := Finset J) ∅ e), P e ∈ S

Tactic:
simpa
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
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))
U : (i : J) → Set (↑(F.obj i) : Type (max u v))
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 :
  U0 =
    ⋂ i ∈ G,
      (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
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty.{w + 1} (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun (x : J) (he : x ∈ G) ↦ ⋯.some
Vs : J → Set (↑(F.obj j) : Type (max u v)) :=
  fun (e : J) ↦
    if h : e ∈ G then
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (F.map (g e h))) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj e) : Type (max u v))) ⁻¹'
        U e
    else Set.univ
V : Set (↑(F.obj j) : Type (max u v)) := ⋂ e ∈ G, Vs e
S : Set (Set (↑(F.obj j) : Type (max u v)))
a : J
E : Finset J
_ha : a ∉ E
hh1 :
  ∀ (P : J → Set (↑(F.obj j) : Type (max u v))) (_univ : Set.univ ∈ S)
    (_inter : ∀ (A B : Set (↑(F.obj j) : Type (max u v))), A ∈ S → B ∈ S → A ∩ B ∈ S)
    (_cond : ∀ (e : J) (_he : e ∈ E), P e ∈ S), ⋂ e ∈ E, P e ∈ S
hh2 : J → Set (↑(F.obj j) : Type (max u v))
hh3 : Set.univ ∈ S
hh4 : ∀ (A B : Set (↑(F.obj j) : Type (max u v))), A ∈ S → B ∈ S → A ∩ B ∈ S
hh5 : ∀ (e : J) (_he : e ∈ Insert.insert a E), hh2 e ∈ S
insert : hh2 a ∩ ⋂ x ∈ E, hh2 x ∈ S
⊢ ⋂ e ∈ Insert.insert a E, hh2 e ∈ S

Tactic:
rw [Finset.set_biInter_insert]

Premises used: Finset.set_biInter_insert
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
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))
U : (i : J) → Set (↑(F.obj i) : Type (max u v))
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 :
  U0 =
    ⋂ i ∈ G,
      (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
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty.{w + 1} (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun (x : J) (he : x ∈ G) ↦ ⋯.some
Vs : J → Set (↑(F.obj j) : Type (max u v)) :=
  fun (e : J) ↦
    if h : e ∈ G then
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (F.map (g e h))) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj e) : Type (max u v))) ⁻¹'
        U e
    else Set.univ
V : Set (↑(F.obj j) : Type (max u v)) := ⋂ e ∈ G, Vs e
S : Set (Set (↑(F.obj j) : Type (max u v)))
a : J
E : Finset J
_ha : a ∉ E
hh1 :
  ∀ (P : J → Set (↑(F.obj j) : Type (max u v))) (_univ : Set.univ ∈ S)
    (_inter : ∀ (A B : Set (↑(F.obj j) : Type (max u v))), A ∈ S → B ∈ S → A ∩ B ∈ S)
    (_cond : ∀ (e : J) (_he : e ∈ E), P e ∈ S), ⋂ e ∈ E, P e ∈ S
hh2 : J → Set (↑(F.obj j) : Type (max u v))
hh3 : Set.univ ∈ S
hh4 : ∀ (A B : Set (↑(F.obj j) : Type (max u v))), A ∈ S → B ∈ S → A ∩ B ∈ S
hh5 : ∀ (e : J) (_he : e ∈ insert a E), hh2 e ∈ S
⊢ hh2 a ∩ ⋂ x ∈ E, hh2 x ∈ S

Tactic:
hh4 _ _ (hh5 _ (Finset.mem_insert_self _ _)) (hh1 _ hh3 hh4 ?_)

Premises used: Finset.mem_insert_self