awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
A : Set X
hA : A ⊆ (↑E : Set X)
h :
  (∀ (n : ℕ) (j : (↑(E.I (C := C) (D := D) n) : Type u_1)),
      IsClosed[t] (A ∩ (↑(map (C := C) (D := D) n (↑j : cell C n)) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[t] (A ∩ D)
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
pos :
  ∀ (hj : j ∈ E.I (C := C) (D := D) n),
    Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
neg :
  ∀ (hj : j ∉ E.I (C := C) (D := D) n),
    Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
⊢ Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)

Tactic:
by_cases hj : j ∈ E.I n

Premises used: Topology.RelCWComplex.Subcomplex.I
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
A : Set X
hA : A ⊆ (↑E : Set X)
h :
  (∀ (n : ℕ) (j : (↑(E.I (C := C) (D := D) n) : Type u_1)),
      IsClosed[t] (A ∩ (↑(map (C := C) (D := D) n (↑j : cell C n)) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[t] (A ∩ D)
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
hj : j ∈ E.I (C := C) (D := D) n
⊢ Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)

Tactic:
Or.intro_right _ (h.1 n ⟨j, hj⟩)

Premises used: Or.intro_right, Subtype.mk, And.left
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
A : Set X
hA : A ⊆ (↑E : Set X)
h :
  (∀ (n : ℕ) (j : (↑(E.I (C := C) (D := D) n) : Type u_1)),
      IsClosed[t] (A ∩ (↑(map (C := C) (D := D) n (↑j : cell C n)) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[t] (A ∩ D)
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
hj : j ∈ E.I (C := C) (D := D) n
⊢ Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)

Tactic:
exact Or.intro_right _ (h.1 n ⟨j, hj⟩)

Premises used: Or.intro_right, Subtype.mk, And.left
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
A : Set X
hA : A ⊆ (↑E : Set X)
h :
  (∀ (n : ℕ) (j : (↑(E.I (C := C) (D := D) n) : Type u_1)),
      IsClosed[t] (A ∩ (↑(map (C := C) (D := D) n (↑j : cell C n)) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[t] (A ∩ D)
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
hj : j ∉ E.I (C := C) (D := D) n
⊢ Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)

Tactic:
Or.intro_left _ ((disjoint_openCell_subcomplex_of_not_mem E hj).symm.mono_left hA)

Premises used: Or.intro_left, Disjoint.mono_left, Disjoint.symm, Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
A : Set X
hA : A ⊆ (↑E : Set X)
h :
  (∀ (n : ℕ) (j : (↑(E.I (C := C) (D := D) n) : Type u_1)),
      IsClosed[t] (A ∩ (↑(map (C := C) (D := D) n (↑j : cell C n)) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[t] (A ∩ D)
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
hj : j ∉ E.I (C := C) (D := D) n
⊢ Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)

Tactic:
exact Or.intro_left _ ((disjoint_openCell_subcomplex_of_not_mem E hj).symm.mono_left hA)

Premises used: Or.intro_left, Disjoint.mono_left, Disjoint.symm, Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : T2Space X
inst_1 : CWComplex C
E : Subcomplex C (D := ∅)
n : ℕ
⊢ @cell _ t (↑E : Set X) ∅ _ n = (↑(E.I (C := C) (D := ∅) n) : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : T2Space X
inst_1 : CWComplex C
E : Subcomplex C (D := ∅)
n : ℕ
i : (↑(E.I (C := C) (D := ∅) n) : Type u_1)
⊢ @map _ t (↑E : Set X) ∅ _ n i = map (C := C) (D := ∅) n (↑i : cell C n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
⊢ openCell (C := (↑E : Set X)) (D := D) n i = openCell (C := C) (D := D) n (↑i : cell C n)

Tactic:
rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
⊢ closedCell (C := (↑E : Set X)) (D := D) n i = closedCell (C := C) (D := D) n (↑i : cell C n)

Tactic:
rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
⊢ cellFrontier (C := (↑E : Set X)) (D := D) n i = cellFrontier (C := C) (D := D) n (↑i : cell C n)

Tactic:
rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
inst_2 : FiniteDimensional C (D := D)
E : Subcomplex C (D := D)
h : ∀ (n : ℕ) (hn : IsEmpty.{u_1 + 1} (@cell _ t C D _ n)), IsEmpty.{u_1 + 1} (@cell _ t (↑E : Set X) D _ n)
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u_1 + 1} (@cell _ t (↑E : Set X) D _ n)

Tactic:
filter_upwards [FiniteDimensional.eventually_isEmpty_cell (C := C) (D := D)] with n hn

Premises used: Topology.RelCWComplex.FiniteDimensional.eventually_isEmpty_cell
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
inst_2 : FiniteDimensional C (D := D)
E : Subcomplex C (D := D)
n : ℕ
hn : IsEmpty.{u_1 + 1} (@cell _ t C D _ n)
⊢ IsEmpty.{u_1 + 1} (@cell _ t (↑E : Set X) D _ n)

Tactic:
simp [isEmpty_subtype]

Premises used: isEmpty_subtype
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
inst_2 : Finite C (D := D)
E : Subcomplex C (D := D)
⊢ Finite (↑E : Set X) (D := D)

Tactic:
finite_of_finiteDimensional_finiteType _

Premises used: Topology.RelCWComplex.finite_of_finiteDimensional_finiteType
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X : CompHaus
⊢ CompactSpace.{u_1} (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)

Tactic:
X.is_compact

Premises used: CompHausLike.is_compact
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X : CompHaus
⊢ T2Space.{u_1} (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)

Tactic:
X.is_hausdorff

Premises used: CompHausLike.is_hausdorff
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
⊢ HasProp (fun (x : TopCat.{u_1}) ↦ True) X

Tactic:
⟨trivial⟩

Premises used: trivial, CompHausLike.HasProp.mk
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X : TopCat
Y : CompHaus
f :
  (↑((stoneCechObj X).toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) →
    (↑(Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
hf : Continuous f
x : (↑(toTop (P := fun (x : TopCat.{u}) ↦ True) (of (fun (x : TopCat.{u}) ↦ True) (StoneCech (↑X : Type u)))) : Type u)
y : (↑X : Type u)
apply :
  Continuous.{u, u} (X := (↑X : Type u)) (Y := (↑((stoneCechObj X).toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
    stoneCechUnit
⊢ stoneCechExtend (g :=
      ContinuousMap.toFun
        (TopCat.Hom.hom
          ((fun (f : stoneCechObj X ⟶ Y) ↦
              TopCat.ofHom
                {
                  toFun :=
                    Function.comp (β :=
                      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                          (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
                        (stoneCechObj X))
                      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
                            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
                        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (stoneCechObj X)) →
                          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y)
                      stoneCechUnit,
                  continuous_toFun := ⋯ : C((↑X : Type u), (↑Y.1 : Type u)) })
            {
              hom :=
                {
                  hom' :=
                    { toFun := f, continuous_toFun := hf :
                      C((↑((stoneCechObj X).toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                        (↑(Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) } :
                  (stoneCechObj X).toTop (P := fun (x : TopCat.{u}) ↦ True).Hom
                    (Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) } :
              InducedCategory.Hom (D := TopCat) (F := toTop (P := fun (x : TopCat.{u}) ↦ True)) (stoneCechObj X) Y })))
      ⋯ (stoneCechUnit y) =
    f (stoneCechUnit y)

Tactic:
apply congr_fun (stoneCechExtend_extends (hf.comp _)) y

Premises used: Continuous.comp, stoneCechExtend_extends, congr_fun
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X : TopCat
Y : CompHaus
f :
  (↑((stoneCechObj X).toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) →
    (↑(Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
hf : Continuous f
x : (↑(toTop (P := fun (x : TopCat.{u}) ↦ True) (of (fun (x : TopCat.{u}) ↦ True) (StoneCech (↑X : Type u)))) : Type u)
y : (↑X : Type u)
⊢ Continuous.{u, u} (X := (↑X : Type u)) (Y := (↑((stoneCechObj X).toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
    stoneCechUnit

Tactic:
apply continuous_stoneCechUnit

Premises used: continuous_stoneCechUnit
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X : TopCat
Y : CompHaus
f : (↑X : Type u) → (↑(compHausToTop.obj Y) : Type u)
hf : Continuous f
x : (↑(TopCat.of (↑X : Type u)) : Type u)
⊢ Eq (α := (↑(TopCat.of (↑Y.1 : Type u)) : Type u))
    ((@ConcreteCategory.hom _ TopCat.instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
            TopCat.carrier _ _ (TopCat.of (↑X : Type u)) (TopCat.of (↑Y.1 : Type u))
            ((fun (f : stoneCechObj X ⟶ Y) ↦
                TopCat.ofHom
                  {
                    toFun :=
                      Function.comp (β :=
                        (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
                          (stoneCechObj X))
                        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                              C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                                (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
                              (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
                          (a :
                              (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (stoneCechObj X)) →
                            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y)
                        stoneCechUnit,
                    continuous_toFun := ⋯ : C((↑X : Type u), (↑Y.1 : Type u)) })
              ((fun (f : X ⟶ compHausToTop.obj Y) ↦
                  (ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := stoneCechExtend ⋯, continuous_toFun := ⋯ } :
                    Quiver.Hom (V := CompHausLike fun (x : TopCat.{u}) ↦ True)
                      (of (fun (x : TopCat.{u}) ↦ True) (StoneCech (↑X : Type u)))
                      (of (fun (x : TopCat.{u}) ↦ True) (↑Y.1 : Type u))))
                { hom' := { toFun := f, continuous_toFun := hf } })) :
          (a : (↑(TopCat.of (↑X : Type u)) : Type u)) → (↑(TopCat.of (↑Y.1 : Type u)) : Type u))
        x :
      (↑(TopCat.of (↑Y.1 : Type u)) : Type u))
    ((@ConcreteCategory.hom _ TopCat.instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
            TopCat.carrier _ _ (TopCat.of (↑X : Type u)) (TopCat.of (↑Y.1 : Type u))
            { hom' := { toFun := f, continuous_toFun := hf : C((↑X : Type u), (↑(compHausToTop.obj Y) : Type u)) } :
              X.Hom (compHausToTop.obj Y) } :
          (a : (↑(TopCat.of (↑X : Type u)) : Type u)) → (↑(TopCat.of (↑Y.1 : Type u)) : Type u))
        x :
      (↑(TopCat.of (↑Y.1 : Type u)) : Type u))

Tactic:
congr_fun (stoneCechExtend_extends hf) _

Premises used: Classical.epsilon, Set.Mem, preStoneCechExtend, T2Quotient.lift, stoneCechExtend_extends, Ultrafilter.extend, Filter.lim, congr_fun, Filter.limUnder, stoneCechExtend, IsDenseInducing.extend
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X : TopCat
Y : CompHaus
f : (↑X : Type u) → (↑(compHausToTop.obj Y) : Type u)
hf : Continuous f
x : (↑(TopCat.of (↑X : Type u)) : Type u)
⊢ Eq (α := (↑(TopCat.of (↑Y.1 : Type u)) : Type u))
    ((@ConcreteCategory.hom _ TopCat.instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
            TopCat.carrier _ _ (TopCat.of (↑X : Type u)) (TopCat.of (↑Y.1 : Type u))
            ((fun (f : stoneCechObj X ⟶ Y) ↦
                TopCat.ofHom
                  {
                    toFun :=
                      Function.comp (β :=
                        (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
                          (stoneCechObj X))
                        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                              C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                                (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
                              (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
                          (a :
                              (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (stoneCechObj X)) →
                            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y)
                        stoneCechUnit,
                    continuous_toFun := ⋯ : C((↑X : Type u), (↑Y.1 : Type u)) })
              ((fun (f : X ⟶ compHausToTop.obj Y) ↦
                  (ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := stoneCechExtend ⋯, continuous_toFun := ⋯ } :
                    Quiver.Hom (V := CompHausLike fun (x : TopCat.{u}) ↦ True)
                      (of (fun (x : TopCat.{u}) ↦ True) (StoneCech (↑X : Type u)))
                      (of (fun (x : TopCat.{u}) ↦ True) (↑Y.1 : Type u))))
                { hom' := { toFun := f, continuous_toFun := hf } })) :
          (a : (↑(TopCat.of (↑X : Type u)) : Type u)) → (↑(TopCat.of (↑Y.1 : Type u)) : Type u))
        x :
      (↑(TopCat.of (↑Y.1 : Type u)) : Type u))
    ((@ConcreteCategory.hom _ TopCat.instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
            TopCat.carrier _ _ (TopCat.of (↑X : Type u)) (TopCat.of (↑Y.1 : Type u))
            { hom' := { toFun := f, continuous_toFun := hf : C((↑X : Type u), (↑(compHausToTop.obj Y) : Type u)) } :
              X.Hom (compHausToTop.obj Y) } :
          (a : (↑(TopCat.of (↑X : Type u)) : Type u)) → (↑(TopCat.of (↑Y.1 : Type u)) : Type u))
        x :
      (↑(TopCat.of (↑Y.1 : Type u)) : Type u))

Tactic:
exact congr_fun (stoneCechExtend_extends hf) _

Premises used: stoneCechExtend_extends, congr_fun
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X : TopCat
⊢ (↑((topToCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) = StoneCech (↑X : Type u_1)

Tactic:
rfl

Premises used: T2Quotient, Quotient, rfl, StoneCech
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
⊢ Limits.HasLimits CompHaus

Tactic:
hasLimits_of_hasLimits_createsLimits compHausToTop

Premises used: CategoryTheory.hasLimits_of_hasLimits_createsLimits, compHausToTop
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
⊢ Limits.HasColimits CompHaus

Tactic:
hasColimits_of_reflective compHausToTop

Premises used: CategoryTheory.hasColimits_of_reflective, compHausToTop
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
change :
  CompactSpace
    (↑{u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
          ∀ {i j : J} (f : i ⟶ j),
            (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                    C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                      (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                    (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                    (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
                  (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
                (u i) =
              u j} :
      Type (max u v))
⊢ CompactSpace (↑(TopCat.limitCone.{v, u, v} FF).pt : Type (max u v))

Tactic:
change CompactSpace { u : ∀ j, F.obj j | ∀ {i j : J} (f : i ⟶ j), (F.map f) (u i) = u j }

Premises used: setOf, Set.Elem, CompactSpace
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
rw :
  IsCompact (X := (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
    {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                  (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
              (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
            (u i) =
          u j}
⊢ CompactSpace
    (↑{u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
          ∀ {i j : J} (f : i ⟶ j),
            (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                    C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                      (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                    (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                    (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
                  (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
                (u i) =
              u j} :
      Type (max u v))

Tactic:
rw [← isCompact_iff_compactSpace]

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
h :
  IsClosed (X := (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
    {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                  (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
              (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
            (u i) =
          u j}
⊢ IsCompact (X := (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
    {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                  (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
              (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
            (u i) =
          u j}

Tactic:
apply IsClosed.isCompact

Premises used: IsClosed.isCompact