[GOAL]
α : Type u
⊢ ∀ (t₁ : Set (Ultrafilter α)),
    t₁ ∈ ultrafilterBasis α →
      ∀ (t₂ : Set (Ultrafilter α)),
        t₂ ∈ ultrafilterBasis α →
          ∀ (x : Ultrafilter α), x ∈ t₁ ∩ t₂ → ∃ t₃, t₃ ∈ ultrafilterBasis α ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
[PROOFSTEP]
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ u ⟨ua, ub⟩
[GOAL]
case intro.intro.intro
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
⊢ ∃ t₃, t₃ ∈ ultrafilterBasis α ∧ u ∈ t₃ ∧ t₃ ⊆ (fun s => {u | s ∈ u}) a ∩ (fun s => {u | s ∈ u}) b
[PROOFSTEP]
refine' ⟨_, ⟨a ∩ b, rfl⟩, inter_mem ua ub, fun v hv => ⟨_, _⟩⟩
[GOAL]
case intro.intro.intro.refine'_1
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s => {u | s ∈ u}) (a ∩ b)
⊢ v ∈ (fun s => {u | s ∈ u}) a
[PROOFSTEP]
apply mem_of_superset hv
[GOAL]
case intro.intro.intro.refine'_2
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s => {u | s ∈ u}) (a ∩ b)
⊢ v ∈ (fun s => {u | s ∈ u}) b
[PROOFSTEP]
apply mem_of_superset hv
[GOAL]
case intro.intro.intro.refine'_1
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s => {u | s ∈ u}) (a ∩ b)
⊢ a ∩ b ⊆ a
[PROOFSTEP]
simp [inter_subset_right a b]
[GOAL]
case intro.intro.intro.refine'_2
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s => {u | s ∈ u}) (a ∩ b)
⊢ a ∩ b ⊆ b
[PROOFSTEP]
simp [inter_subset_right a b]
[GOAL]
α : Type u
s : Set α
⊢ IsClosed {u | s ∈ u}
[PROOFSTEP]
rw [← isOpen_compl_iff]
[GOAL]
α : Type u
s : Set α
⊢ IsOpen {u | s ∈ u}ᶜ
[PROOFSTEP]
convert ultrafilter_isOpen_basic sᶜ using 1
[GOAL]
case h.e'_3
α : Type u
s : Set α
⊢ {u | s ∈ u}ᶜ = {u | sᶜ ∈ u}
[PROOFSTEP]
ext u
[GOAL]
case h.e'_3.h
α : Type u
s : Set α
u : Ultrafilter α
⊢ u ∈ {u | s ∈ u}ᶜ ↔ u ∈ {u | sᶜ ∈ u}
[PROOFSTEP]
exact Ultrafilter.compl_mem_iff_not_mem.symm
[GOAL]
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ x = joinM u
[PROOFSTEP]
rw [eq_comm, ← Ultrafilter.coe_le_coe]
[GOAL]
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ↑(joinM u) ≤ ↑x
[PROOFSTEP]
change ↑u ≤ 𝓝 x ↔ ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
[GOAL]
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u
[PROOFSTEP]
simp only [TopologicalSpace.nhds_generateFrom, le_iInf_iff, ultrafilterBasis, le_principal_iff, mem_setOf_eq]
[GOAL]
α : 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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
intro h a ha
[GOAL]
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
[PROOFSTEP]
exact h _ ⟨ha, a, rfl⟩
[GOAL]
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
[PROOFSTEP]
rintro h a ⟨xi, a, rfl⟩
[GOAL]
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
[PROOFSTEP]
exact h _ xi
[GOAL]
α : Type u
⊢ TotallyDisconnectedSpace (Ultrafilter α)
[PROOFSTEP]
rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]
[GOAL]
α : Type u
⊢ ∀ (x : Ultrafilter α), connectedComponent x = {x}
[PROOFSTEP]
intro A
[GOAL]
α : Type u
A : Ultrafilter α
⊢ connectedComponent A = {A}
[PROOFSTEP]
simp only [Set.eq_singleton_iff_unique_mem, mem_connectedComponent, true_and_iff]
[GOAL]
α : Type u
A : Ultrafilter α
⊢ ∀ (x : Ultrafilter α), x ∈ connectedComponent A → x = A
[PROOFSTEP]
intro B hB
[GOAL]
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
⊢ B = A
[PROOFSTEP]
rw [← Ultrafilter.coe_le_coe]
[GOAL]
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
⊢ ↑B ≤ ↑A
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
s : Set α
hs : s ∈ ↑A
⊢ s ∈ ↑B
[PROOFSTEP]
rw [connectedComponent_eq_iInter_clopen, Set.mem_iInter] at hB 
[GOAL]
α : Type u
A B : Ultrafilter α
hB : ∀ (i : { Z // IsClopen Z ∧ A ∈ Z }), B ∈ ↑i
s : Set α
hs : s ∈ ↑A
⊢ s ∈ ↑B
[PROOFSTEP]
let Z := {F : Ultrafilter α | s ∈ F}
[GOAL]
α : Type u
A B : Ultrafilter α
hB : ∀ (i : { Z // IsClopen Z ∧ A ∈ Z }), B ∈ ↑i
s : Set α
hs : s ∈ ↑A
Z : Set (Ultrafilter α) := {F | s ∈ F}
⊢ s ∈ ↑B
[PROOFSTEP]
have hZ : IsClopen Z := ⟨ultrafilter_isOpen_basic s, ultrafilter_isClosed_basic s⟩
[GOAL]
α : Type u
A B : Ultrafilter α
hB : ∀ (i : { Z // IsClopen Z ∧ A ∈ Z }), B ∈ ↑i
s : Set α
hs : s ∈ ↑A
Z : Set (Ultrafilter α) := {F | s ∈ F}
hZ : IsClopen Z
⊢ s ∈ ↑B
[PROOFSTEP]
exact hB ⟨Z, hZ, hs⟩
[GOAL]
α : Type u
b : Ultrafilter α
⊢ Tendsto pure (↑b) (𝓝 b)
[PROOFSTEP]
rw [Tendsto, ← coe_map, ultrafilter_converges_iff]
[GOAL]
α : Type u
b : Ultrafilter α
⊢ b = joinM (map pure b)
[PROOFSTEP]
ext s
[GOAL]
case h
α : Type u
b : Ultrafilter α
s : Set α
⊢ s ∈ b ↔ s ∈ joinM (map pure b)
[PROOFSTEP]
change s ∈ b ↔ {t | s ∈ t} ∈ map pure b
[GOAL]
case h
α : Type u
b : Ultrafilter α
s : Set α
⊢ s ∈ b ↔ {t | s ∈ t} ∈ map pure b
[PROOFSTEP]
simp_rw [mem_map, preimage_setOf_eq, mem_pure, setOf_mem_eq]
[GOAL]
α : Type u
b : Ultrafilter α
⊢ comap pure (𝓝 b) ≤ ↑b
[PROOFSTEP]
rw [TopologicalSpace.nhds_generateFrom]
[GOAL]
α : Type u
b : Ultrafilter α
⊢ comap pure (⨅ (s : Set (Ultrafilter α)) (_ : s ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 s) ≤ ↑b
[PROOFSTEP]
simp only [comap_iInf, comap_principal]
[GOAL]
α : Type u
b : Ultrafilter α
⊢ ⨅ (i : Set (Ultrafilter α)) (_ : i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' i) ≤ ↑b
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ s ∈ ⨅ (i : Set (Ultrafilter α)) (_ : i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' i)
[PROOFSTEP]
rw [← le_principal_iff]
[GOAL]
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ ⨅ (i : Set (Ultrafilter α)) (_ : i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' i) ≤ 𝓟 s
[PROOFSTEP]
refine' iInf_le_of_le {u | s ∈ u} _
[GOAL]
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ ⨅ (_ : {u | s ∈ u} ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s
[PROOFSTEP]
refine' iInf_le_of_le ⟨hs, ⟨s, rfl⟩⟩ _
[GOAL]
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ 𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s
[PROOFSTEP]
exact principal_mono.2 fun a => id
[GOAL]
α : Type u
⊢ Function.Injective pure
[PROOFSTEP]
intro x y h
[GOAL]
α : Type u
x y : α
h : pure x = pure y
⊢ x = y
[PROOFSTEP]
have : { x } ∈ (pure x : Ultrafilter α) := singleton_mem_pure
[GOAL]
α : Type u
x y : α
h : pure x = pure y
this : {x} ∈ pure x
⊢ x = y
[PROOFSTEP]
rw [h] at this 
[GOAL]
α : Type u
x y : α
h : pure x = pure y
this : {x} ∈ pure y
⊢ x = y
[PROOFSTEP]
exact (mem_singleton_iff.mp (mem_pure.mp this)).symm
[GOAL]
α : Type u
⊢ induced pure Ultrafilter.topologicalSpace = ⊥
[PROOFSTEP]
apply eq_bot_of_singletons_open
[GOAL]
case h
α : Type u
⊢ ∀ (x : α), IsOpen {x}
[PROOFSTEP]
intro x
[GOAL]
case h
α : Type u
x : α
⊢ IsOpen {x}
[PROOFSTEP]
use{u : Ultrafilter α | { x } ∈ u}, ultrafilter_isOpen_basic _
[GOAL]
case right
α : Type u
x : α
⊢ pure ⁻¹' {u | {x} ∈ u} = {x}
[PROOFSTEP]
simp
[GOAL]
α : Type u
γ : Type u_1
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
⊢ Ultrafilter.extend f ∘ pure = f
[PROOFSTEP]
letI : TopologicalSpace α := ⊥
[GOAL]
α : Type u
γ : Type u_1
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
this : TopologicalSpace α := ⊥
⊢ Ultrafilter.extend f ∘ pure = f
[PROOFSTEP]
haveI : DiscreteTopology α := ⟨rfl⟩
[GOAL]
α : Type u
γ : Type u_1
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
this✝ : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ Ultrafilter.extend f ∘ pure = f
[PROOFSTEP]
exact funext (denseInducing_pure.extend_eq continuous_of_discreteTopology)
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
⊢ Continuous (Ultrafilter.extend f)
[PROOFSTEP]
have h : ∀ b : Ultrafilter α, ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c) :=
  fun b =>
    -- b.map f is an ultrafilter on γ, which is compact, so it converges to some c in γ.
  let ⟨c, _, h'⟩ := isCompact_univ.ultrafilter_le_nhds (b.map f) (by rw [le_principal_iff]; exact univ_mem)
  ⟨c, le_trans (map_mono (ultrafilter_comap_pure_nhds _)) h'⟩
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ ↑(Ultrafilter.map f b) ≤ 𝓟 univ
[PROOFSTEP]
rw [le_principal_iff]
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ univ ∈ ↑(Ultrafilter.map f b)
[PROOFSTEP]
exact univ_mem
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
⊢ Continuous (Ultrafilter.extend f)
[PROOFSTEP]
letI : TopologicalSpace α := ⊥
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
this : TopologicalSpace α := ⊥
⊢ Continuous (Ultrafilter.extend f)
[PROOFSTEP]
haveI : NormalSpace γ := normalOfCompactT2
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
this✝ : TopologicalSpace α := ⊥
this : NormalSpace γ
⊢ Continuous (Ultrafilter.extend f)
[PROOFSTEP]
exact denseInducing_pure.continuous_extend h
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 c
[PROOFSTEP]
let b' : Ultrafilter (Ultrafilter α) := b.map pure
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 c
[PROOFSTEP]
have t : ↑b' ≤ 𝓝 b := ultrafilter_converges_iff.mpr (bind_pure _).symm
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 c
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 (Ultrafilter.extend f b)
[PROOFSTEP]
have := (continuous_ultrafilter_extend f).tendsto b
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 (Ultrafilter.extend f b)
[PROOFSTEP]
refine' le_trans _ (le_trans (map_mono t) this)
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ map (Ultrafilter.extend f) ↑b'
[PROOFSTEP]
change _ ≤ map (Ultrafilter.extend f ∘ pure) ↑b
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ map (Ultrafilter.extend f ∘ pure) ↑b
[PROOFSTEP]
rw [ultrafilter_extend_extends]
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ map f ↑b
[PROOFSTEP]
exact le_rfl
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
⊢ TopologicalSpace (StoneCech α)
[PROOFSTEP]
unfold StoneCech
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
⊢ TopologicalSpace (Quotient (stoneCechSetoid α))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Inhabited α
⊢ Inhabited (StoneCech α)
[PROOFSTEP]
unfold StoneCech
[GOAL]
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Inhabited α
⊢ Inhabited (Quotient (stoneCechSetoid α))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
inst✝⁵ : TopologicalSpace α
γ : Type u
inst✝⁴ : TopologicalSpace γ
inst✝³ : T2Space γ
inst✝² : CompactSpace γ
γ' : Type u
inst✝¹ : TopologicalSpace γ'
inst✝ : T2Space γ'
f : α → γ
hf : Continuous f
g₁ g₂ : StoneCech α → γ'
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
⊢ g₁ = g₂
[PROOFSTEP]
apply Continuous.ext_on denseRange_stoneCechUnit h₁ h₂
[GOAL]
α : Type u
inst✝⁵ : TopologicalSpace α
γ : Type u
inst✝⁴ : TopologicalSpace γ
inst✝³ : T2Space γ
inst✝² : CompactSpace γ
γ' : Type u
inst✝¹ : TopologicalSpace γ'
inst✝ : T2Space γ'
f : α → γ
hf : Continuous f
g₁ g₂ : StoneCech α → γ'
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
⊢ EqOn g₁ g₂ (range stoneCechUnit)
[PROOFSTEP]
rintro x ⟨x, rfl⟩
[GOAL]
case intro
α : Type u
inst✝⁵ : TopologicalSpace α
γ : Type u
inst✝⁴ : TopologicalSpace γ
inst✝³ : T2Space γ
inst✝² : CompactSpace γ
γ' : Type u
inst✝¹ : TopologicalSpace γ'
inst✝ : T2Space γ'
f : α → γ
hf : Continuous f
g₁ g₂ : StoneCech α → γ'
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
x : α
⊢ g₁ (stoneCechUnit x) = g₂ (stoneCechUnit x)
[PROOFSTEP]
apply congr_fun h x
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = Ultrafilter.extend f (pure x)
[PROOFSTEP]
skip
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = Ultrafilter.extend f (pure x)
[PROOFSTEP]
trans f x
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ f x = Ultrafilter.extend f (pure x)
[PROOFSTEP]
swap
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ f x = Ultrafilter.extend f (pure x)
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x
[PROOFSTEP]
symm
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f (pure x) = f x
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x
[PROOFSTEP]
all_goals refine' ultrafilter_extend_eq_iff.mpr (le_trans (map_mono _) (hf.tendsto _))
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f (pure x) = f x
[PROOFSTEP]
refine' ultrafilter_extend_eq_iff.mpr (le_trans (map_mono _) (hf.tendsto _))
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x
[PROOFSTEP]
refine' ultrafilter_extend_eq_iff.mpr (le_trans (map_mono _) (hf.tendsto _))
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ ↑(pure x) ≤ 𝓝 x
[PROOFSTEP]
apply pure_le_nhds
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ ↑u ≤ 𝓝 x
[PROOFSTEP]
exact ux
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ Tendsto stoneCechUnit (↑g) (𝓝 (stoneCechUnit x))
[PROOFSTEP]
have : (g.map pure).toFilter ≤ 𝓝 g := by
  rw [ultrafilter_converges_iff]
  exact (bind_pure _).symm
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ ↑(Ultrafilter.map pure g) ≤ 𝓝 g
[PROOFSTEP]
rw [ultrafilter_converges_iff]
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ g = joinM (Ultrafilter.map pure g)
[PROOFSTEP]
exact (bind_pure _).symm
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
⊢ Tendsto stoneCechUnit (↑g) (𝓝 (stoneCechUnit x))
[PROOFSTEP]
have : (g.map stoneCechUnit : Filter (StoneCech α)) ≤ 𝓝 ⟦g⟧ :=
  continuousAt_iff_ultrafilter.mp (continuous_quotient_mk'.tendsto g) _ this
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this✝ : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
this : ↑(Ultrafilter.map stoneCechUnit g) ≤ 𝓝 (Quotient.mk (stoneCechSetoid α) g)
⊢ Tendsto stoneCechUnit (↑g) (𝓝 (stoneCechUnit x))
[PROOFSTEP]
rwa [show ⟦g⟧ = ⟦pure x⟧ from Quotient.sound <| convergent_eqv_pure gx] at this 
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
⊢ T2Space (StoneCech α)
[PROOFSTEP]
rw [t2_iff_ultrafilter]
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
⊢ ∀ {x y : StoneCech α} (f : Ultrafilter (StoneCech α)), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y
[PROOFSTEP]
rintro ⟨x⟩ ⟨y⟩ g gx gy
[GOAL]
case mk.mk
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
⊢ Quot.mk Setoid.r x = Quot.mk Setoid.r y
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case mk.mk.a
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
⊢ x ≈ y
[PROOFSTEP]
intro γ tγ h₁ h₂ f hf
[GOAL]
case mk.mk.a
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f x = Ultrafilter.extend f y
[PROOFSTEP]
skip
[GOAL]
case mk.mk.a
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f x = Ultrafilter.extend f y
[PROOFSTEP]
let ff := stoneCechExtend hf
[GOAL]
case mk.mk.a
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
ff : StoneCech α → γ := stoneCechExtend hf
⊢ Ultrafilter.extend f x = Ultrafilter.extend f y
[PROOFSTEP]
change ff ⟦x⟧ = ff ⟦y⟧
[GOAL]
case mk.mk.a
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
ff : StoneCech α → γ := stoneCechExtend hf
⊢ ff (Quotient.mk (stoneCechSetoid α) x) = ff (Quotient.mk (stoneCechSetoid α) y)
[PROOFSTEP]
have lim := fun (z : Ultrafilter α) (gz : (g : Filter (StoneCech α)) ≤ 𝓝 ⟦z⟧) =>
  ((continuous_stoneCechExtend hf).tendsto _).mono_left gz
[GOAL]
case mk.mk.a
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
ff : StoneCech α → γ := stoneCechExtend hf
lim :
  ∀ (z : Ultrafilter α),
    ↑g ≤ 𝓝 (Quotient.mk (stoneCechSetoid α) z) →
      Tendsto (stoneCechExtend hf) (↑g) (𝓝 (stoneCechExtend hf (Quotient.mk (stoneCechSetoid α) z)))
⊢ ff (Quotient.mk (stoneCechSetoid α) x) = ff (Quotient.mk (stoneCechSetoid α) y)
[PROOFSTEP]
exact tendsto_nhds_unique (lim x gx) (lim y gy)
