awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
P : Ultrafilter X.A
hq1 : X.str P ∈ Q
hq2 : P ∈ basic A
hq3 : X.str P = q
⊢ P ∈ 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
claim2 : ∀ B ∈ C0, B.Nonempty
⊢ ∀ B ∈ C0, (AA ∩ B).Nonempty

Tactic:
have claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty := by
    rintro B ⟨Q, hQ, rfl⟩
    have : (Q ∩ cl A).Nonempty := Filter.nonempty_of_mem (inter_mem hQ hF)
    rcases this with ⟨q, hq1, P, hq2, hq3⟩
    refine ⟨P, hq2, ?_⟩
    rw [← hq3] at hq1
    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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
obtain : ∀ (G : Ultrafilter (Ultrafilter X.A)) (h1 : C1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets), X.str F ∈ cl A
⊢ X.str F ∈ cl A

Tactic:
obtain ⟨G, h1⟩ := exists_ultrafilter_of_finite_inter_nonempty _ this

Premises used: Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : C1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
h : X.join G ∈ basic A ∧ X.str (X.join G) = X.str F
⊢ X.str F ∈ cl A

Tactic:
use X.join G

Premises used: Compactum.join
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : C1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
⊢ Ultrafilter.map X.str G = F

Tactic:
have : G.map X.str = F := Ultrafilter.coe_le_coe.1 fun S hS => h1 (Or.inr ⟨S, hS, rfl⟩)
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this_1 : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : C1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
this : Ultrafilter.map X.str G = F
h : X.join G ∈ basic A ∧ X.str F = X.str F
⊢ X.join G ∈ basic A ∧ X.str (X.join G) = X.str F

Tactic:
rw [join_distrib, this]

Premises used: Compactum.join_distrib
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this_1 : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : C1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
this : Ultrafilter.map X.str G = F
⊢ X.join G ∈ basic A ∧ X.str F = X.str F

Tactic:
⟨h1 (Or.inl rfl), rfl⟩

Premises used: And.intro, Or.inl, rfl
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this_1 : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : C1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
this : Ultrafilter.map X.str G = F
⊢ X.join G ∈ basic A ∧ X.str F = X.str F

Tactic:
exact ⟨h1 (Or.inl rfl), rfl⟩
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
suffices : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
⊢ X.str F ∈ cl A

Tactic:
suffices ∀ T : fsu, ι T ⊆ C1 → (⋂₀ ι T).Nonempty by
    obtain ⟨G, h1⟩ := exists_ultrafilter_of_finite_inter_nonempty _ this
    use X.join G
    have : G.map X.str = F := Ultrafilter.coe_le_coe.1 fun S hS => h1 (Or.inr ⟨S, hS, rfl⟩)
    rw [join_distrib, this]
    exact ⟨h1 (Or.inl rfl), rfl⟩
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
⊢ FiniteInter (finiteInterClosure C1)

Tactic:
have claim4 := finiteInterClosure_finiteInter C1
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
⊢ FiniteInter C0

Tactic:
have claim5 : FiniteInter C0 := ⟨⟨_, univ_mem, Set.preimage_univ⟩, claim1⟩
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
P : Set (Ultrafilter X.A)
hP : P ∈ C2
inl : ∀ (h : P ∈ C0), P.Nonempty
inr : ∀ (h : ∃ Q ∈ C0, P = AA ∩ Q), P.Nonempty
⊢ P.Nonempty

Tactic:
rcases this P hP with h | h
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
P : Set (Ultrafilter X.A)
hP : P ∈ C2
h : P ∈ C0
⊢ P.Nonempty

Tactic:
claim2 _ h
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
P : Set (Ultrafilter X.A)
hP : P ∈ C2
h : P ∈ C0
⊢ P.Nonempty

Tactic:
exact claim2 _ h
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
P : Set (Ultrafilter X.A)
hP : P ∈ C2
h : ∃ Q ∈ C0, P = AA ∩ Q
inr : ∀ (Q : Set (Ultrafilter X.A)) (hQ : Q ∈ C0) (hP : AA ∩ Q ∈ C2), (AA ∩ Q).Nonempty
⊢ P.Nonempty

Tactic:
rcases h with ⟨Q, hQ, rfl⟩

Premises used: rfl
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
Q : Set (Ultrafilter X.A)
hQ : Q ∈ C0
hP : AA ∩ Q ∈ C2
⊢ (AA ∩ Q).Nonempty

Tactic:
claim3 _ hQ
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
Q : Set (Ultrafilter X.A)
hQ : Q ∈ C0
hP : AA ∩ Q ∈ C2
⊢ (AA ∩ Q).Nonempty

Tactic:
exact claim3 _ hQ
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
suffices : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
⊢ ∀ P ∈ C2, P.Nonempty

Tactic:
suffices ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q by
      intro P hP
      rcases this P hP with h | h
      · exact claim2 _ h
      · rcases h with ⟨Q, hQ, rfl⟩
        exact claim3 _ hQ
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
P : Set (Ultrafilter X.A)
hP : P ∈ C2
⊢ P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q

Tactic:
claim5.finiteInterClosure_insert _ hP

Premises used: FiniteInter.finiteInterClosure_insert
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
P : Set (Ultrafilter X.A)
hP : P ∈ C2
⊢ P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q

Tactic:
exact claim5.finiteInterClosure_insert _ hP

Premises used: FiniteInter.finiteInterClosure_insert
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
⊢ ∀ P ∈ C2, P.Nonempty

Tactic:
have claim6 : ∀ P ∈ C2, (P : Set (Ultrafilter X)).Nonempty := by
    suffices ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q by
      intro P hP
      rcases this P hP with h | h
      · exact claim2 _ h
      · rcases h with ⟨Q, hQ, rfl⟩
        exact claim3 _ hQ
    intro P hP
    exact claim5.finiteInterClosure_insert _ hP
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
hT : ι T ⊆ C1
this : ⋂₀ ι T ∈ C2
⊢ (⋂₀ ι T).Nonempty

Tactic:
claim6 _ this
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
hT : ι T ⊆ C1
this : ⋂₀ ι T ∈ C2
⊢ (⋂₀ ι T).Nonempty

Tactic:
exact claim6 _ this
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
hT : ι T ⊆ C1
suffices : ⋂₀ ι T ∈ C2
⊢ (⋂₀ ι T).Nonempty

Tactic:
suffices ⋂₀ ι T ∈ C2 by exact claim6 _ this
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
hT : ι T ⊆ C1
apply : (↑T : Set (Set (Ultrafilter X.A))) ⊆ finiteInterClosure C1
⊢ ⋂₀ ι T ∈ C2

Tactic:
apply claim4.finiteInter_mem T

Premises used: FiniteInter.finiteInter_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
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
hT : ι T ⊆ C1
t : Set (Ultrafilter X.A)
ht : t ∈ (↑T : Set (Set (Ultrafilter X.A)))
⊢ t ∈ finiteInterClosure C1

Tactic:
finiteInterClosure.basic (@hT t ht)

Premises used: Set.Mem, FiniteInter.finiteInterClosure.basic
-- 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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
hT : ι T ⊆ C1
t : Set (Ultrafilter X.A)
ht : t ∈ (↑T : Set (Set (Ultrafilter X.A)))
⊢ t ∈ finiteInterClosure C1

Tactic:
exact finiteInterClosure.basic (@hT t ht)

Premises used: FiniteInter.finiteInterClosure.basic
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
rw : ∀ (F : Ultrafilter X.A), cl A ∈ F → X.str F ∈ cl A
⊢ IsClosed (cl A)

Tactic:
rw [isClosed_iff]

Premises used: Compactum.isClosed_iff
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : cl A ∈ F
⊢ X.str F ∈ cl A

Tactic:
cl_cl _ ⟨F, hF, rfl⟩

Premises used: And.intro, Exists.intro, _private.0.Compactum.cl_cl, rfl
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : cl A ∈ F
⊢ X.str F ∈ cl A

Tactic:
exact cl_cl _ ⟨F, hF, rfl⟩

Premises used: And.intro, Exists.intro, _private.0.Compactum.cl_cl, rfl
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
F : Ultrafilter X.A
x : X.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)))
T0 : ssu := {S : Set (Ultrafilter X.A) | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : (↑F : Filter X.A) ≤ 𝓝 x
A : Set X.A
hA : IsClosed A
h : A ∈ F
by_contra : ∀ (H : x ∉ A), False
⊢ x ∈ A

Tactic:
by_contra H