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 : 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:
exact 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
-- 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
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
⊢ ∀ (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
-- 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
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
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)
⊢ 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)

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

Premises used: Homeomorph.induced_eq, TopCat.homeoOfIso, CategoryTheory.Iso.symm, Eq.symm, Eq.trans
-- 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
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
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)
⊢ 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:
dsimp [coneOfConeForget_pt, c', topologicalSpaceConePtOfConeForget]

Premises used: TopCat.topologicalSpaceConePtOfConeForget, TopCat.coneOfConeForget_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 : 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
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
| ⨅ (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:
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 : 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
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)
⊢ 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:
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 : 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)
              (e.inv ≫ c'.π.app j)) :
          (a : (↑c.pt : Type u)) → (↑(F.obj j) : Type u))
        (F.obj j).str)

Tactic:
simp [← induced_compose, homeoOfIso, c']

Premises used: induced_compose, TopCat.homeoOfIso
-- 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
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)

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

Premises used: CategoryTheory.Limits.Cone.π, iInf, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Cone.pt, _private.0.TopCat.nonempty_isLimit_iff_eq_induced.match_1, Nonempty.intro, TopCat.str, TopologicalSpace.induced, Iff.intro, TopCat.induced_of_isLimit, Eq, DFunLike.coe, CategoryTheory.Functor.obj, 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 : 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)
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
⊢ 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)

Tactic:
refine ⟨fun ⟨hc⟩ ↦ induced_of_isLimit _ hc, fun h ↦ ⟨?_⟩⟩
-- 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
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
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 := ⋯, continuous_invFun := ⋯ })) ≫
        c.π.app j
⊢ IsLimit c

Tactic:
refine .ofIsoLimit (isLimitConeOfForget _ hc) (Cone.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
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)
⊢ Continuous.{u, u} (X :=
    (↑(coneOfConeForget
            (Functor.mapCone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
              c)).pt :
      Type u))
    (Equiv.toFun
      (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)))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : 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)
⊢ Continuous.{u, u} (X := (↑c.pt : Type u))
    (Equiv.invFun
      (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)))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : 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)
⊢ (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 TopCat.isoOfHomeo
      { toEquiv := .refl _,
        continuous_toFun := h ▸ by fun_prop,
        continuous_invFun := h ▸ by fun_prop }

Premises used: Homeomorph.mk, TopCat.carrier, TopCat.isoOfHomeo, Equiv.refl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : 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)
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 := ⋯, continuous_invFun := ⋯ })) ≫
      c.π.app j

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

Tactic:
induced_of_isLimit _ (limit.isLimit _)

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

Tactic:
rw [← Types.hasLimit_iff_small_sections]

Premises used: CategoryTheory.Limits.Types.hasLimit_iff_small_sections
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
mp : HasLimit F → HasLimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
mpr :
  HasLimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) → HasLimit F
⊢ HasLimit F ↔ HasLimit (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))

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

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

Tactic:
⟨⟨_, isLimitConeOfForget _ (limit.isLimit _)⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk, TopCat.isLimitConeOfForget