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
h : HasLimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
⊢ HasLimit F

Tactic:
exact ⟨⟨_, isLimitConeOfForget _ (limit.isLimit _)⟩⟩
-- 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)).sections :
      Type (max u v))
⊢ HasLimit F

Tactic:
rw [hasLimit_iff_small_sections]

Premises used: TopCat.hasLimit_iff_small_sections
-- 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)).sections :
      Type (max u v))

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
⊢ HasLimits TopCat

Tactic:
TopCat.topCat_hasLimitsOfSize.{u, u}

Premises used: TopCat.topCat_hasLimitsOfSize
-- 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 ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
j : J
rw :
  coinduced (X := (↑(F.1 j) : Type u))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
      (str (F.1 j)) ≤
    topologicalSpaceCoconePtOfCoconeForget c
⊢ Continuous (X := (↑(F.1 j) : Type u)) (Y := coconePtOfCoconeForget c)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) :
      (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))

Tactic:
rw [continuous_iff_coinduced_le]

Premises used: continuous_iff_coinduced_le
-- 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 ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
j : J
dsimp :
  LE.le (α := TopologicalSpace (coconePtOfCoconeForget c))
    (coinduced (X := (↑(F.1 j) : Type u))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) (str (F.1 j)))
    (⨆ (j : J),
      coinduced (X := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) (F.obj j).str)
⊢ coinduced (X := (↑(F.1 j) : Type u))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
      (str (F.1 j)) ≤
    topologicalSpaceCoconePtOfCoconeForget c

Tactic:
dsimp [topologicalSpaceCoconePtOfCoconeForget]

Premises used: 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 ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
j : J
⊢ LE.le (α := TopologicalSpace (coconePtOfCoconeForget c))
    (coinduced (X := (↑(F.1 j) : Type u))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) (str (F.1 j)))
    (⨆ (j : J),
      coinduced (X := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) (F.obj j).str)

Tactic:
le_iSup (fun j ↦ (F.obj j).str.coinduced _) j

Premises used: le_iSup, TopologicalSpace.coinduced, TopCat.str, CategoryTheory.Functor.obj
-- 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 ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
j : J
⊢ LE.le (α := TopologicalSpace (coconePtOfCoconeForget c))
    (coinduced (X := (↑(F.1 j) : Type u))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) (str (F.1 j)))
    (⨆ (j : J),
      coinduced (X := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) (F.obj j).str)

Tactic:
exact le_iSup (fun j ↦ (F.obj j).str.coinduced _) j

Premises used: le_iSup, TopologicalSpace.coinduced, TopCat.str, CategoryTheory.Functor.obj
-- 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 ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
j j' : J
φ : j ⟶ j'
w :
  ∀ (x : (↑(F.obj j) : Type u)),
    Eq (α :=
      (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (of (coconePtOfCoconeForget c))) j') : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (F.map φ ≫
                ofHom
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j')) :
                        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j')) →
                          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j')),
                    continuous_toFun := ⋯ : C((↑(F.1 j') : Type u), coconePtOfCoconeForget c) }) :
            (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj (of (coconePtOfCoconeForget c))).obj j') : Type u))
          x :
        (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (of (coconePtOfCoconeForget c))) j') : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (of (coconePtOfCoconeForget c))) j')
              (ofHom
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) :
                        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j)) →
                          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)),
                    continuous_toFun := ⋯ : C((↑(F.1 j) : Type u), coconePtOfCoconeForget c) } ≫
                CategoryTheory.Functor.map (Functor.obj (Functor.const J) (of (coconePtOfCoconeForget c))) φ) :
            (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj (of (coconePtOfCoconeForget c))).obj j') : Type u))
          x :
        (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (of (coconePtOfCoconeForget c))) j') : Type u))
⊢ F.map φ ≫
      ofHom
        {
          toFun :=
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j')) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j')) →
                (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j')),
          continuous_toFun := ⋯ : C((↑(F.1 j') : Type u), coconePtOfCoconeForget c) } =
    ofHom
        {
          toFun :=
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j)) →
                (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)),
          continuous_toFun := ⋯ : C((↑(F.1 j) : Type u), coconePtOfCoconeForget c) } ≫
      CategoryTheory.Functor.map (Functor.obj (Functor.const J) (of (coconePtOfCoconeForget c))) φ

Tactic:
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 ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
j j' : J
φ : j ⟶ j'
x : (↑(F.obj j) : Type u)
⊢ Eq (α :=
    (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (of (coconePtOfCoconeForget c))) j') : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (F.map φ ≫
              ofHom
                {
                  toFun :=
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j')) :
                      (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j')) →
                        (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j')),
                  continuous_toFun := ⋯ : C((↑(F.1 j') : Type u), coconePtOfCoconeForget c) }) :
          (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj (of (coconePtOfCoconeForget c))).obj j') : Type u))
        x :
      (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (of (coconePtOfCoconeForget c))) j') : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (of (coconePtOfCoconeForget c))) j')
            (ofHom
                {
                  toFun :=
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) :
                      (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j)) →
                        (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)),
                  continuous_toFun := ⋯ : C((↑(F.1 j) : Type u), coconePtOfCoconeForget c) } ≫
              CategoryTheory.Functor.map (Functor.obj (Functor.const J) (of (coconePtOfCoconeForget c))) φ) :
          (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj (of (coconePtOfCoconeForget c))).obj j') : Type u))
        x :
      (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (of (coconePtOfCoconeForget c))) j') : Type u))

Tactic:
apply ConcreteCategory.congr_hom (c.ι.naturality φ)

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom
-- 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
refine :
  ∀ (s : Cocone F),
    Continuous (X := coconePtOfCoconeForget c) (Y := (↑s.1 : Type u))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.desc
              (Functor.mapCocone
                (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
        (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) (forget.mapCocone s).pt)
⊢ IsColimit (coconeOfCoconeForget c)

Tactic:
refine IsColimit.ofFaithful forget (ht := hc)
    (fun s ↦ ofHom (ContinuousMap.mk (hc.desc ((forget).mapCocone s)) ?_)) (fun _ ↦ 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_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
rw :
  topologicalSpaceCoconePtOfCoconeForget c ≤
    induced (Y := (↑s.1 : Type u))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.desc
              (Functor.mapCocone
                (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
        (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) (forget.mapCocone s).pt)
      (str s.1)
⊢ Continuous (X := coconePtOfCoconeForget c) (Y := (↑s.1 : Type u))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
              s))) :
      (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) (forget.mapCocone s).pt)

Tactic:
rw [continuous_iff_le_induced]

Premises used: continuous_iff_le_induced
-- 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
dsimp :
  LE.le (α := TopologicalSpace (coconePtOfCoconeForget c))
    (⨆ (j : J),
      coinduced (X := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) (F.obj j).str)
    (induced (Y := (↑s.1 : Type u))
      (⇑(@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)
      (str s.1))
⊢ topologicalSpaceCoconePtOfCoconeForget c ≤
    induced (Y := (↑s.1 : Type u))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.desc
              (Functor.mapCocone
                (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
        (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) (forget.mapCocone s).pt)
      (str s.1)

Tactic:
dsimp [topologicalSpaceCoconePtOfCoconeForget]

Premises used: 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_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
rw :
  ∀ (i : J),
    LE.le (α := TopologicalSpace (coconePtOfCoconeForget c))
      (coinduced (X :=
        ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj i))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app i)) : (a : ToType (F.obj i)) → c.pt) (F.obj i).str)
      (induced (Y := (↑s.1 : Type u))
        (⇑(@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)
        (str s.1))
⊢ LE.le (α := TopologicalSpace (coconePtOfCoconeForget c))
    (⨆ (j : J),
      coinduced (X := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) (F.obj j).str)
    (induced (Y := (↑s.1 : Type u))
      (⇑(@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)
      (str s.1))

Tactic:
rw [iSup_le_iff]

Premises used: iSup_le_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_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
rw :
  LE.le (α :=
    TopologicalSpace
      (ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j)))
    (F.obj j).str
    (induced (Y := (↑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))
      (str s.1))
⊢ LE.le (α := TopologicalSpace (coconePtOfCoconeForget c))
    (coinduced (X := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) (F.obj j).str)
    (induced (Y := (↑s.1 : Type u))
      (⇑(@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)
      (str s.1))

Tactic:
rw [coinduced_le_iff_le_induced, induced_compose]

Premises used: induced_compose, coinduced_le_iff_le_induced
-- 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
⊢ LE.le (α := TopologicalSpace (↑(F.obj j) : Type u)) (F.obj j).str
    (induced (Y := (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u))
      (⇑(Hom.hom (s.ι.app j)) : (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj s.pt).obj j) : Type u))
      (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j).str)

Tactic:
continuous_iff_le_induced.1 (s.ι.app j).hom.continuous

Premises used: ContinuousMap.continuous, continuous_iff_le_induced, CategoryTheory.Limits.Cocone.ι, TopCat.Hom.hom, Iff.mp, CategoryTheory.NatTrans.app
-- 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
h :
  (↑s.1 : Type u) = (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u) →
    Eq (α :=
      ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j) →
        (↑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))
      (⇑(Hom.hom (s.ι.app j)) : (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj s.pt).obj j) : Type u))
⊢ LE.le (α :=
    TopologicalSpace
      (ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j)))
    (F.obj j).str
    (induced (Y := (↑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))
      (str s.1))

Tactic:
convert! continuous_iff_le_induced.1 (s.ι.app j).hom.continuous

Premises used: ContinuousMap.continuous, continuous_iff_le_induced, CategoryTheory.Limits.Cocone.ι, TopCat.Hom.hom, Iff.mp, CategoryTheory.NatTrans.app
-- 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)
h :
  ∀ (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))
⊢ Eq (α :=
    ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j) → (↑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))
    (⇑(Hom.hom (s.ι.app j)) : (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj s.pt).obj j) : Type u))

Tactic:
ext x
-- 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:
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