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_1 c : Cocone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsColimit c
s : Cocone F
j : J
e_2 : (↑s.1 : Type u) = (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u)
x : ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j)
⊢ Eq (α := (↑s.1 : Type u))
    (Function.comp (β := coconePtOfCoconeForget c)
        (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (hc.desc
                (Functor.mapCocone
                  (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
          (a : c.pt) → ToType s.pt)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) x :
      (↑s.1 : Type u))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj s.pt).obj j) : Type u)) x :
      (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u))

Tactic:
exact ConcreteCategory.hom_ext_iff.mp (hc.fac ((forget).mapCocone s) j) x

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.mapCocone, CategoryTheory.ConcreteCategory.hom_ext_iff, CategoryTheory.forget, Iff.mp, TopCat
-- 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 c
c' : Cocone F :=
  coconeOfCoconeForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsColimit c' :=
  isColimitCoconeOfForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isColimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
⊢ ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j

Tactic:
have he (j : J) : c'.ι.app j ≫ e.hom = c.ι.app j :=
    IsColimit.comp_coconePointUniqueUpToIso_hom hc' hc j
-- 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 c
c' : Cocone F :=
  coconeOfCoconeForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsColimit c' :=
  isColimitCoconeOfForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isColimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
apply :
  Eq (α := TopologicalSpace (↑c.pt : Type u))
    (coinduced (X := (↑c'.pt : Type u)) (⇑(homeoOfIso e) : (a : (↑c'.pt : Type u)) → (↑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)
⊢ 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)

Tactic:
apply (homeoOfIso e).coinduced_eq.symm.trans

Premises used: TopCat.homeoOfIso, Eq.symm, Eq.trans, Homeomorph.coinduced_eq
-- 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 c
c' : Cocone F :=
  coconeOfCoconeForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsColimit c' :=
  isColimitCoconeOfForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isColimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
dsimp :
  Eq (α := TopologicalSpace (↑c.pt : Type u))
    (coinduced (X :=
      coconePtOfCoconeForget
        (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c))
      (⇑(homeoOfIso e) : (a : coconePtOfCoconeForget (forget.mapCocone c)) → (↑c.pt : Type u))
      (⨆ (j : J),
        coinduced (X :=
          ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
          (⇑{
                toFun :=
                  (⇑(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)) → (↑c.pt : Type u)) } :
            (a : ToType (F.obj j)) → ToType c.pt)
          (F.obj j).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)) → (↑c.pt : Type u))
        (F.obj j).str)
⊢ Eq (α := TopologicalSpace (↑c.pt : Type u))
    (coinduced (X := (↑c'.pt : Type u)) (⇑(homeoOfIso e) : (a : (↑c'.pt : Type u)) → (↑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)

Tactic:
dsimp [coconeOfCoconeForget_pt, c', topologicalSpaceCoconePtOfCoconeForget]

Premises used: TopCat.coconeOfCoconeForget_pt, TopCat.topologicalSpaceCoconePtOfCoconeForget
-- 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 c
c' : Cocone F :=
  coconeOfCoconeForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsColimit c' :=
  isColimitCoconeOfForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isColimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
simp :
  Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u))
    (⨆ (i : J),
      coinduced (X :=
        coconePtOfCoconeForget
          (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
            c))
        (⇑(homeoOfIso e) : (a : coconePtOfCoconeForget (forget.mapCocone c)) → (↑c.pt : Type u))
        (coinduced (X :=
          ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj i))
          (⇑{
                toFun :=
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) (c.ι.app i)) :
                    (a : (↑(F.obj i) : Type u)) → (↑c.pt : Type u)) } :
            (a : ToType (F.obj i)) → ToType c.pt)
          (F.obj i).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)) → (↑c.pt : Type u))
        (F.obj j).str)
⊢ Eq (α := TopologicalSpace (↑c.pt : Type u))
    (coinduced (X :=
      coconePtOfCoconeForget
        (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c))
      (⇑(homeoOfIso e) : (a : coconePtOfCoconeForget (forget.mapCocone c)) → (↑c.pt : Type u))
      (⨆ (j : J),
        coinduced (X :=
          ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
          (⇑{
                toFun :=
                  (⇑(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)) → (↑c.pt : Type u)) } :
            (a : ToType (F.obj j)) → ToType c.pt)
          (F.obj j).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)) → (↑c.pt : Type u))
        (F.obj j).str)

Tactic:
simp only [coinduced_iSup]

Premises used: coinduced_iSup
-- 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 c
c' : Cocone F :=
  coconeOfCoconeForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsColimit c' :=
  isColimitCoconeOfForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isColimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
simp :
  ⨆ (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 ≫ e.hom)) :
        (a : (↑(F.obj j) : Type u)) → (↑c.pt : Type u))
      (F.obj j).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)) → (↑c.pt : Type u))
      (F.obj j).str

Tactic:
simp only [← he]
-- 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 c
c' : Cocone F :=
  coconeOfCoconeForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsColimit c' :=
  isColimitCoconeOfForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isColimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
conv_rhs :
  Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u))
    (⨆ (i : J),
      coinduced (X :=
        coconePtOfCoconeForget
          (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
            c))
        (⇑(homeoOfIso e) : (a : coconePtOfCoconeForget (forget.mapCocone c)) → (↑c.pt : Type u))
        (coinduced (X :=
          ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj i))
          (⇑{
                toFun :=
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) (c.ι.app i)) :
                    (a : (↑(F.obj i) : Type u)) → (↑c.pt : Type u)) } :
            (a : ToType (F.obj i)) → ToType c.pt)
          (F.obj i).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 ≫ e.hom)) :
          (a : (↑(F.obj j) : Type u)) → (↑c.pt : Type u))
        (F.obj j).str)
⊢ Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u))
    (⨆ (i : J),
      coinduced (X :=
        coconePtOfCoconeForget
          (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
            c))
        (⇑(homeoOfIso e) : (a : coconePtOfCoconeForget (forget.mapCocone c)) → (↑c.pt : Type u))
        (coinduced (X :=
          ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj i))
          (⇑{
                toFun :=
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) (c.ι.app i)) :
                    (a : (↑(F.obj i) : Type u)) → (↑c.pt : Type u)) } :
            (a : ToType (F.obj i)) → ToType c.pt)
          (F.obj i).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)) → (↑c.pt : Type u))
        (F.obj j).str)

Tactic:
conv_rhs => simp only [← he]
-- 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 c
c' : Cocone F :=
  coconeOfCoconeForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsColimit c' :=
  isColimitCoconeOfForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isColimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u))
    (⨆ (i : J),
      coinduced (X :=
        coconePtOfCoconeForget
          (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
            c))
        (⇑(homeoOfIso e) : (a : coconePtOfCoconeForget (forget.mapCocone c)) → (↑c.pt : Type u))
        (coinduced (X :=
          ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj i))
          (⇑{
                toFun :=
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) (c.ι.app i)) :
                    (a : (↑(F.obj i) : Type u)) → (↑c.pt : Type u)) } :
            (a : ToType (F.obj i)) → ToType c.pt)
          (F.obj i).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 ≫ e.hom)) :
          (a : (↑(F.obj j) : Type u)) → (↑c.pt : Type u))
        (F.obj j).str)

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
c : Cocone F
hc : IsColimit c
X : Set (↑c.pt : Type u)
trans : IsOpen X ↔ TopologicalSpace.IsOpen X
trans₁ :
  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)
⊢ 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)

Tactic:
trans (⨆ (j : J), (F.obj j).str.coinduced (c.ι.app j)).IsOpen X

Premises used: TopologicalSpace.IsOpen
-- 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 c
X : Set (↑c.pt : Type u)
rw : IsOpen X ↔ TopologicalSpace.IsOpen X
rw₁ rw₂ : IsOpen X ↔ IsOpen X
⊢ IsOpen X ↔ TopologicalSpace.IsOpen X

Tactic:
rw [← coinduced_of_isColimit c hc, isOpen_fold]

Premises used: TopCat.coinduced_of_isColimit, isOpen_fold
-- 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 c
X : Set (↑c.pt : Type u)
simp : TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen X
⊢ 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)

Tactic:
simp only [← isOpen_coinduced]

Premises used: isOpen_coinduced
-- 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 c
X : Set (↑c.pt : Type u)
⊢ TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen X

Tactic:
apply isOpen_iSup_iff

Premises used: isOpen_iSup_iff
-- 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 c
X : Set (↑c.pt : Type u)
⊢ IsClosed X ↔
    ∀ (j : J),
      IsClosed (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)

Tactic:
simp only [← isOpen_compl_iff, isOpen_iff_of_isColimit _ hc,
    Functor.const_obj_obj, Set.preimage_compl]

Premises used: CategoryTheory.Functor.const_obj_obj, TopCat.isOpen_iff_of_isColimit, Set.preimage_compl, isOpen_compl_iff
-- 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 c
X : Type u'
inst_1 : TopologicalSpace X
f : (↑c.pt : Type u) → X
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)
⊢ 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)))

Tactic:
simp only [continuous_def, isOpen_iff_of_isColimit _ hc]

Premises used: TopCat.isOpen_iff_of_isColimit, continuous_def
-- 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)
⊢ 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)

Tactic:
⟨fun ⟨hc⟩ ↦ coinduced_of_isColimit _ hc, fun h ↦ ⟨?_⟩⟩

Premises used: CategoryTheory.ConcreteCategory.hom, iSup, Nonempty.intro, TopologicalSpace.coinduced, TopCat.coinduced_of_isColimit, TopCat.str, CategoryTheory.Limits.Cocone.ι, Iff.intro, _private.0.TopCat.nonempty_isColimit_iff_eq_coinduced.match_1, Eq, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.Limits.Cocone.pt
-- 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)
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
⊢ 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)

Tactic:
refine ⟨fun ⟨hc⟩ ↦ coinduced_of_isColimit _ hc, fun h ↦ ⟨?_⟩⟩