awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
x : X.A
F : Ultrafilter X.A
h1 : F ∈ basic A
h2 : X.str F = x
⊢ ∃ (u : Ultrafilter X.A), A ∈ u ∧ (↑u : Filter X.A) ≤ 𝓝 x

Tactic:
⟨F, h1, le_nhds_of_str_eq _ _ h2⟩

Premises used: Compactum.le_nhds_of_str_eq, And.intro, Exists.intro
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
x : X.A
F : Ultrafilter X.A
h1 : F ∈ basic A
h2 : X.str F = x
⊢ ∃ (u : Ultrafilter X.A), A ∈ u ∧ (↑u : Filter X.A) ≤ 𝓝 x

Tactic:
exact ⟨F, h1, le_nhds_of_str_eq _ _ h2⟩
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
x : X.A
F : Ultrafilter X.A
h1 : A ∈ F
h2 : (↑F : Filter X.A) ≤ 𝓝 x
⊢ x ∈ cl A

Tactic:
⟨F, h1, str_eq_of_le_nhds _ _ h2⟩

Premises used: Set.Mem, setOf, _private.0.Compactum.cl, And.intro, Exists.intro, Set.image, Compactum.str_eq_of_le_nhds
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
x : X.A
F : Ultrafilter X.A
h1 : A ∈ F
h2 : (↑F : Filter X.A) ≤ 𝓝 x
⊢ x ∈ cl A

Tactic:
exact ⟨F, h1, str_eq_of_le_nhds _ _ h2⟩
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
f : X ⟶ Y
rw :
  ∀ (x : X.A) (g : Ultrafilter X.A),
    (↑g : Filter X.A) ≤ 𝓝 x →
      Tendsto («β» := Y.A)
        ((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f) :
            (a : X.A) → Y.A) :
          (a : X.A) → Y.A)
        (↑g : Filter X.A)
        (𝓝
            ((ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f :
                (a : X.A) → Y.A)
              x) :
          Filter Y.A)
⊢ Continuous (X := X.A) (Y := Y.A)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f) :
      (a : X.A) → Y.A)

Tactic:
rw [continuous_iff_ultrafilter]

Premises used: continuous_iff_ultrafilter
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : (↑g : Filter X.A) ≤ 𝓝 x
a :
  Y.str
      (Ultrafilter.map
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f) :
          (a : X.A) → Y.A)
        g) =
    (ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f : (a : X.A) → Y.A) x
⊢ LE.le (α := Filter Y.A)
    ((↑(Ultrafilter.map
            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f) :
              (a : X.A) → Y.A)
            g) :
        Filter Y.A) :
      Filter Y.A)
    (𝓝
        ((ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f :
            (a : X.A) → Y.A)
          x) :
      Filter Y.A)

Tactic:
apply le_nhds_of_str_eq

Premises used: Compactum.le_nhds_of_str_eq
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h rw : (↑g : Filter X.A) ≤ 𝓝 x
⊢ Y.str
      (Ultrafilter.map
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f) :
          (a : X.A) → Y.A)
        g) =
    (ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f : (a : X.A) → Y.A) x

Tactic:
rw [← str_hom_commute, str_eq_of_le_nhds _ x _]

Premises used: Compactum.str_hom_commute, Compactum.str_eq_of_le_nhds
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : (↑g : Filter X.A) ≤ 𝓝 x
⊢ (↑g : Filter X.A) ≤ 𝓝 x

Tactic:
apply h
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h :
  ∀ (x : Functor.obj (𝟭 (Type u_1)) X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (β.η.app X ≫ ↾Ultrafilter.lim)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)).toFun x
⊢ β.η.app X ≫ ↾Ultrafilter.lim = 𝟙 X

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
x : Functor.obj (𝟭 (Type u_1)) X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.η.app X ≫ ↾Ultrafilter.lim)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)).toFun x

Tactic:
lim_eq (pure_le_nhds _)

Premises used: Classical.epsilon, lim_eq, pure_le_nhds, Filter.lim, Ultrafilter.lim
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
x : Functor.obj (𝟭 (Type u_1)) X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.η.app X ≫ ↾Ultrafilter.lim)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)).toFun x

Tactic:
exact lim_eq (pure_le_nhds _)

Premises used: lim_eq, pure_le_nhds
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h :
  ∀ (FF : (β.toFunctor ⋙ β.toFunctor).obj X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X ≫ ↾Ultrafilter.lim)).toFun FF =
      TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF
⊢ β.μ.app X ≫ ↾Ultrafilter.lim = β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim

Tactic:
ext FF
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : (β.toFunctor ⋙ β.toFunctor).obj X
h :
  ∀ (FF : Ultrafilter (Ultrafilter X)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X ≫ ↾Ultrafilter.lim)).toFun FF =
      TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X ≫ ↾Ultrafilter.lim)).toFun FF =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF

Tactic:
change Ultrafilter (Ultrafilter X) at FF

Premises used: Ultrafilter
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
⊢ let x := (Ultrafilter.map Ultrafilter.lim FF).lim;
  x = (Ultrafilter.map Ultrafilter.lim FF).lim

Tactic:
set x := (Ultrafilter.map Ultrafilter.lim FF).lim with c1

Premises used: Ultrafilter.lim, Ultrafilter.map
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
U : Set X
F : Ultrafilter X
h1 : F.lim ∈ U
hU : IsOpen[inst] U
⊢ U ∈ F

Tactic:
isOpen_iff_ultrafilter.mp hU _ h1 _ (Ultrafilter.le_nhds_lim _)

Premises used: isOpen_iff_ultrafilter, Ultrafilter.le_nhds_lim, Iff.mp
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
U : Set X
F : Ultrafilter X
h1 : F.lim ∈ U
hU : IsOpen[inst] U
⊢ U ∈ F

Tactic:
exact isOpen_iff_ultrafilter.mp hU _ h1 _ (Ultrafilter.le_nhds_lim _)

Premises used: isOpen_iff_ultrafilter, Ultrafilter.le_nhds_lim, Iff.mp
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
⊢ ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F

Tactic:
have c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen U → U ∈ F := by
      intro U F h1 hU
      exact isOpen_iff_ultrafilter.mp hU _ h1 _ (Ultrafilter.le_nhds_lim _)
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
rw : ∀ (s : Set X), x ∈ s → IsOpen[inst] s → s ∈ (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X)
⊢ (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x

Tactic:
rw [le_nhds_iff]

Premises used: le_nhds_iff
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
rwa rwa₁ rwa₂ rwa₃ : x ∈ U
⊢ (Ultrafilter.map Ultrafilter.lim FF).lim ∈ U

Tactic:
rwa [← c1]
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
⊢ U ∈ (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X)

Tactic:
exact mem_coe.2 (c2 _ _ (by rwa [← c1]) hU)

Premises used: Iff.mpr, Ultrafilter.mem_coe
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
⊢ (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x

Tactic:
have c3 : ↑(Ultrafilter.map Ultrafilter.lim FF) ≤ 𝓝 x := by
      rw [le_nhds_iff]
      intro U hx hU
      exact mem_coe.2 (c2 _ _ (by rwa [← c1]) hU)
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
this : Ultrafilter.lim ⁻¹' U ∈ FF
apply : Ultrafilter.lim ⁻¹' U ⊆ {G : Ultrafilter X | U ∈ G}
⊢ {G : Ultrafilter X | U ∈ G} ∈ FF

Tactic:
apply mem_of_superset this

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
this : Ultrafilter.lim ⁻¹' U ∈ FF
P : Ultrafilter X
hP : P ∈ Ultrafilter.lim ⁻¹' U
⊢ Membership.mem (γ := Set (Ultrafilter X)) {G : Ultrafilter X | U ∈ G} P

Tactic:
c2 U P hP hU

Premises used: Set.Mem, setOf
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
this : Ultrafilter.lim ⁻¹' U ∈ FF
P : Ultrafilter X
hP : P ∈ Ultrafilter.lim ⁻¹' U
⊢ Membership.mem (γ := Set (Ultrafilter X)) {G : Ultrafilter X | U ∈ G} P

Tactic:
exact c2 U P hP hU
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
suffices : Ultrafilter.lim ⁻¹' U ∈ FF
⊢ {G : Ultrafilter X | U ∈ G} ∈ FF

Tactic:
suffices Ultrafilter.lim ⁻¹' U ∈ FF by
        apply mem_of_superset this
        intro P hP
        exact c2 U P hP hU
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
⊢ Ultrafilter.lim ⁻¹' U ∈ FF

Tactic:
@c3 U (IsOpen.mem_nhds hU hx)

Premises used: Set.Mem, setOf, Set.preimage, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
⊢ Ultrafilter.lim ⁻¹' U ∈ FF

Tactic:
exact @c3 U (IsOpen.mem_nhds hU hx)

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
⊢ ∀ (U : Set X), x ∈ U → IsOpen[inst] U → {G : Ultrafilter X | U ∈ G} ∈ FF

Tactic:
have c4 : ∀ U : Set X, x ∈ U → IsOpen U → { G : Ultrafilter X | U ∈ G } ∈ FF := by
      intro U hx hU
      suffices Ultrafilter.lim ⁻¹' U ∈ FF by
        apply mem_of_superset this
        intro P hP
        exact c2 U P hP hU
      exact @c3 U (IsOpen.mem_nhds hU hx)
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
c4 : ∀ (U : Set X), x ∈ U → IsOpen[inst] U → {G : Ultrafilter X | U ∈ G} ∈ FF
h :
  (↑((β.μ.app X).hom'.toFun FF) : Filter X) ≤
    𝓝 (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X ≫ ↾Ultrafilter.lim)).toFun FF =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF

Tactic:
apply lim_eq

Premises used: lim_eq
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
c4 : ∀ (U : Set X), x ∈ U → IsOpen[inst] U → {G : Ultrafilter X | U ∈ G} ∈ FF
h :
  ∀ (s : Set X),
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF ∈ s →
      IsOpen[inst] s → s ∈ (↑((β.μ.app X).hom'.toFun FF) : Filter X)
⊢ (↑((β.μ.app X).hom'.toFun FF) : Filter X) ≤
    𝓝 (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF)

Tactic:
rw [le_nhds_iff]

Premises used: le_nhds_iff
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
c4 : ∀ (U : Set X), x ∈ U → IsOpen[inst] U → {G : Ultrafilter X | U ∈ G} ∈ FF
⊢ ∀ (s : Set X),
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF ∈ s →
      IsOpen[inst] s → s ∈ (↑((β.μ.app X).hom'.toFun FF) : Filter X)

Tactic:
c4

Premises used: Classical.epsilon, Set.Mem, setOf, Set.preimage, Filter.lim, Ultrafilter.lim
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
c4 : ∀ (U : Set X), x ∈ U → IsOpen[inst] U → {G : Ultrafilter X | U ∈ G} ∈ FF
⊢ ∀ (s : Set X),
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF ∈ s →
      IsOpen[inst] s → s ∈ (↑((β.μ.app X).hom'.toFun FF) : Filter X)

Tactic:
exact c4
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
f : X.A → Y.A
cont : Continuous f
⊢ ∀ (x : X.A) (g : Ultrafilter X.A), (↑g : Filter X.A) ≤ 𝓝 x → Tendsto f (↑g : Filter X.A) (𝓝 (f x))

Tactic:
rw [continuous_iff_ultrafilter] at cont

Premises used: continuous_iff_ultrafilter
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
f : X.A → Y.A
cont : ∀ (x : X.A) (g : Ultrafilter X.A), (↑g : Filter X.A) ≤ 𝓝 x → Tendsto f (↑g : Filter X.A) (𝓝 (f x))
h :
  ∀ (F : Ultrafilter X.A),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾f) ≫ Y.a)).toFun F =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.a ≫ ↾f)).toFun F
⊢ β.map (↾f) ≫ Y.a = X.a ≫ ↾f

Tactic:
ext (F : Ultrafilter X)

Premises used: CategoryTheory.Monad.Algebra.A, Ultrafilter
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
f : X.A → Y.A
cont : ∀ (x : X.A) (g : Ultrafilter X.A), (↑g : Filter X.A) ≤ 𝓝 x → Tendsto f (↑g : Filter X.A) (𝓝 (f x))
F : Ultrafilter X.A
⊢ Tendsto f (↑F : Filter X.A) (𝓝 (f (X.str F)))

Tactic:
specialize cont (X.str F) F (le_nhds_of_str_eq F (X.str F) rfl)

Premises used: Compactum.le_nhds_of_str_eq, Compactum.str, rfl
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
f : X.A → Y.A
F : Ultrafilter X.A
cont : Tendsto f (↑F : Filter X.A) (𝓝 (f (X.str F)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾f) ≫ Y.a)).toFun F =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.a ≫ ↾f)).toFun F

Tactic:
simpa using str_eq_of_le_nhds (Ultrafilter.map f F) _ cont

Premises used: Ultrafilter.map, Compactum.str_eq_of_le_nhds
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
_ : ∀ {Y : Compactum.{u_1}}, Function.Injective (α := X ⟶ Y) compactumToCompHaus.map
⊢ ∀ {Y : Compactum.{u_1}}, Function.Injective (α := X ⟶ Y) compactumToCompHaus.map

Tactic:
_
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
_ : ∀ ⦃a₁ a₂ : X ⟶ Y⦄, compactumToCompHaus.map a₁ = compactumToCompHaus.map a₂ → a₁ = a₂
⊢ Function.Injective (α := X ⟶ Y) compactumToCompHaus.map

Tactic:
_
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
a₁ : X ⟶ Y
_ : ∀ ⦃a₂ : X ⟶ Y⦄, compactumToCompHaus.map a₁ = compactumToCompHaus.map a₂ → a₁ = a₂
⊢ ∀ ⦃a₂ : X ⟶ Y⦄, compactumToCompHaus.map a₁ = compactumToCompHaus.map a₂ → a₁ = a₂

Tactic:
_
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
a₁ a₂ : X ⟶ Y
h : compactumToCompHaus.map a₁ = compactumToCompHaus.map a₂
f : a₁.f = a₂.f
⊢ a₁ = a₂

Tactic:
apply Monad.Algebra.Hom.ext

Premises used: CategoryTheory.Monad.Algebra.Hom.ext
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
a₁ a₂ : X ⟶ Y
h : compactumToCompHaus.map a₁ = compactumToCompHaus.map a₂
f :
  ∀ (x : X.A),
    (ConcreteCategory.hom (FC := TypeCat.Fun) a₁.f).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) a₂.f).toFun x
⊢ a₁.f = a₂.f

Tactic:
ext
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
a₁ a₂ : X ⟶ Y
h : compactumToCompHaus.map a₁ = compactumToCompHaus.map a₂
x : X.A
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) a₁.f).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) a₂.f).toFun x

Tactic:
simpa using ConcreteCategory.congr_hom h _

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Topology.Category.Compactum
Goal:
D : CompHaus
x : Set (↑D.1 : Type u_1)
h : IsOpen x
⊢ ∀ (F : Ultrafilter (↑D.1 : Type u_1)), F.lim ∈ x → x ∈ (↑F : Filter (↑D.1 : Type u_1))

Tactic:
rw [isOpen_iff_ultrafilter'] at h

Premises used: isOpen_iff_ultrafilter'
-- Module: Mathlib.Topology.Category.Compactum
Goal:
D : CompHaus
x : Set (↑D.1 : Type u_1)
h : ∀ (F : Ultrafilter (↑D.1 : Type u_1)), F.lim ∈ x → x ∈ (↑F : Filter (↑D.1 : Type u_1))
⊢ IsOpen (id ⁻¹' x)

Tactic:
h

Premises used: Classical.epsilon, Set.Mem, setOf, Set.preimage, Compactum.str, Filter.lim, Ultrafilter.lim, IsOpen
-- Module: Mathlib.Topology.Category.Compactum
Goal:
D : CompHaus
x : Set (↑D.1 : Type u_1)
h : ∀ (F : Ultrafilter (↑D.1 : Type u_1)), F.lim ∈ x → x ∈ (↑F : Filter (↑D.1 : Type u_1))
⊢ IsOpen (id ⁻¹' x)

Tactic:
exact h
-- Module: Mathlib.Topology.Category.Compactum
Goal:
D : CompHaus
x : Set (Compactum.ofTopologicalSpace (↑(D.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)).A
h1 : IsOpen x
rw : ∀ (F : Ultrafilter (↑D.1 : Type u_1)), F.lim ∈ id ⁻¹' x → id ⁻¹' x ∈ (↑F : Filter (↑D.1 : Type u_1))
⊢ IsOpen (id ⁻¹' x)

Tactic:
rw [isOpen_iff_ultrafilter']

Premises used: isOpen_iff_ultrafilter'
-- Module: Mathlib.Topology.Category.Compactum
Goal:
D : CompHaus
x : Set (Compactum.ofTopologicalSpace (↑(D.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)).A
h1 : IsOpen x
F : Ultrafilter (↑D.1 : Type u_1)
h2 : F.lim ∈ id ⁻¹' x
⊢ id ⁻¹' x ∈ (↑F : Filter (↑D.1 : Type u_1))

Tactic:
h1 _ h2

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.Category.Compactum
Goal:
D : CompHaus
x : Set (Compactum.ofTopologicalSpace (↑(D.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)).A
h1 : IsOpen x
F : Ultrafilter (↑D.1 : Type u_1)
h2 : F.lim ∈ id ⁻¹' x
⊢ id ⁻¹' x ∈ (↑F : Filter (↑D.1 : Type u_1))

Tactic:
exact h1 _ h2
-- Module: Mathlib.Topology.Category.Compactum
Goal:
⊢ compactumToCompHaus.EssSurj

Tactic:
{ mem_essImage := fun X => ⟨Compactum.ofTopologicalSpace X,
      ⟨isoOfTopologicalSpace⟩⟩ }

Premises used: compactumToCompHaus.isoOfTopologicalSpace, Compactum.ofTopologicalSpace, CategoryTheory.Functor.EssSurj.mk, Nonempty.intro, TopCat.carrier, Exists.intro, CompHausLike.toTop