-- Mathlib/Topology/Category/Compactum.lean
theorem str_eq_of_le_nhds {X : Compactum} (F : Ultrafilter X) (x : X) : ↑F ≤ 𝓝 x → X.str F = x

Proof state:
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 => ↑x
T0 : ssu := {S | ∃ A ∈ F, S = Compactum.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 ≤ 𝓝 x
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : x ∉ A
⊢ False

Tactic:
rw [le_nhds_iff] at cond

Result:
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 => ↑x
T0 : ssu := {S | ∃ A ∈ F, S = Compactum.basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ∀ (s : Set X.A), x ∈ s → IsOpen s → s ∈ ↑F
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : x ∉ A
⊢ False

Proof state:
case refl
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 => ↑x
T0 : ssu := {S | ∃ A ∈ F, S = Compactum.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 ≤ 𝓝 (X.str x)
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → X.str x ∈ A
claim2 : ∀ A ∈ F, X.str x ∈ Compactum.cl A
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), ↑F ⊆ T1 → (⋂₀ ι F).Nonempty
h1 : T1 ⊆ (↑G).sets
hP : P ∈ ↑(X.incl (X.str x))
⊢ x ∈ X.str ⁻¹' P

Tactic:
exact hP

Result:
no goals

Proof state:
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 => ↑x
T0 : ssu := {S | ∃ A ∈ F, S = Compactum.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 ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ Compactum.cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
this : ∀ S ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q
⊢ ∀ S ∈ T2, S.Nonempty

Tactic:
intro S hS

Result:
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 => ↑x
T0 : ssu := {S | ∃ A ∈ F, S = Compactum.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 ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ Compactum.cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
this : ∀ S ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ S.Nonempty

Proof state:
case intro
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 => ↑x
T0 : ssu := {S | ∃ A ∈ F, S = Compactum.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 ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ Compactum.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 ⊆ T1 → (⋂₀ ι F).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ (↑G).sets
c1 : X.join G = F
⊢ X.str F = 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

Result:
case intro
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 => ↑x
T0 : ssu := {S | ∃ A ∈ F, S = Compactum.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 ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ Compactum.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 ⊆ T1 → (⋂₀ ι F).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ (↑G).sets
c1 : X.join G = F
c2 : Ultrafilter.map X.str G = X.incl x
⊢ X.str F = x

Proof state:
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 => ↑x
T0 : ssu := {S | ∃ A ∈ F, S = Compactum.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 ≤ 𝓝 x
⊢ ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A

Tactic:
intro A hA h

Result:
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 => ↑x
T0 : ssu := {S | ∃ A ∈ F, S = Compactum.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 ≤ 𝓝 x
A : Set X.A
hA : IsClosed A
h : A ∈ F
⊢ x ∈ A

Proof state:
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
⊢ ↑F ≤ 𝓝 x → X.str F = x

Tactic:
let ssu := Set (Set (Ultrafilter X))

Result:
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))
⊢ ↑F ≤ 𝓝 x → X.str F = x

Proof state:
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 => ↑x
T0 : ssu := {S | ∃ A ∈ F, S = Compactum.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 ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ Compactum.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 ⊆ T1
⊢ (⋂₀ ι T).Nonempty

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

Result:
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 => ↑x
T0 : ssu := {S | ∃ A ∈ F, S = Compactum.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 ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ Compactum.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 ⊆ T1
⊢ ↑T ⊆ finiteInterClosure T1