awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
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 (↑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)
have 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))
Tactic: convert! continuous_iff_le_induced.1 (s.π.app j).hom.continuous
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
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)
⊢ 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))
have 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))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (hypothesis)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cone F
hc : IsLimit c
c' : Cone F :=
  coneOfConeForget
    (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsLimit c' :=
  isLimitConeOfForget
    (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isLimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.conePointUniqueUpToIso hc
⊢ Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u)) c.pt.str
    (⨅ (j : J),
      induced (Y := (↑(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 : (↑(((Functor.const J).obj c.pt).obj j) : Type u)) → (↑(F.obj j) : Type u))
        (F.obj j).str)
have he : ∀ (j : J), e.inv ≫ c'.π.app j = c.π.app j
Tactic: have he (j : J) : e.inv ≫ c'.π.app j = c.π.app j :=
    IsLimit.conePointUniqueUpToIso_inv_comp hc' hc j
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cone F
hc : IsLimit c
c' : Cone F :=
  coneOfConeForget
    (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsLimit c' :=
  isLimitConeOfForget
    (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isLimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.conePointUniqueUpToIso hc
he : ∀ (j : J), e.inv ≫ c'.π.app j = c.π.app j
⊢ Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u)) c.pt.str
    (⨅ (j : J),
      induced (Y := (↑(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 : (↑(((Functor.const J).obj c.pt).obj j) : Type u)) → (↑(F.obj j) : Type u))
        (F.obj j).str)
have apply : Eq (α := TopologicalSpace (↑c.pt : Type u))
  (induced (Y := (↑c'.pt : Type u)) (⇑(homeoOfIso e.symm) : (a : (↑c.pt : Type u)) → (↑c'.pt : Type u)) c'.pt.str)
  (⨅ (j : J),
    induced (Y := (↑(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 : (↑(((Functor.const J).obj c.pt).obj j) : Type u)) → (↑(F.obj j) : Type u))
      (F.obj j).str)
Tactic: apply (homeoOfIso e.symm).induced_eq.symm.trans
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cone F
hc : IsLimit c
c' : Cone F :=
  coneOfConeForget
    (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsLimit c' :=
  isLimitConeOfForget
    (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isLimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.conePointUniqueUpToIso hc
he : ∀ (j : J), e.inv ≫ c'.π.app j = c.π.app j
⊢ Eq (α := TopologicalSpace (↑c.pt : Type u))
    (induced (Y := (↑c'.pt : Type u)) (⇑(homeoOfIso e.symm) : (a : (↑c.pt : Type u)) → (↑c'.pt : Type u)) c'.pt.str)
    (⨅ (j : J),
      induced (Y := (↑(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 : (↑(((Functor.const J).obj c.pt).obj j) : Type u)) → (↑(F.obj j) : Type u))
        (F.obj j).str)
have dsimp : Eq (α := TopologicalSpace (↑c.pt : Type u))
  (induced (Y :=
    conePtOfConeForget
      (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c))
    (⇑(homeoOfIso e.symm) : (a : (↑c.pt : Type u)) → conePtOfConeForget (forget.mapCone c))
    (⨅ (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 := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.π.app j)) :
          (a : (↑c.pt : Type u)) → (↑(F.obj j) : Type u))
        (F.obj j).str))
  (⨅ (j : J),
    induced (Y := (↑(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 : (↑c.pt : Type u)) → (↑(F.obj j) : Type u))
      (F.obj j).str)
Tactic: dsimp [coneOfConeForget_pt, c', topologicalSpaceConePtOfConeForget]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cone F
hc : IsLimit c
c' : Cone F :=
  coneOfConeForget
    (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsLimit c' :=
  isLimitConeOfForget
    (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isLimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.conePointUniqueUpToIso hc
he : ∀ (j : J), e.inv ≫ c'.π.app j = c.π.app j
| ⨅ (j : J),
    induced (Y := (↑(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 : (↑c.pt : Type u)) → (↑(F.obj j) : Type u))
      (F.obj j).str
have simp : ⨅ (j : J),
  induced (Y := (↑(F.obj j) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          (e.inv ≫ c'.π.app j)) :
      (a : (↑c.pt : Type u)) → (↑(F.obj j) : Type u))
    (F.obj j).str
Tactic: simp only [← he]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cone F
hc : IsLimit c
c' : Cone F :=
  coneOfConeForget
    (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsLimit c' :=
  isLimitConeOfForget
    (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isLimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.conePointUniqueUpToIso hc
he : ∀ (j : J), e.inv ≫ c'.π.app j = c.π.app j
⊢ Eq (α := TopologicalSpace (↑c.pt : Type u))
    (induced (Y :=
      conePtOfConeForget
        (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c))
      (⇑(homeoOfIso e.symm) : (a : (↑c.pt : Type u)) → conePtOfConeForget (forget.mapCone c))
      (⨅ (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 := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.π.app j)) :
            (a : (↑c.pt : Type u)) → (↑(F.obj j) : Type u))
          (F.obj j).str))
    (⨅ (j : J),
      induced (Y := (↑(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 : (↑c.pt : Type u)) → (↑(F.obj j) : Type u))
        (F.obj j).str)
have conv_rhs : Eq (α := TopologicalSpace (↑c.pt : Type u))
  (induced (Y :=
    conePtOfConeForget
      (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c))
    (⇑(homeoOfIso e.symm) : (a : (↑c.pt : Type u)) → conePtOfConeForget (forget.mapCone c))
    (⨅ (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 := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.π.app j)) :
          (a : (↑c.pt : Type u)) → (↑(F.obj j) : Type u))
        (F.obj j).str))
  (⨅ (j : J),
    induced (Y := (↑(F.obj j) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (e.inv ≫ c'.π.app j)) :
        (a : (↑c.pt : Type u)) → (↑(F.obj j) : Type u))
      (F.obj j).str)
Tactic: conv_rhs => simp only [← he]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cone F
hc :
  IsLimit (F := F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
    (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
⊢ Nonempty (IsLimit c) ↔
    Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u)) c.pt.str
      (⨅ (j : J),
        induced (Y := (↑(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 : (↑(((Functor.const J).obj c.pt).obj j) : Type u)) → (↑(F.obj j) : Type u))
          (F.obj j).str)
have refine : (h :
    Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u)) c.pt.str
      (⨅ (j : J),
        induced (Y := (↑(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 : (↑(((Functor.const J).obj c.pt).obj j) : Type u)) → (↑(F.obj j) : Type u))
          (F.obj j).str)) →
  IsLimit c
Tactic: refine ⟨fun ⟨hc⟩ ↦ induced_of_isLimit _ hc, fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cone F
hc :
  IsLimit (F := F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
    (Functor.mapCone (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),
      induced (Y := (↑(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 : (↑(((Functor.const J).obj c.pt).obj j) : Type u)) → (↑(F.obj j) : Type u))
        (F.obj j).str)
⊢ IsLimit c
have refine_1 : (coneOfConeForget
      (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
        c)).pt ≅
  c.pt
Tactic: refine .ofIsoLimit (isLimitConeOfForget _ hc) (Cone.ext ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cone F
hc :
  IsLimit (F := F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
    (Functor.mapCone (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),
      induced (Y := (↑(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 : (↑(((Functor.const J).obj c.pt).obj j) : Type u)) → (↑(F.obj j) : Type u))
        (F.obj j).str)
refine_1 :
  (coneOfConeForget
        (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
          c)).pt ≅
    c.pt
⊢ IsLimit c
have refine_2 : ∀ (j : J),
  (coneOfConeForget
            (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
              c)).π.app
      j =
    Iso.hom
        (isoOfHomeo
          (let __Equiv :
            (↑(coneOfConeForget
                      (Functor.mapCone
                        (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
              (↑(coneOfConeForget
                      (Functor.mapCone
                        (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                        c)).pt :
                Type u);
          { toEquiv := __Equiv, continuous_toFun := sorry, continuous_invFun := sorry })) ≫
      c.π.app j
Tactic: refine .ofIsoLimit (isLimitConeOfForget _ hc) (Cone.ext ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
⊢ HasLimit F ↔
    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))
have rw : HasLimit F ↔ HasLimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
Tactic: rw [← Types.hasLimit_iff_small_sections]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
⊢ HasLimit F ↔ HasLimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
have mp : HasLimit F → HasLimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
mp : HasLimit F → HasLimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
⊢ HasLimit F ↔ HasLimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
have mpr : HasLimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) → HasLimit F
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
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
⊢ HasLimit F
have 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))
Tactic: rw [hasLimit_iff_small_sections]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
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
⊢ 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))
have 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
Tactic: rw [continuous_iff_coinduced_le]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
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
⊢ 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
have 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)
Tactic: dsimp [topologicalSpaceCoconePtOfCoconeForget]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
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'
⊢ 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))) φ
have 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 := sorry : 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 := sorry : 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: ext