awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : (↑S.1 : Type (max u v))
i j : J
f : i ⟶ j
⊢ Eq (α := (↑(F.obj j) : Type (max u v)))
    ((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)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (S.π.app i) :
            (a : (↑S.pt : Type (max u v))) → (↑(F.obj i) : Type (max u v)))
          x) :
      (↑(F.obj j) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (S.π.app i ≫ F.map f) :
          (a : (↑S.pt : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
        x :
      (↑(F.obj j) : Type (max u v)))

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
m : S.pt ⟶ (limitCone.{v, u, w} F).pt
h : ∀ (j : J), m ≫ (limitCone.{v, u, w} F).π.app j = S.π.app j
a : (↑S.pt : Type (max u v))
⊢ Eq (α := (↑(limitCone.{v, u, w} F).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)
            m :
          (a : (↑S.pt : Type (max u v))) → (↑(limitCone F).pt : Type (max u v)))
        a :
      (↑(limitCone.{v, u, w} F).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)
            (X := S.pt) (Y := (limitCone.{v, u, w} F).pt)
            (ofHom
              {
                toFun := fun (x : (↑S.1 : Type (max u v))) ↦
                  Subtype.mk (p := fun (x : (j : J) → (↑(F.obj j) : Type (max u v))) ↦
                    ∀ {i j : J} (f : i ⟶ 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)))
                          (x i) =
                        x j)
                    (fun (x_1 : J) ↦
                      ((Hom.hom ((limitCone.{v, u, w} F).π.app x_1)).comp (Hom.hom m) :
                          (a : (↑S.pt : Type (max u v))) → (↑(F.obj x_1) : Type (max u v)))
                        x)
                    ⋯,
                continuous_toFun := ⋯ }) :
          (a : (↑S.pt : Type (max u v))) → (↑(limitCone F).pt : Type (max u v)))
        a :
      (↑(limitCone.{v, u, w} F).pt : Type (max u v)))

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

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 : Cone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
j : J
⊢ topologicalSpaceConePtOfConeForget c ≤
    induced (Y := (↑(F.1 j) : Type u))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.π.app j)) :
        (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
      (str (F.1 j))

Tactic:
iInf_le _ _

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

Tactic:
exact iInf_le _ _

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

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

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

Premises used: CategoryTheory.Limits.Cone.π, 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 : Cone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsLimit c
refine :
  ∀ (s : Cone F),
    Continuous (X := (↑s.1 : Type u)) (Y := conePtOfConeForget c)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.lift
              (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                s))) :
        (a : (fun (X : Type u) ↦ X) (forget.mapCone s).pt) → (fun (X : Type u) ↦ X) c.pt)
⊢ IsLimit (coneOfConeForget c)

Tactic:
refine IsLimit.ofFaithful forget (ht := hc)
    (fun s ↦ ofHom (ContinuousMap.mk (hc.lift ((forget).mapCone 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 : Cone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsLimit c
s : Cone F
rw :
  coinduced (X := (↑s.1 : Type u))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.lift
              (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                s))) :
        (a : (fun (X : Type u) ↦ X) (forget.mapCone s).pt) → (fun (X : Type u) ↦ X) c.pt)
      (str s.1) ≤
    topologicalSpaceConePtOfConeForget c
⊢ Continuous (X := (↑s.1 : Type u)) (Y := conePtOfConeForget c)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.lift
            (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
              s))) :
      (a : (fun (X : Type u) ↦ X) (forget.mapCone s).pt) → (fun (X : Type u) ↦ X) c.pt)

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_1 c : Cone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsLimit c
s : Cone F
dsimp :
  LE.le (α := TopologicalSpace (conePtOfConeForget c))
    (coinduced (X := (↑s.1 : Type u))
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (hc.lift
              (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                s))) :
        (a : ToType s.pt) → c.pt)
      (str s.1))
    (⨅ (j : J),
      induced (Y := 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 : c.pt) → ToType (F.obj j)) (F.obj j).str)
⊢ coinduced (X := (↑s.1 : Type u))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.lift
              (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                s))) :
        (a : (fun (X : Type u) ↦ X) (forget.mapCone s).pt) → (fun (X : Type u) ↦ X) c.pt)
      (str s.1) ≤
    topologicalSpaceConePtOfConeForget c

Tactic:
dsimp [topologicalSpaceConePtOfConeForget]

Premises used: TopCat.topologicalSpaceConePtOfConeForget
-- 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 : Cone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsLimit c
s : Cone F
rw :
  ∀ (i : J),
    LE.le (α := TopologicalSpace (conePtOfConeForget c))
      (coinduced (X := (↑s.1 : Type u))
        (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (hc.lift
                (Functor.mapCone
                  (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
          (a : ToType s.pt) → c.pt)
        (str s.1))
      (induced (Y := 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 : c.pt) → ToType (F.obj i)) (F.obj i).str)
⊢ LE.le (α := TopologicalSpace (conePtOfConeForget c))
    (coinduced (X := (↑s.1 : Type u))
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (hc.lift
              (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                s))) :
        (a : ToType s.pt) → c.pt)
      (str s.1))
    (⨅ (j : J),
      induced (Y := 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 : c.pt) → ToType (F.obj j)) (F.obj j).str)

Tactic:
rw [le_iInf_iff]

Premises used: le_iInf_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 : Cone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsLimit c
s : Cone F
j : J
rw :
  LE.le (α := TopologicalSpace (↑s.1 : Type u)) (str s.1)
    (induced (Y := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
      (Function.comp (β := conePtOfConeForget c)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.π.app j)) : (a : c.pt) → ToType (F.obj j))
        (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (hc.lift
                (Functor.mapCone
                  (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
          (a : ToType s.pt) → c.pt))
      (F.obj j).str)
⊢ LE.le (α := TopologicalSpace (conePtOfConeForget c))
    (coinduced (X := (↑s.1 : Type u))
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (hc.lift
              (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                s))) :
        (a : ToType s.pt) → c.pt)
      (str s.1))
    (induced (Y := 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 : c.pt) → ToType (F.obj j)) (F.obj j).str)

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 : Cone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsLimit c
s : Cone F
j : J
⊢ LE.le (α := TopologicalSpace (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u))
    (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j).str
    (induced (Y := (↑(F.obj j) : Type u))
      (⇑(Hom.hom (s.π.app j)) : (a : (↑(((Functor.const J).obj s.pt).obj j) : Type u)) → (↑(F.obj j) : Type u))
      (F.obj j).str)

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

Premises used: ContinuousMap.continuous, CategoryTheory.Limits.Cone.π, continuous_iff_le_induced, 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 : Cone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsLimit c
s : Cone F
j : J
h :
  TopologicalSpace (↑s.1 : Type u) =
      TopologicalSpace (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u) →
    (↑s.1 : Type u) = (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u) →
      Eq (α :=
        (↑s.1 : Type u) →
          ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
        (Function.comp (β := conePtOfConeForget c)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.π.app j)) : (a : c.pt) → ToType (F.obj j))
          (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (hc.lift
                  (Functor.mapCone
                    (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
            (a : ToType s.pt) → c.pt))
        (⇑(Hom.hom (s.π.app j)) : (a : (↑(((Functor.const J).obj s.pt).obj j) : Type u)) → (↑(F.obj j) : Type u))
⊢ LE.le (α := TopologicalSpace (↑s.1 : Type u)) (str s.1)
    (induced (Y := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
      (Function.comp (β := conePtOfConeForget c)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.π.app j)) : (a : c.pt) → ToType (F.obj j))
        (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (hc.lift
                (Functor.mapCone
                  (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
          (a : ToType s.pt) → c.pt))
      (F.obj j).str)

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

Premises used: ContinuousMap.continuous, CategoryTheory.Limits.Cone.π, continuous_iff_le_induced, 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 : Cone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsLimit c
s : Cone F
j : J
e_1 :
  TopologicalSpace (↑s.1 : Type u) =
    TopologicalSpace (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u)
e_1_1 : (↑s.1 : Type u) = (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u)
h :
  ∀ (x : (↑s.1 : Type u)),
    Eq (α := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
      (Function.comp (β := conePtOfConeForget c)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.π.app j)) : (a : c.pt) → ToType (F.obj j))
          (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (hc.lift
                  (Functor.mapCone
                    (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
            (a : ToType s.pt) → c.pt)
          x :
        ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
      ((Hom.hom (s.π.app j) : (a : (↑(((Functor.const J).obj s.pt).obj j) : Type u)) → (↑(F.obj j) : Type u)) x :
        (↑(F.obj j) : Type u))
⊢ Eq (α :=
    (↑s.1 : Type u) → ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
    (Function.comp (β := conePtOfConeForget c)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.π.app j)) : (a : c.pt) → ToType (F.obj j))
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (hc.lift
              (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                s))) :
        (a : ToType s.pt) → c.pt))
    (⇑(Hom.hom (s.π.app j)) : (a : (↑(((Functor.const J).obj s.pt).obj j) : Type u)) → (↑(F.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 : Cone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsLimit c
s : Cone F
j : J
e_1 :
  TopologicalSpace (↑s.1 : Type u) =
    TopologicalSpace (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u)
e_1_1 : (↑s.1 : Type u) = (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u)
x : (↑s.1 : Type u)
⊢ Eq (α := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
    (Function.comp (β := conePtOfConeForget c)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.π.app j)) : (a : c.pt) → ToType (F.obj j))
        (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (hc.lift
                (Functor.mapCone
                  (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
          (a : ToType s.pt) → c.pt)
        x :
      ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
    ((Hom.hom (s.π.app j) : (a : (↑(((Functor.const J).obj s.pt).obj j) : Type u)) → (↑(F.obj j) : Type u)) x :
      (↑(F.obj j) : Type u))

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

Premises used: CategoryTheory.ConcreteCategory.hom_ext_iff, CategoryTheory.forget, Iff.mp, TopCat, CategoryTheory.Functor.mapCone, CategoryTheory.Limits.IsLimit.fac