awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
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
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 := ⋯, continuous_invFun := ⋯ })) =
      c.ι.app j
⊢ IsColimit c

Tactic:
refine .ofIsoColimit (isColimitCoconeOfForget _ hc) (Cocone.ext ?_ ?_)
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
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)
⊢ Continuous.{u, u} (X :=
    (↑(coconeOfCoconeForget
            (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
              c)).pt :
      Type u))
    (Equiv.toFun
      (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)))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
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)
⊢ Continuous.{u, u} (X := (↑c.pt : Type u))
    (Equiv.invFun
      (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)))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
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)
⊢ (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 TopCat.isoOfHomeo
      { toEquiv := .refl _,
        continuous_toFun := h ▸ by fun_prop,
        continuous_invFun := h ▸ by fun_prop }

Premises used: Homeomorph.mk, TopCat.carrier, TopCat.isoOfHomeo, Equiv.refl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
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)
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 := ⋯, continuous_invFun := ⋯ })) =
    c.ι.app j

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
inst_1 : HasColimit F
⊢ Eq.{u + 1} (α := TopologicalSpace (↑(colimit F) : Type u)) (colimit F).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) (Y :=
              colimit F) (colimit.ι F j)) :
          (a : (↑(F.obj j) : Type u)) → (↑(colimit F) : Type u))
        (F.obj j).str)

Tactic:
coinduced_of_isColimit _ (colimit.isColimit _)

Premises used: Set.Mem, setOf, CategoryTheory.Limits.colimit.isColimit, TopCat.coinduced_of_isColimit, OrderDual
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
inst_1 : HasColimit F
U : Set (↑(colimit F) : Type u)
⊢ IsOpen U ↔
    ∀ (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) (Y :=
                colimit F) (colimit.ι F j)) :
            (a : (↑(F.obj j) : Type u)) → (↑(colimit F) : Type u)) ⁻¹'
          U)

Tactic:
apply isOpen_iff_of_isColimit _ (colimit.isColimit _)

Premises used: CategoryTheory.Limits.colimit.isColimit, TopCat.isOpen_iff_of_isColimit
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
rw :
  HasColimit F ↔
    HasColimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
⊢ 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

Tactic:
rw [← Types.hasColimit_iff_small_colimitType]

Premises used: CategoryTheory.Limits.Types.hasColimit_iff_small_colimitType
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
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))
mpr :
  HasColimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) →
    HasColimit F
⊢ HasColimit F ↔
    HasColimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))

Tactic:
constructor
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
h : HasColimit F
⊢ HasColimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))

Tactic:
infer_instance
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
h : HasColimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
⊢ HasColimit F

Tactic:
⟨⟨_, isColimitCoconeOfForget _ (colimit.isColimit _)⟩⟩

Premises used: CategoryTheory.Limits.colimit.isColimit, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, TopCat.isColimitCoconeOfForget
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
h : HasColimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
⊢ HasColimit F

Tactic:
exact ⟨⟨_, isColimitCoconeOfForget _ (colimit.isColimit _)⟩⟩
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
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
rw :
  Small.{u, max u v}
    (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)).ColimitType
⊢ HasColimit F

Tactic:
rw [hasColimit_iff_small_colimitType]

Premises used: TopCat.hasColimit_iff_small_colimitType
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
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
⊢ Small.{u, max u v}
    (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)).ColimitType

Tactic:
infer_instance
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
⊢ HasColimits TopCat

Tactic:
TopCat.topCat_hasColimitsOfSize.{u, u}

Premises used: TopCat.topCat_hasColimitsOfSize
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
X : TopCat
f : X ⟶ of PUnit.{u + 1}
⊢ f = default

Tactic:
ext
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
X : TopCat
⊢ Continuous (Y := (↑X : Type u)) fun (x : PEmpty.{u + 1}) ↦ x.elim

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
X : TopCat
f : of PEmpty.{u + 1} ⟶ X
⊢ f = default

Tactic:
ext ⟨⟩
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
X : TopCat
a : ∀ (x : Set PEmpty.{u_1 + 1}), IsOpen x ↔ IsOpen x
⊢ 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

Tactic:
ext
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
X : TopCat
x : Set PEmpty.{u_1 + 1}
⊢ IsOpen x ↔ IsOpen x

Tactic:
simp
-- 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
⊢ IsTopologicalBasis (α := (↑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}

Tactic:
IsTopologicalBasis.iInf_induced hT fun j (x : C.pt) => C.π.app j x

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ConcreteCategory.hom, DFunLike.coe, CategoryTheory.NatTrans.app, IsTopologicalBasis.iInf_induced
-- 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
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₁ :
  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}

Tactic:
convert! IsTopologicalBasis.iInf_induced hT fun j (x : C.pt) => C.π.app j x using 1

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ConcreteCategory.hom, DFunLike.coe, CategoryTheory.NatTrans.app, IsTopologicalBasis.iInf_induced
-- 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
⊢ 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:
induced_of_isLimit C hC

Premises used: Set.Mem, setOf, TopCat.induced_of_isLimit, OrderDual
-- 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
⊢ 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:
exact induced_of_isLimit C hC

Premises used: TopCat.induced_of_isLimit
-- 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
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
⊢ 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:
ext U0
-- 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
rw : Set (↑(F.obj j) : Type (max u v))
⊢ Set (↑(F.obj i) : Type (max u v))

Tactic:
rw [h]