awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
x x_1 : X ⟶ Y
h :
  Eq.{u_1 + 1} (α := (a : X.A) → Y.A)
    ((fun (f : X ⟶ Y) ↦
        ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.f) :
            (a : (fun (X : Type u_1) ↦ X) X.A) → (fun (X : Type u_1) ↦ X) Y.A) :
          (a : (fun (X : Type u_1) ↦ X) X.A) → (fun (X : Type u_1) ↦ X) Y.A))
      x)
    ((fun (f : X ⟶ Y) ↦
        ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.f) :
            (a : (fun (X : Type u_1) ↦ X) X.A) → (fun (X : Type u_1) ↦ X) Y.A) :
          (a : (fun (X : Type u_1) ↦ X) X.A) → (fun (X : Type u_1) ↦ X) Y.A))
      x_1)
⊢ β.forget.map x = β.forget.map x_1

Tactic:
aesop
-- Module: Mathlib.Topology.Category.Compactum
Goal:
⊢ HasLimits Compactum

Tactic:
hasLimits_of_hasLimits_createsLimits forget

Premises used: Compactum.forget, CategoryTheory.hasLimits_of_hasLimits_createsLimits
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
x : X.A
change :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (β.η.app X.A ≫ X.a) :
        (a : (fun (X : Type u_1) ↦ X) ((𝟭 (Type u_1)).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
      x =
    x
⊢ X.str (X.incl x) = x

Tactic:
change ((β).η.app _ ≫ X.a) _ = _

Premises used: CategoryTheory.Monad.Algebra.a, CategoryTheory.ConcreteCategory.hom, CategoryTheory.ofTypeMonad, CategoryTheory.Monad.η, CategoryTheory.CategoryStruct.comp, Ultrafilter, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
x : X.A
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X.A) :
        (a : (fun (X : Type u_1) ↦ X) ((𝟭 (Type u_1)).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
      x =
    x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.η.app X.A ≫ X.a) :
        (a : (fun (X : Type u_1) ↦ X) ((𝟭 (Type u_1)).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
      x =
    x

Tactic:
rw [Monad.Algebra.unit]

Premises used: CategoryTheory.Monad.Algebra.unit
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
x : X.A
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X.A) :
        (a : (fun (X : Type u_1) ↦ X) ((𝟭 (Type u_1)).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
      x =
    x

Tactic:
rfl
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
change :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.a ≫ f.f) :
        (a : (fun (X : Type u_1) ↦ X) (β.obj X.A)) → (fun (X : Type u_1) ↦ X) Y.A)
      xs =
    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)
        xs)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f : (a : X.A) → Y.A)
      (X.str xs) =
    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)
        xs)

Tactic:
change (X.a ≫ f.f) _ = _

Premises used: CategoryTheory.Monad.Algebra.a, CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.comp, CategoryTheory.Monad.Algebra.Hom.f, DFunLike.coe
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map f.f ≫ Y.a) :
        (a : (fun (X : Type u_1) ↦ X) (β.obj X.A)) → (fun (X : Type u_1) ↦ X) Y.A)
      xs =
    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)
        xs)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.a ≫ f.f) :
        (a : (fun (X : Type u_1) ↦ X) (β.obj X.A)) → (fun (X : Type u_1) ↦ X) Y.A)
      xs =
    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)
        xs)

Tactic:
rw [← f.h]

Premises used: CategoryTheory.Monad.Algebra.Hom.h
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map f.f ≫ Y.a) :
        (a : (fun (X : Type u_1) ↦ X) (β.obj X.A)) → (fun (X : Type u_1) ↦ X) Y.A)
      xs =
    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)
        xs)

Tactic:
rfl
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
change :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X.A ≫ X.a) :
        (a : (fun (X : Type u_1) ↦ X) ((β.toFunctor ⋙ β.toFunctor).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
      uux =
    X.str (Ultrafilter.map X.str uux)
⊢ X.str (X.join uux) = X.str (Ultrafilter.map X.str uux)

Tactic:
change ((β).μ.app _ ≫ X.a) _ = _

Premises used: CategoryTheory.Monad.Algebra.a, CategoryTheory.ConcreteCategory.hom, CategoryTheory.ofTypeMonad, CategoryTheory.Monad.μ, CategoryTheory.CategoryStruct.comp, Ultrafilter, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map X.a ≫ X.a) :
        (a : (fun (X : Type u_1) ↦ X) ((β.toFunctor ⋙ β.toFunctor).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
      uux =
    X.str (Ultrafilter.map X.str uux)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X.A ≫ X.a) :
        (a : (fun (X : Type u_1) ↦ X) ((β.toFunctor ⋙ β.toFunctor).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
      uux =
    X.str (Ultrafilter.map X.str uux)

Tactic:
rw [Monad.Algebra.assoc]

Premises used: CategoryTheory.Monad.Algebra.assoc
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map X.a ≫ X.a) :
        (a : (fun (X : Type u_1) ↦ X) ((β.toFunctor ⋙ β.toFunctor).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
      uux =
    X.str (Ultrafilter.map X.str uux)

Tactic:
rfl
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
S : Set X.A
rw : IsOpen Sᶜ ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
⊢ IsClosed S ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

Tactic:
rw [← isOpen_compl_iff]

Premises used: isOpen_compl_iff
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
S : Set X.A
mp : IsOpen Sᶜ → ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
mpr : (∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S) → IsOpen Sᶜ
⊢ IsOpen Sᶜ ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

Tactic:
constructor
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
S : Set X.A
cond : IsOpen Sᶜ
F : Ultrafilter X.A
h : S ∈ F
mp : ∀ (c : X.str F ∉ S), False
⊢ X.str F ∈ S

Tactic:
by_contra c
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
S : Set X.A
cond : IsOpen Sᶜ
F : Ultrafilter X.A
h : S ∈ F
c : X.str F ∉ S
⊢ Sᶜ ∈ F

Tactic:
specialize cond F c
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h : S ∈ F
c : X.str F ∉ S
cond : Sᶜ ∈ F
⊢ S ∉ F

Tactic:
rw [compl_mem_iff_notMem] at cond

Premises used: Ultrafilter.compl_mem_iff_notMem
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h : S ∈ F
c : X.str F ∉ S
cond : S ∉ F
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
S : Set X.A
h1 : ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
⊢ S ∈ F → X.str F ∈ S

Tactic:
specialize h1 F
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
h1 : S ∈ F → X.str F ∈ S
mpr : ∀ (h : S ∈ F), Sᶜ ∈ F
mpr₁ : ∀ (h : Sᶜ ∈ F), Sᶜ ∈ F
⊢ Sᶜ ∈ F

Tactic:
rcases F.mem_or_compl_mem S with h | h

Premises used: Ultrafilter.mem_or_compl_mem
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
h1 : S ∈ F → X.str F ∈ S
h : S ∈ F
⊢ Sᶜ ∈ F

Tactic:
absurd (h1 h) h2

Premises used: absurd
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
h1 : S ∈ F → X.str F ∈ S
h : Sᶜ ∈ F
⊢ Sᶜ ∈ F

Tactic:
h
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
h1 : S ∈ F → X.str F ∈ S
h : S ∈ F
⊢ Sᶜ ∈ F

Tactic:
exacts [absurd (h1 h) h2, h]

Premises used: absurd
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
isCompact_univ : IsCompact.{u_1} (X := X.A) Set.univ
⊢ CompactSpace.{u_1} X.A

Tactic:
constructor
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
isCompact_univ :
  ∀ (f : Ultrafilter X.A),
    (↑f : Filter X.A) ≤ 𝓟 Set.univ → ∃ (x : X.A), Membership.mem (γ := Set X.A) Set.univ x ∧ (↑f : Filter X.A) ≤ 𝓝 x
⊢ IsCompact.{u_1} (X := X.A) Set.univ

Tactic:
rw [isCompact_iff_ultrafilter_le_nhds]

Premises used: isCompact_iff_ultrafilter_le_nhds
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
F : Ultrafilter X.A
isCompact_univ :
  (↑F : Filter X.A) ≤ 𝓟 Set.univ → ∃ (x : X.A), Membership.mem (γ := Set X.A) Set.univ x ∧ (↑F : Filter X.A) ≤ 𝓝 x
⊢ (↑F : Filter X.A) ≤ 𝓟 Set.univ → ∃ (x : X.A), Membership.mem (γ := Set X.A) Set.univ x ∧ (↑F : Filter X.A) ≤ 𝓝 x

Tactic:
_
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
F : Ultrafilter X.A
h : (↑F : Filter X.A) ≤ 𝓟 Set.univ
⊢ Membership.mem (γ := Set X.A) Set.univ (X.str F)

Tactic:
tauto
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
F : Ultrafilter X.A
h : (↑F : Filter X.A) ≤ 𝓟 Set.univ
isCompact_univ : (↑F : Filter X.A) ≤ 𝓝 (X.str F)
⊢ ∃ (x : X.A), Membership.mem (γ := Set X.A) Set.univ x ∧ (↑F : Filter X.A) ≤ 𝓝 x

Tactic:
refine ⟨X.str F, by tauto, ?_⟩
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
F : Ultrafilter X.A
h : (↑F : Filter X.A) ≤ 𝓟 Set.univ
isCompact_univ : ∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ (↑F : Filter X.A)
⊢ (↑F : Filter X.A) ≤ 𝓝 (X.str F)

Tactic:
rw [le_nhds_iff]

Premises used: le_nhds_iff
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
F : Ultrafilter X.A
h : (↑F : Filter X.A) ≤ 𝓟 Set.univ
S : Set X.A
h1 : X.str F ∈ S
h2 : IsOpen S
⊢ S ∈ (↑F : Filter X.A)

Tactic:
h2 F h1
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
F : Ultrafilter X.A
h : (↑F : Filter X.A) ≤ 𝓟 Set.univ
S : Set X.A
h1 : X.str F ∈ S
h2 : IsOpen S
⊢ S ∈ (↑F : Filter X.A)

Tactic:
exact h2 F h1
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A B : Set X.A
h : ∀ (G : Ultrafilter X.A), G ∈ basic (A ∩ B) ↔ G ∈ basic A ∩ basic B
⊢ basic (A ∩ B) = basic A ∩ basic B

Tactic:
ext G
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
h : G ∈ basic (A ∩ B) → G ∈ basic A ∩ basic B
h₁ : G ∈ basic A ∩ basic B → G ∈ basic (A ∩ B)
⊢ G ∈ basic (A ∩ B) ↔ G ∈ basic A ∩ basic B

Tactic:
constructor
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
h : G ∈ basic A
h₁ : G ∈ basic B
⊢ G ∈ basic A ∩ basic B

Tactic:
constructor
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
h : ∀ a ∈ A ∩ B, a ∈ A
⊢ G ∈ basic A

Tactic:
filter_upwards [hG] with _
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
h : ∀ a ∈ A ∩ B, a ∈ B
⊢ G ∈ basic B

Tactic:
filter_upwards [hG] with _
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
a : X.A
⊢ a ∈ A ∩ B → a ∈ A

Tactic:
And.left

Premises used: Set.Mem, setOf, Set.inter, And.left
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
a : X.A
⊢ a ∈ A ∩ B → a ∈ B

Tactic:
And.right

Premises used: Set.Mem, setOf, Set.inter, And.right
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
a : X.A
⊢ a ∈ A ∩ B → a ∈ A

Tactic:
exacts [And.left, And.right]

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
h1 : G ∈ basic A
h2 : G ∈ basic B
⊢ G ∈ basic (A ∩ B)

Tactic:
inter_mem h1 h2

Premises used: _private.0.Compactum.basic, Set.Mem, Filter.inter_mem, setOf
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
h1 : G ∈ basic A
h2 : G ∈ basic B
⊢ G ∈ basic (A ∩ B)

Tactic:
exact inter_mem h1 h2

Premises used: Filter.inter_mem
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
a : X.A
ha : a ∈ A
⊢ X.str (X.incl a) = a

Tactic:
simp
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
Q : Set X.A
hQ : Q ∈ F
R : Set X.A
hR : R ∈ F
h : Q ∩ R ∈ F ∧ X.str ⁻¹' (Q ∩ R) = X.str ⁻¹' Q ∩ X.str ⁻¹' R
⊢ X.str ⁻¹' Q ∩ X.str ⁻¹' R ∈ C0

Tactic:
use Q ∩ R
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
Q : Set X.A
hQ : Q ∈ F
R : Set X.A
hR : R ∈ F
h : Q ∩ R ∈ F
⊢ Q ∩ R ∈ F ∧ X.str ⁻¹' (Q ∩ R) = X.str ⁻¹' Q ∩ X.str ⁻¹' R

Tactic:
simp only [and_true, Set.preimage_inter]

Premises used: Set.preimage_inter, and_true
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
Q : Set X.A
hQ : Q ∈ F
R : Set X.A
hR : R ∈ F
⊢ Q ∩ R ∈ F

Tactic:
inter_sets _ hQ hR

Premises used: Filter.inter_sets
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
Q : Set X.A
hQ : Q ∈ F
R : Set X.A
hR : R ∈ F
⊢ Q ∩ R ∈ F

Tactic:
exact inter_sets _ hQ hR

Premises used: Filter.inter_sets
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
⊢ ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0

Tactic:
have claim1 : ∀ (B) (_ : B ∈ C0) (C) (_ : C ∈ C0), B ∩ C ∈ C0 := by
    rintro B ⟨Q, hQ, rfl⟩ C ⟨R, hR, rfl⟩
    use Q ∩ R
    simp only [and_true, Set.preimage_inter]
    exact inter_sets _ hQ hR
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
Q : Set X.A
hQ : Q ∈ F
obtain : ∀ q ∈ Q, (X.str ⁻¹' Q).Nonempty
⊢ (X.str ⁻¹' Q).Nonempty

Tactic:
obtain ⟨q⟩ := Filter.nonempty_of_mem hQ

Premises used: Filter.nonempty_of_mem
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
Q : Set X.A
hQ : Q ∈ F
q : X.A
h_1 : q ∈ Q
h : X.incl q ∈ X.str ⁻¹' Q
⊢ (X.str ⁻¹' Q).Nonempty

Tactic:
use X.incl q

Premises used: Compactum.incl
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
Q : Set X.A
hQ : Q ∈ F
q : X.A
h : q ∈ Q
⊢ X.incl q ∈ X.str ⁻¹' Q

Tactic:
simpa
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
⊢ ∀ B ∈ C0, B.Nonempty

Tactic:
have claim2 : ∀ B ∈ C0, Set.Nonempty B := by
    rintro B ⟨Q, hQ, rfl⟩
    obtain ⟨q⟩ := Filter.nonempty_of_mem hQ
    use X.incl q
    simpa
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
⊢ (Q ∩ cl A).Nonempty

Tactic:
have : (Q ∩ cl A).Nonempty := Filter.nonempty_of_mem (inter_mem hQ hF)
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
this : (Q ∩ cl A).Nonempty
rcases :
  ∀ (q : X.A) (hq1 : q ∈ Q) (P : Ultrafilter X.A) (hq2 : P ∈ basic A) (hq3 : X.str P = q), (AA ∩ X.str ⁻¹' Q).Nonempty
⊢ (AA ∩ X.str ⁻¹' Q).Nonempty

Tactic:
rcases this with ⟨q, hq1, P, hq2, hq3⟩
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
q : X.A
hq1 : q ∈ Q
P : Ultrafilter X.A
hq2 : P ∈ basic A
hq3 : X.str P = q
⊢ (AA ∩ X.str ⁻¹' Q).Nonempty

Tactic:
⟨P, hq2, ?_⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
q : X.A
hq1 : q ∈ Q
P : Ultrafilter X.A
hq2 : P ∈ basic A
hq3 : X.str P = q
refine : P ∈ X.str ⁻¹' Q
⊢ (AA ∩ X.str ⁻¹' Q).Nonempty

Tactic:
refine ⟨P, hq2, ?_⟩
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
q : X.A
hq1 : q ∈ Q
P : Ultrafilter X.A
hq2 : P ∈ basic A
hq3 : X.str P = q
⊢ X.str P ∈ Q

Tactic:
rw [← hq3] at hq1
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
q : X.A
hq1 : q ∈ Q
P : Ultrafilter X.A
hq2 : P ∈ basic A
hq3 : X.str P = q
hq1₁ : X.str P ∈ Q
⊢ P ∈ basic A

Tactic:
rw [← hq3] at hq1
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
q : X.A
hq1 : q ∈ Q
P : Ultrafilter X.A
hq2 : P ∈ basic A
hq3 : X.str P = q
hq1₁ : X.str P ∈ Q
hq2₁ : P ∈ basic A
⊢ X.str P = q

Tactic:
rw [← hq3] at hq1