awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
refine_1 :
  LE.le (α := TopologicalSpace (↑(uliftFunctor.mapCone c).pt : Type (max u v))) (uliftFunctor.mapCone c).pt.str
    (⨅ (j : J),
      TopologicalSpace.induced (Y := (↑((K ⋙ uliftFunctor).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) ((uliftFunctor.mapCone c).π.app j)) :
          (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj j) : Type (max u v))) →
            (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj j).str)
refine_2 :
  LE.le (α := TopologicalSpace (↑(uliftFunctor.mapCone c).pt : Type (max u v)))
    (⨅ (j : J),
      TopologicalSpace.induced (Y := (↑((K ⋙ uliftFunctor).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) ((uliftFunctor.mapCone c).π.app j)) :
          (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj j) : Type (max u v))) →
            (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj j).str)
    (uliftFunctor.mapCone c).pt.str
⊢ Eq (α := TopologicalSpace (↑(uliftFunctor.mapCone c).pt : Type (max u v))) (uliftFunctor.mapCone c).pt.str
    (⨅ (j : J),
      TopologicalSpace.induced (Y := (↑((K ⋙ uliftFunctor).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) ((uliftFunctor.mapCone c).π.app j)) :
          (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj j) : Type (max u v))) →
            (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj j).str)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
refine_1 :
  ∀ (i : J),
    LE.le (α := TopologicalSpace (↑(uliftFunctor.mapCone c).pt : Type (max u v))) (uliftFunctor.mapCone c).pt.str
      (TopologicalSpace.induced (Y := (↑((K ⋙ uliftFunctor).obj i) : Type (max u v)))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) ((uliftFunctor.mapCone c).π.app i)) :
          (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj i) : Type (max u v))) →
            (↑((K ⋙ uliftFunctor).obj i) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj i).str)
⊢ LE.le (α := TopologicalSpace (↑(uliftFunctor.mapCone c).pt : Type (max u v))) (uliftFunctor.mapCone c).pt.str
    (⨅ (j : J),
      TopologicalSpace.induced (Y := (↑((K ⋙ uliftFunctor).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) ((uliftFunctor.mapCone c).π.app j)) :
          (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj j) : Type (max u v))) →
            (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj j).str)

Tactic:
rw [le_iInf_iff]

Premises used: le_iInf_iff
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
j : J
t : Set (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))
ht : IsOpen t
⊢ IsOpen (X := (↑(uliftFunctor.mapCone c).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) ((uliftFunctor.mapCone c).π.app j)) :
        (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj j) : Type (max u v))) →
          (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))) ⁻¹'
      t)

Tactic:
⟨Homeomorph.ulift.symm ⁻¹' ((uliftFunctor.map (c.π.app j)) ⁻¹' t), ?_, rfl⟩

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ConcreteCategory.hom, TopCat.uliftFunctor, CategoryTheory.Functor.map, Homeomorph.ulift, Set.preimage, Homeomorph.symm, And.intro, Exists.intro, IsOpen, DFunLike.coe, CategoryTheory.NatTrans.app, rfl
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
j : J
t : Set (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))
ht : IsOpen t
refine_1 :
  IsOpen.{u} (X := (↑c.pt : Type u))
    (Set.preimage (β := ULift.{v, u} (↑c.pt : Type u))
      (⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (uliftFunctor.map (c.π.app j))) :
          (a : (↑(uliftFunctor.obj (((Functor.const J).obj c.pt).obj j)) : Type (max u v))) →
            (↑(uliftFunctor.obj (K.obj j)) : Type (max u v))) ⁻¹'
        t))
⊢ IsOpen (X := (↑(uliftFunctor.mapCone c).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) ((uliftFunctor.mapCone c).π.app j)) :
        (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj j) : Type (max u v))) →
          (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))) ⁻¹'
      t)

Tactic:
refine ⟨Homeomorph.ulift.symm ⁻¹' ((uliftFunctor.map (c.π.app j)) ⁻¹' t), ?_, rfl⟩
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
j : J
t : Set (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))
ht : IsOpen t
refine_1 :
  IsOpen (X := ULift.{v, u} (↑c.pt : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
            carrier) (uliftFunctor.map (c.π.app j))) :
        (a : (↑(uliftFunctor.obj (((Functor.const J).obj c.pt).obj j)) : Type (max u v))) →
          (↑(uliftFunctor.obj (K.obj j)) : Type (max u v))) ⁻¹'
      t)
⊢ IsOpen.{u} (X := (↑c.pt : Type u))
    (Set.preimage (β := ULift.{v, u} (↑c.pt : Type u))
      (⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (uliftFunctor.map (c.π.app j))) :
          (a : (↑(uliftFunctor.obj (((Functor.const J).obj c.pt).obj j)) : Type (max u v))) →
            (↑(uliftFunctor.obj (K.obj j)) : Type (max u v))) ⁻¹'
        t))

Tactic:
apply Homeomorph.ulift.continuous_invFun.isOpen_preimage

Premises used: Homeomorph.ulift, Homeomorph.continuous_invFun, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
j : J
t : Set (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))
ht : IsOpen t
⊢ IsOpen (X := ULift.{v, u} (↑c.pt : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
            carrier) (uliftFunctor.map (c.π.app j))) :
        (a : (↑(uliftFunctor.obj (((Functor.const J).obj c.pt).obj j)) : Type (max u v))) →
          (↑(uliftFunctor.obj (K.obj j)) : Type (max u v))) ⁻¹'
      t)

Tactic:
apply (uliftFunctor.map (c.π.app j)).hom.continuous_toFun.isOpen_preimage _ ht

Premises used: CategoryTheory.Limits.Cone.π, TopCat.uliftFunctor, CategoryTheory.Functor.map, ContinuousMap.continuous_toFun, TopCat.Hom.hom, Continuous.isOpen_preimage, CategoryTheory.NatTrans.app
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
refine_2 :
  ∀ (i : J),
    LE.le (α := TopologicalSpace (↑(uliftFunctor.mapCone c).pt : Type (max u v)))
      (TopologicalSpace.generateFrom (⋃ (i : J), {s : Set (↑(uliftFunctor.mapCone c).pt : Type (max u v)) | IsOpen s}))
      (TopologicalSpace.induced ULift.down
        (TopologicalSpace.induced (Y := (↑(K.obj i) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.π.app i)) :
            (a : (↑(((Functor.const J).obj c.pt).obj i) : Type u)) → (↑(K.obj i) : Type u))
          (K.obj i).str))
⊢ LE.le (α := TopologicalSpace (↑(uliftFunctor.mapCone c).pt : Type (max u v)))
    (⨅ (j : J),
      TopologicalSpace.induced (Y := (↑((K ⋙ uliftFunctor).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) ((uliftFunctor.mapCone c).π.app j)) :
          (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj j) : Type (max u v))) →
            (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj j).str)
    (TopologicalSpace.induced ULift.down c.pt.str)

Tactic:
rw [← generateFrom_iUnion_isOpen, induced_of_isLimit _ hc, induced_iInf, le_iInf_iff]

Premises used: generateFrom_iUnion_isOpen, le_iInf_iff, TopCat.induced_of_isLimit, induced_iInf
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
i : J
t : Set (↑(K.obj i) : Type u)
ht : IsOpen t
⊢ IsOpen (X := (↑(uliftFunctor.mapCone c).pt : Type (max u v)))
    (ULift.down ⁻¹'
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.π.app i)) :
          (a : (↑(((Functor.const J).obj c.pt).obj i) : Type u)) → (↑(K.obj i) : Type u)) ⁻¹'
        t)

Tactic:
.basic _ ?_

Premises used: TopologicalSpace.GenerateOpen.basic, IsOpen
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
i : J
t : Set (↑(K.obj i) : Type u)
ht : IsOpen t
refine_2 :
  Membership.mem (γ := Set (Set (↑(uliftFunctor.mapCone c).pt : Type (max u v))))
    (⋃ (i : J), {s : Set (↑(uliftFunctor.mapCone c).pt : Type (max u v)) | IsOpen s})
    (ULift.down ⁻¹'
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.π.app i)) :
          (a : (↑(((Functor.const J).obj c.pt).obj i) : Type u)) → (↑(K.obj i) : Type u)) ⁻¹'
        t)
⊢ IsOpen (X := (↑(uliftFunctor.mapCone c).pt : Type (max u v)))
    (ULift.down ⁻¹'
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.π.app i)) :
          (a : (↑(((Functor.const J).obj c.pt).obj i) : Type u)) → (↑(K.obj i) : Type u)) ⁻¹'
        t)

Tactic:
refine .basic _ ?_
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
i : J
t : Set (↑(K.obj i) : Type u)
ht : IsOpen t
refine_2 :
  ∃ (i_1 : J),
    Membership.mem (γ := Set (Set (↑(uliftFunctor.mapCone c).pt : Type (max u v))))
      {s : Set (↑(uliftFunctor.mapCone c).pt : Type (max u v)) | IsOpen s}
      (ULift.down ⁻¹'
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.π.app i)) :
            (a : (↑(((Functor.const J).obj c.pt).obj i) : Type u)) → (↑(K.obj i) : Type u)) ⁻¹'
          t)
⊢ Membership.mem (γ := Set (Set (↑(uliftFunctor.mapCone c).pt : Type (max u v))))
    (⋃ (i : J), {s : Set (↑(uliftFunctor.mapCone c).pt : Type (max u v)) | IsOpen s})
    (ULift.down ⁻¹'
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.π.app i)) :
          (a : (↑(((Functor.const J).obj c.pt).obj i) : Type u)) → (↑(K.obj i) : Type u)) ⁻¹'
        t)

Tactic:
rw [Set.mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
i : J
t : Set (↑(K.obj i) : Type u)
ht : IsOpen t
⊢ ∃ (i_1 : J),
    Membership.mem (γ := Set (Set (↑(uliftFunctor.mapCone c).pt : Type (max u v))))
      {s : Set (↑(uliftFunctor.mapCone c).pt : Type (max u v)) | IsOpen s}
      (ULift.down ⁻¹'
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.π.app i)) :
            (a : (↑(((Functor.const J).obj c.pt).obj i) : Type u)) → (↑(K.obj i) : Type u)) ⁻¹'
          t)

Tactic:
⟨i, ULift.down ⁻¹' t, Homeomorph.ulift.continuous_toFun.isOpen_preimage _ ht, rfl⟩

Premises used: Homeomorph.continuous_toFun, Homeomorph.ulift, Set.preimage, And.intro, Exists.intro, Continuous.isOpen_preimage, ULift.down, rfl
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
i : J
t : Set (↑(K.obj i) : Type u)
ht : IsOpen t
⊢ ∃ (i_1 : J),
    Membership.mem (γ := Set (Set (↑(uliftFunctor.mapCone c).pt : Type (max u v))))
      {s : Set (↑(uliftFunctor.mapCone c).pt : Type (max u v)) | IsOpen s}
      (ULift.down ⁻¹'
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.π.app i)) :
            (a : (↑(((Functor.const J).obj c.pt).obj i) : Type u)) → (↑(K.obj i) : Type u)) ⁻¹'
          t)

Tactic:
exact ⟨i, ULift.down ⁻¹' t, Homeomorph.ulift.continuous_toFun.isOpen_preimage _ ht, rfl⟩
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
⊢ IsLimit (F :=
    (K ⋙ uliftFunctor) ⋙
      forget TopCat (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier))
    (Functor.mapCone
      (forget TopCat (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier))
      (uliftFunctor.mapCone c))

Tactic:
exact isLimitOfPreserves (forget TopCat ⋙ CategoryTheory.uliftFunctor) hc

Premises used: CategoryTheory.Functor.comp, CategoryTheory.uliftFunctor, CategoryTheory.forget, TopCat, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
⊢ PreservesColimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor

Tactic:
⟨⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩

Premises used: CategoryTheory.Limits.PreservesColimitsOfSize.mk, CategoryTheory.Limits.PreservesColimit.mk, CategoryTheory.Limits.PreservesColimitsOfShape.mk
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
refine :
  ∀ {J : Type w} [inst : Category.{w', w} J] {K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat} {c : Cocone K}
    (hc : IsColimit c), Nonempty (IsColimit (uliftFunctor.mapCocone c))
⊢ PreservesColimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor

Tactic:
refine ⟨⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
rw :
  Eq (α := TopologicalSpace (↑(uliftFunctor.mapCocone c).pt : Type (max u v))) (uliftFunctor.mapCocone c).pt.str
    (⨆ (j : J),
      TopologicalSpace.coinduced (X := (↑((K ⋙ uliftFunctor).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) ((uliftFunctor.mapCocone c).ι.app j)) :
          (a : (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))) →
            (↑(((Functor.const J).obj (uliftFunctor.mapCocone c).pt).obj j) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj j).str)
hc₁ :
  IsColimit (F :=
    (K ⋙ uliftFunctor) ⋙
      forget TopCat (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier))
    (Functor.mapCocone
      (forget TopCat (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier))
      (uliftFunctor.mapCocone c))
⊢ Nonempty (IsColimit (uliftFunctor.mapCocone c))

Tactic:
rw [nonempty_isColimit_iff_eq_coinduced]

Premises used: TopCat.nonempty_isColimit_iff_eq_coinduced
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
a : ∀ (s : Set (↑(uliftFunctor.mapCocone c).pt : Type (max u v))), IsOpen s ↔ IsOpen s
⊢ Eq (α := TopologicalSpace (↑(uliftFunctor.mapCocone c).pt : Type (max u v))) (uliftFunctor.mapCocone c).pt.str
    (⨆ (j : J),
      TopologicalSpace.coinduced (X := (↑((K ⋙ uliftFunctor).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) ((uliftFunctor.mapCocone c).ι.app j)) :
          (a : (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))) →
            (↑(((Functor.const J).obj (uliftFunctor.mapCocone c).pt).obj j) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj j).str)

Tactic:
ext s
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
s : Set (↑(uliftFunctor.mapCocone c).pt : Type (max u v))
⊢ s ⊆
    Set.range (ι := (↑c.pt : Type u))
      (⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u))

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
s : Set (↑(uliftFunctor.mapCocone c).pt : Type (max u v))
a :
  (∀ (j : J),
      IsOpen (X := (↑(K.obj j) : Type u))
        (Set.preimage (β := (↑(Functor.obj.{w', u, w, u + 1} (Functor.obj (Functor.const J) c.pt) j) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑(K.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u))
          ((⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u)) ⁻¹' s))) ↔
    ∀ (i : J), IsOpen s
⊢ IsOpen s ↔ IsOpen s

Tactic:
rw [Homeomorph.ulift.symm.isOpenEmbedding.isOpen_iff_preimage_isOpen (by simp),
      isOpen_iff_of_isColimit _ hc, isOpen_iSup_iff]

Premises used: Topology.IsOpenEmbedding.isOpen_iff_preimage_isOpen, isOpen_iSup_iff, Homeomorph.ulift, Homeomorph.symm, Homeomorph.isOpenEmbedding, TopCat.isOpen_iff_of_isColimit
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
s : Set (↑(uliftFunctor.mapCocone c).pt : Type (max u v))
a :
  ∀ (a : J),
    IsOpen (X := (↑(K.obj a) : Type u))
        (Set.preimage (β := (↑(Functor.obj.{w', u, w, u + 1} (Functor.obj (Functor.const J) c.pt) a) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app a)) :
            (a_1 : (↑(K.obj a) : Type u)) → (↑(((Functor.const J).obj c.pt).obj a) : Type u))
          ((⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u)) ⁻¹' s)) ↔
      IsOpen s
⊢ (∀ (j : J),
      IsOpen (X := (↑(K.obj j) : Type u))
        (Set.preimage (β := (↑(Functor.obj.{w', u, w, u + 1} (Functor.obj (Functor.const J) c.pt) j) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑(K.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u))
          ((⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u)) ⁻¹' s))) ↔
    ∀ (i : J), IsOpen s

Tactic:
congr!
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
s : Set (↑(uliftFunctor.mapCocone c).pt : Type (max u v))
a : J
⊢ Subset (α := Set (↑(K.obj a) : Type u))
    (Set.preimage (β := (↑(Functor.obj.{w', u, w, u + 1} (Functor.obj (Functor.const J) c.pt) a) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (c.ι.app a)) :
        (a_1 : (↑(K.obj a) : Type u)) → (↑(((Functor.const J).obj c.pt).obj a) : Type u))
      ((⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u)) ⁻¹' s))
    (Set.range (ι := ULift.{v, u} (↑(K.obj a) : Type u))
      (⇑Homeomorph.ulift : (a_1 : ULift.{v, u} (↑(K.obj a) : Type u)) → (↑(K.obj a) : Type u)))

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
s : Set (↑(uliftFunctor.mapCocone c).pt : Type (max u v))
a_1 : J
a :
  IsOpen (X := ULift.{v, u} (↑(K.obj a_1) : Type u))
      (Set.preimage (β := (↑(K.obj a_1) : Type u))
        (⇑Homeomorph.ulift : (a : ULift.{v, u} (↑(K.obj a_1) : Type u)) → (↑(K.obj a_1) : Type u))
        (Set.preimage (β := (↑(Functor.obj.{w', u, w, u + 1} (Functor.obj (Functor.const J) c.pt) a_1) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app a_1)) :
            (a : (↑(K.obj a_1) : Type u)) → (↑(((Functor.const J).obj c.pt).obj a_1) : Type u))
          ((⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u)) ⁻¹' s))) ↔
    IsOpen s
⊢ IsOpen (X := (↑(K.obj a_1) : Type u))
      (Set.preimage (β := (↑(Functor.obj.{w', u, w, u + 1} (Functor.obj (Functor.const J) c.pt) a_1) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app a_1)) :
          (a : (↑(K.obj a_1) : Type u)) → (↑(((Functor.const J).obj c.pt).obj a_1) : Type u))
        ((⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u)) ⁻¹' s)) ↔
    IsOpen s

Tactic:
rw [Homeomorph.ulift.isOpenEmbedding.isOpen_iff_preimage_isOpen (by simp)]

Premises used: Topology.IsOpenEmbedding.isOpen_iff_preimage_isOpen, Homeomorph.ulift, Homeomorph.isOpenEmbedding
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
s : Set (↑(uliftFunctor.mapCocone c).pt : Type (max u v))
a : J
⊢ IsOpen (X := ULift.{v, u} (↑(K.obj a) : Type u))
      (Set.preimage (β := (↑(K.obj a) : Type u))
        (⇑Homeomorph.ulift : (a_1 : ULift.{v, u} (↑(K.obj a) : Type u)) → (↑(K.obj a) : Type u))
        (Set.preimage (β := (↑(Functor.obj.{w', u, w, u + 1} (Functor.obj (Functor.const J) c.pt) a) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app a)) :
            (a_1 : (↑(K.obj a) : Type u)) → (↑(((Functor.const J).obj c.pt).obj a) : Type u))
          ((⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u)) ⁻¹' s))) ↔
    IsOpen s

Tactic:
rfl