awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
x_1 : Ultrafilter X.A
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  Membership.mem (γ := Set (Ultrafilter X.A)) (basic Set.univ) x_1 →
    Membership.mem (γ := Set (Ultrafilter X.A)) Set.univ x_1
⊢ Membership.mem (γ := Set (Ultrafilter X.A)) (basic Set.univ) x_1 →
    Membership.mem (γ := Set (Ultrafilter X.A)) Set.univ x_1

Tactic:
tauto
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
x_1 : Ultrafilter X.A
h :
  Membership.mem (γ := Set (Ultrafilter X.A)) Set.univ x_1 →
    Membership.mem (γ := Set (Ultrafilter X.A)) (basic Set.univ) x_1
⊢ Membership.mem (γ := Set (Ultrafilter X.A)) Set.univ x_1 ↔
    Membership.mem (γ := Set (Ultrafilter X.A)) (basic Set.univ) x_1

Tactic:
refine ⟨?_, by tauto⟩
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
x_1 : Ultrafilter X.A
h : Membership.mem (γ := Set (Ultrafilter X.A)) Set.univ x_1
⊢ Membership.mem (γ := Set (Ultrafilter X.A)) (basic Set.univ) x_1

Tactic:
apply Filter.univ_sets

Premises used: Filter.univ_sets
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ ∀ ⦃s : Set (Ultrafilter X.A)⦄, s ∈ T0 → ∀ ⦃t : Set (Ultrafilter X.A)⦄, t ∈ T0 → s ∩ t ∈ T0

Tactic:
claim3
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ ∀ ⦃s : Set (Ultrafilter X.A)⦄, s ∈ T0 → ∀ ⦃t : Set (Ultrafilter X.A)⦄, t ∈ T0 → s ∩ t ∈ T0

Tactic:
exact claim3
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ S ∈ finiteInterClosure (insert AA T0)

Tactic:
hS

Premises used: Set.Mem
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ S ∈ finiteInterClosure (insert AA T0)

Tactic:
exact hS
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
⊢ ∀ S ∈ T2, S.Nonempty

Tactic:
have claim6 : ∀ S ∈ T2, Set.Nonempty S := by
    suffices ∀ S ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q by
      intro S hS
      rcases this _ hS with h | h
      · exact claim5 S h
      · rcases h with ⟨Q, hQ, rfl⟩
        exact claim4 Q hQ
    intro S hS
    apply finiteInterClosure_insert
    · constructor
      · use Set.univ
        refine ⟨Filter.univ_sets _, ?_⟩
        ext
        refine ⟨?_, by tauto⟩
        · intro
          apply Filter.univ_sets
      · exact claim3
    · exact hS
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
obtain : ∀ (G : Ultrafilter (Ultrafilter X.A)) (h1 : T1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets), X.str F = x
⊢ X.str F = x

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

Premises used: Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
⊢ X.join G = F

Tactic:
have c1 : X.join G = F := Ultrafilter.coe_le_coe.1 fun P hP => h1 (Or.inr ⟨P, hP, 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
c1 : X.join G = F
⊢ Ultrafilter.map X.str G = X.incl x

Tactic:
Ultrafilter.coe_le_coe.1 fun P hP => ?_

Premises used: Ultrafilter.coe_le_coe, Iff.mp
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
c1 : X.join G = F
refine : ∀ (P : Set X.A) (hP : P ∈ (↑(X.incl x) : Filter X.A)), P ∈ (↑(Ultrafilter.map X.str G) : Filter X.A)
⊢ Ultrafilter.map X.str G = X.incl x

Tactic:
refine Ultrafilter.coe_le_coe.1 fun P hP => ?_

Premises used: Ultrafilter.coe_le_coe, Iff.mp
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
c1 : X.join G = F
P : Set X.A
hP : P ∈ (↑(X.incl x) : Filter X.A)
apply : AA ⊆ X.str ⁻¹' P
⊢ P ∈ (↑(Ultrafilter.map X.str G) : Filter X.A)

Tactic:
apply mem_of_superset (h1 (Or.inl rfl))

Premises used: Or.inl, rfl, Filter.mem_of_superset
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
F : Ultrafilter 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}
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim5 : ∀ S ∈ T0, S.Nonempty
G : Ultrafilter (Ultrafilter X.A)
c1 : X.join G = F
P : Set X.A
x : Ultrafilter X.A
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {X.str x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : (↑F : Filter X.A) ≤ 𝓝 (X.str x)
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → X.str x ∈ A
claim2 : ∀ A ∈ F, X.str x ∈ cl A
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
h1 : T1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
hP : P ∈ (↑(X.incl (X.str x)) : Filter X.A)
⊢ x ∈ X.str ⁻¹' P

Tactic:
hP

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
F : Ultrafilter 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}
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim5 : ∀ S ∈ T0, S.Nonempty
G : Ultrafilter (Ultrafilter X.A)
c1 : X.join G = F
P : Set X.A
x : Ultrafilter X.A
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {X.str x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : (↑F : Filter X.A) ≤ 𝓝 (X.str x)
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → X.str x ∈ A
claim2 : ∀ A ∈ F, X.str x ∈ cl A
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
h1 : T1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
hP : P ∈ (↑(X.incl (X.str x)) : Filter X.A)
⊢ x ∈ X.str ⁻¹' P

Tactic:
exact hP
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
c1 : X.join G = F
⊢ Ultrafilter.map X.str G = X.incl x

Tactic:
have c2 : G.map X.str = X.incl x := by
      refine Ultrafilter.coe_le_coe.1 fun P hP => ?_
      apply mem_of_superset (h1 (Or.inl rfl))
      rintro x ⟨rfl⟩
      exact hP
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
c1 : X.join G = F
c2 : Ultrafilter.map X.str G = X.incl x
⊢ X.str F = x

Tactic:
simp [← c1, c2]
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
suffices : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
⊢ X.str F = x

Tactic:
suffices ∀ F : fsu, ↑F ⊆ T1 → (⋂₀ ι F).Nonempty by
    obtain ⟨G, h1⟩ := Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty _ this
    have c1 : X.join G = F := Ultrafilter.coe_le_coe.1 fun P hP => h1 (Or.inr ⟨P, hP, rfl⟩)
    have c2 : G.map X.str = X.incl x := by
      refine Ultrafilter.coe_le_coe.1 fun P hP => ?_
      apply mem_of_superset (h1 (Or.inl rfl))
      rintro x ⟨rfl⟩
      exact hP
    simp [← c1, c2]
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
T : fsu
hT : (↑T : Set (Set (Ultrafilter X.A))) ⊆ T1
⊢ (⋂₀ ι T).Nonempty

Tactic:
claim6 _ (finiteInter_mem (.finiteInterClosure_finiteInter _) _ ?_)

Premises used: FiniteInter.finiteInterClosure_finiteInter, FiniteInter.finiteInter_mem
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
T : fsu
hT : (↑T : Set (Set (Ultrafilter X.A))) ⊆ T1
refine : (↑T : Set (Set (Ultrafilter X.A))) ⊆ finiteInterClosure T1
⊢ (⋂₀ ι T).Nonempty

Tactic:
refine claim6 _ (finiteInter_mem (.finiteInterClosure_finiteInter _) _ ?_)

Premises used: FiniteInter.finiteInterClosure_finiteInter, FiniteInter.finiteInter_mem
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
T : fsu
hT : (↑T : Set (Set (Ultrafilter X.A))) ⊆ T1
t : Set (Ultrafilter X.A)
ht : t ∈ (↑T : Set (Set (Ultrafilter X.A)))
⊢ t ∈ finiteInterClosure T1

Tactic:
finiteInterClosure.basic (@hT t ht)

Premises used: Set.Mem, FiniteInter.finiteInterClosure.basic
-- 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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
T : fsu
hT : (↑T : Set (Set (Ultrafilter X.A))) ⊆ T1
t : Set (Ultrafilter X.A)
ht : t ∈ (↑T : Set (Set (Ultrafilter X.A)))
⊢ t ∈ finiteInterClosure T1

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

Premises used: FiniteInter.finiteInterClosure.basic
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
F : Ultrafilter X.A
x : X.A
h : X.str F = x
s : Set X.A
hx : x ∈ s
hs : IsOpen s
rwa rwa₁ rwa₂ rwa₃ : x ∈ s
⊢ X.str F ∈ s

Tactic:
rwa [h]
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
rw : ∀ {x y : X.A} (f : Ultrafilter X.A), (↑f : Filter X.A) ≤ 𝓝 x → (↑f : Filter X.A) ≤ 𝓝 y → x = y
⊢ T2Space.{u_1} X.A

Tactic:
rw [t2_iff_ultrafilter]

Premises used: t2_iff_ultrafilter
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
x : X.A
_ : ∀ {y : X.A} (f : Ultrafilter X.A), (↑f : Filter X.A) ≤ 𝓝 x → (↑f : Filter X.A) ≤ 𝓝 y → x = y
⊢ ∀ {y : X.A} (f : Ultrafilter X.A), (↑f : Filter X.A) ≤ 𝓝 x → (↑f : Filter X.A) ≤ 𝓝 y → x = y

Tactic:
_
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
x y : X.A
F : Ultrafilter X.A
hx : (↑F : Filter X.A) ≤ 𝓝 x
hy : (↑F : Filter X.A) ≤ 𝓝 y
rw : X.str F = y
rw₁ rw₂ : X.str F = X.str F
⊢ x = y

Tactic:
rw [← str_eq_of_le_nhds _ _ hx, ← str_eq_of_le_nhds _ _ hy]

Premises used: Compactum.str_eq_of_le_nhds
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
F : Ultrafilter X.A
rw : ∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ (↑F : Filter X.A)
⊢ F.lim = X.str F

Tactic:
rw [Ultrafilter.lim_eq_iff_le_nhds, le_nhds_iff]

Premises used: le_nhds_iff, Ultrafilter.lim_eq_iff_le_nhds
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
F : Ultrafilter X.A
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  ∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ (↑F : Filter X.A)
⊢ ∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ (↑F : Filter X.A)

Tactic:
tauto
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
h : ∀ (x : X.A), x ∈ cl A ↔ x ∈ closure A
⊢ cl A = closure A

Tactic:
ext
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
x : X.A
h : x ∈ cl A ↔ ∃ (u : Ultrafilter X.A), A ∈ u ∧ (↑u : Filter X.A) ≤ 𝓝 x
⊢ x ∈ cl A ↔ x ∈ closure A

Tactic:
rw [mem_closure_iff_ultrafilter]

Premises used: mem_closure_iff_ultrafilter
-- Module: Mathlib.Topology.Category.Compactum
Goal:
X : Compactum
A : Set X.A
x : X.A
h : x ∈ cl A → ∃ (u : Ultrafilter X.A), A ∈ u ∧ (↑u : Filter X.A) ≤ 𝓝 x
h₁ : (∃ (u : Ultrafilter X.A), A ∈ u ∧ (↑u : Filter X.A) ≤ 𝓝 x) → x ∈ cl A
⊢ x ∈ cl A ↔ ∃ (u : Ultrafilter X.A), A ∈ u ∧ (↑u : Filter X.A) ≤ 𝓝 x

Tactic:
constructor