α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ↑(joinM u) ≤ ↑x
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ x = joinM u
rw [eq_comm, ← Ultrafilter.coe_le_coe]
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ↑(joinM u) ≤ ↑x
change ↑u ≤ 𝓝 x ↔ ∀ s ∈ x, { v : Ultrafilter α | s ∈ v } ∈ u
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u) ↔
    ∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u
simp only [TopologicalSpace.nhds_generateFrom, le_iInf_iff, ultrafilterBasis, le_principal_iff,
  mem_setOf_eq]
case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u) →
    ∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u

case mpr
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u) →
    ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u) ↔
    ∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u
constructor
case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u
a : Set α
ha : a ∈ x
⊢ {v | a ∈ v} ∈ u
case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u) →
    ∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u
intro h a ha
no goals
case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u
a : Set α
ha : a ∈ x
⊢ {v | a ∈ v} ∈ u
exact h _ ⟨ha, a, rfl⟩
case mpr.intro.intro
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u
a : Set α
xi : x ∈ (fun s => {u | s ∈ u}) a
⊢ (fun s => {u | s ∈ u}) a ∈ ↑u
case mpr
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u) →
    ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u
rintro h a ⟨xi, a, rfl⟩
no goals
case mpr.intro.intro
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u
a : Set α
xi : x ∈ (fun s => {u | s ∈ u}) a
⊢ (fun s => {u | s ∈ u}) a ∈ ↑u
exact h _ xi