-- Mathlib/Topology/Category/Compactum.lean
theorem cl_cl {X : Compactum} (A : Set X) : cl (cl A) ⊆ cl A

Proof state:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ Compactum.basic (Compactum.cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | 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:
rintro B ⟨Q, hQ, rfl⟩

Result:
case intro.intro
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ Compactum.basic (Compactum.cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | 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
⊢ (X.str ⁻¹' Q).Nonempty

Proof state:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ Compactum.basic (Compactum.cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | 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

Result:
no goals

Proof state:
case intro.intro
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ Compactum.basic (Compactum.cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | 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), ι T ⊆ C1 → (⋂₀ ι T).Nonempty

Tactic:
intro T hT

Result:
case intro.intro
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ Compactum.basic (Compactum.cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | 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).Nonempty

Proof state:
case intro.intro
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ Compactum.basic (Compactum.cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | 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 ⊆ finiteInterClosure C1

Tactic:
intro t ht

Result:
case intro.intro
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ Compactum.basic (Compactum.cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | 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
⊢ t ∈ finiteInterClosure C1

Proof state:
case intro.intro
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ Compactum.basic (Compactum.cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
⊢ X.str F ∈ Compactum.cl A

Tactic:
let C2 := finiteInterClosure C1

Result:
case intro.intro
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ Compactum.basic (Compactum.cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
⊢ X.str F ∈ Compactum.cl A

Proof state:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ Compactum.basic (Compactum.cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | 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:
rintro B ⟨Q, hQ, rfl⟩

Result:
case intro.intro
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ Compactum.basic (Compactum.cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | 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
⊢ (AA ∩ X.str ⁻¹' Q).Nonempty

Proof state:
case h
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ Compactum.basic (Compactum.cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x => ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | 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).sets
this : Ultrafilter.map X.str G = F
⊢ X.join G ∈ Compactum.basic A ∧ X.str F = X.str F

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

Result:
no goals