awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
a : Set α
xi :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    x
⊢ (fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a ∈ (↑u : Filter (Ultrafilter α))

Tactic:
exact h _ xi
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
⊢ CompactSpace.{u} (Ultrafilter α)

Tactic:
⟨isCompact_iff_ultrafilter_le_nhds.mpr fun f _ ↦
      ⟨joinM f, trivial, ultrafilter_converges_iff.mpr rfl⟩⟩

Premises used: Iff.mpr, trivial, isCompact_iff_ultrafilter_le_nhds, CompactSpace.mk, And.intro, Exists.intro, ultrafilter_converges_iff, rfl, joinM
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
⊢ T2Space.{u} (Ultrafilter α)

Tactic:
t2_iff_ultrafilter.mpr fun {x y} f fx fy ↦
    have hx : x = joinM f := ultrafilter_converges_iff.mp fx
    have hy : y = joinM f := ultrafilter_converges_iff.mp fy
    hx.trans hy.symm

Premises used: Iff.mpr, Iff.mp, t2_iff_ultrafilter, ultrafilter_converges_iff, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
rw : ∀ (x : Ultrafilter α), connectedComponent x = {x}
⊢ TotallyDisconnectedSpace.{u} (Ultrafilter α)

Tactic:
rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]

Premises used: totallyDisconnectedSpace_iff_connectedComponent_singleton
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
A : Ultrafilter α
simp : ∀ x ∈ connectedComponent A, x = A
⊢ connectedComponent A = {A}

Tactic:
simp only [Set.eq_singleton_iff_unique_mem, mem_connectedComponent, true_and]

Premises used: mem_connectedComponent, Set.eq_singleton_iff_unique_mem, true_and
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
rw : (↑B : Filter α) ≤ (↑A : Filter α)
⊢ B = A

Tactic:
rw [← Ultrafilter.coe_le_coe]

Premises used: Ultrafilter.coe_le_coe
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
s : Set α
hs : s ∈ (↑A : Filter α)
rw :
  ∀ (hB : ∀ (i : { s : Set (Ultrafilter α) // IsClopen s ∧ A ∈ s }), B ∈ (↑i : Set (Ultrafilter α))) ⦃s : Set α⦄
    (hs : s ∈ (↑A : Filter α)), s ∈ (↑B : Filter α)
⊢ s ∈ (↑B : Filter α)

Tactic:
rw [connectedComponent_eq_iInter_isClopen, Set.mem_iInter] at hB

Premises used: Set.mem_iInter, connectedComponent_eq_iInter_isClopen
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
A B : Ultrafilter α
hB : ∀ (i : { s : Set (Ultrafilter α) // IsClopen s ∧ A ∈ s }), B ∈ (↑i : Set (Ultrafilter α))
s : Set α
hs : s ∈ (↑A : Filter α)
Z : Set (Ultrafilter α) := {F : Ultrafilter α | s ∈ F}
⊢ IsClopen Z

Tactic:
have hZ : IsClopen Z := ⟨ultrafilter_isClosed_basic s, ultrafilter_isOpen_basic s⟩
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
A B : Ultrafilter α
hB : ∀ (i : { s : Set (Ultrafilter α) // IsClopen s ∧ A ∈ s }), B ∈ (↑i : Set (Ultrafilter α))
s : Set α
hs : s ∈ (↑A : Filter α)
Z : Set (Ultrafilter α) := {F : Ultrafilter α | s ∈ F}
hZ : IsClopen Z
⊢ s ∈ (↑B : Filter α)

Tactic:
hB ⟨Z, hZ, hs⟩

Premises used: Set.Mem, setOf, Subtype.mk, And.intro
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
A B : Ultrafilter α
hB : ∀ (i : { s : Set (Ultrafilter α) // IsClopen s ∧ A ∈ s }), B ∈ (↑i : Set (Ultrafilter α))
s : Set α
hs : s ∈ (↑A : Filter α)
Z : Set (Ultrafilter α) := {F : Ultrafilter α | s ∈ F}
hZ : IsClopen Z
⊢ s ∈ (↑B : Filter α)

Tactic:
exact hB ⟨Z, hZ, hs⟩

Premises used: Subtype.mk, And.intro
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
b : Ultrafilter α
rw : b = joinM (map pure b)
⊢ Tendsto pure (↑b : Filter α) (𝓝 b)

Tactic:
rw [Tendsto, ← coe_map, ultrafilter_converges_iff]

Premises used: Ultrafilter.coe_map, Filter.Tendsto, ultrafilter_converges_iff
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
b : Ultrafilter α
h : ∀ (s : Set α), s ∈ b ↔ s ∈ joinM (map pure b)
⊢ b = joinM (map pure b)

Tactic:
ext s
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
b : Ultrafilter α
s : Set α
h : s ∈ b ↔ Membership.mem (γ := Ultrafilter (Ultrafilter α)) (map pure b) {t : Ultrafilter α | s ∈ t}
⊢ s ∈ b ↔ s ∈ joinM (map pure b)

Tactic:
change s ∈ b ↔ {t | s ∈ t} ∈ map pure b

Premises used: Pure.pure, Ultrafilter.map
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
b : Ultrafilter α
s : Set α
h : s ∈ b ↔ preimage (β := Ultrafilter α) pure {t : Ultrafilter α | s ∈ t} ∈ b
h₁ : s ∈ b ↔ {a : α | Membership.mem (γ := Ultrafilter α) (pure a) s} ∈ b
h₂ : s ∈ b ↔ {a : α | a ∈ s} ∈ b
⊢ s ∈ b ↔ Membership.mem (γ := Ultrafilter (Ultrafilter α)) (map pure b) {t : Ultrafilter α | s ∈ t}

Tactic:
simp_rw [mem_map, preimage_setOf_eq, mem_pure, setOf_mem_eq]

Premises used: Ultrafilter.mem_pure, Ultrafilter.mem_map, Set.setOf_mem_eq, Set.preimage_setOf_eq
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
b : Ultrafilter α
rw :
  comap (β := Ultrafilter α) pure
      (⨅ (s : Set (Ultrafilter α)),
        ⨅ (_ :
          Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α} s),
          𝓟 s) ≤
    (↑b : Filter α)
⊢ comap pure (𝓝 b) ≤ (↑b : Filter α)

Tactic:
rw [TopologicalSpace.nhds_generateFrom]

Premises used: TopologicalSpace.nhds_generateFrom
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
b : Ultrafilter α
simp :
  ⨅ (i : Set (Ultrafilter α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α} i),
        𝓟 (pure ⁻¹' i) ≤
    (↑b : Filter α)
⊢ comap (β := Ultrafilter α) pure
      (⨅ (s : Set (Ultrafilter α)),
        ⨅ (_ :
          Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α} s),
          𝓟 s) ≤
    (↑b : Filter α)

Tactic:
simp only [comap_iInf, comap_principal]

Premises used: Filter.comap_iInf, Filter.comap_principal
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ (↑b : Filter α)
rw :
  ⨅ (i : Set (Ultrafilter α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α} i),
        𝓟 (pure ⁻¹' i) ≤
    𝓟 s
⊢ Membership.mem (γ := Filter α)
    (⨅ (i : Set (Ultrafilter α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α} i),
        𝓟 (pure ⁻¹' i))
    s

Tactic:
rw [← le_principal_iff]

Premises used: Filter.le_principal_iff
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ (↑b : Filter α)
⊢ ⨅ (i : Set (Ultrafilter α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α} i),
        𝓟 (pure ⁻¹' i) ≤
    𝓟 s

Tactic:
iInf_le_of_le { u | s ∈ u } ?_

Premises used: Set.Mem, setOf, Membership.mem, iInf_le_of_le
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ (↑b : Filter α)
refine :
  ⨅ (_ :
      Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α}
        {u : Ultrafilter α | s ∈ u}),
      𝓟 (preimage (β := Ultrafilter α) pure {u : Ultrafilter α | s ∈ u}) ≤
    𝓟 s
⊢ ⨅ (i : Set (Ultrafilter α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α} i),
        𝓟 (pure ⁻¹' i) ≤
    𝓟 s

Tactic:
refine iInf_le_of_le { u | s ∈ u } ?_

Premises used: setOf, Membership.mem, iInf_le_of_le
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ (↑b : Filter α)
⊢ ⨅ (_ :
      Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α}
        {u : Ultrafilter α | s ∈ u}),
      𝓟 (preimage (β := Ultrafilter α) pure {u : Ultrafilter α | s ∈ u}) ≤
    𝓟 s

Tactic:
iInf_le_of_le ⟨hs, ⟨s, rfl⟩⟩ ?_

Premises used: Set.Mem, And.intro, Exists.intro, iInf_le_of_le, rfl
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ (↑b : Filter α)
refine : 𝓟 (preimage (β := Ultrafilter α) pure {u : Ultrafilter α | s ∈ u}) ≤ 𝓟 s
⊢ ⨅ (_ :
      Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α}
        {u : Ultrafilter α | s ∈ u}),
      𝓟 (preimage (β := Ultrafilter α) pure {u : Ultrafilter α | s ∈ u}) ≤
    𝓟 s

Tactic:
refine iInf_le_of_le ⟨hs, ⟨s, rfl⟩⟩ ?_

Premises used: iInf_le_of_le
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ (↑b : Filter α)
⊢ 𝓟 (preimage (β := Ultrafilter α) pure {u : Ultrafilter α | s ∈ u}) ≤ 𝓟 s

Tactic:
principal_mono.2 fun _ ↦ id

Premises used: Iff.mpr, Filter.principal_mono, id
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ (↑b : Filter α)
⊢ 𝓟 (preimage (β := Ultrafilter α) pure {u : Ultrafilter α | s ∈ u}) ≤ 𝓟 s

Tactic:
exact principal_mono.2 fun _ ↦ id

Premises used: Iff.mpr, Filter.principal_mono, id
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
⊢ DenseRange.{u, u} (X := Ultrafilter α) pure

Tactic:
fun x ↦ mem_closure_iff_ultrafilter.mpr
    ⟨x.map pure, range_mem_map, ultrafilter_converges_iff.mpr (bind_pure x).symm⟩

Premises used: Pure.pure, Iff.mpr, Dense, bind_pure, mem_closure_iff_ultrafilter, And.intro, Exists.intro, DenseRange, Filter.range_mem_map, ultrafilter_converges_iff, Ultrafilter.map, Eq.symm
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
h : ∀ (x : α), IsOpen[induced pure Ultrafilter.topologicalSpace] {x}
⊢ Eq.{u + 1} (α := TopologicalSpace α) (induced pure Ultrafilter.topologicalSpace) ⊥

Tactic:
apply eq_bot_of_singletons_open

Premises used: eq_bot_of_singletons_open
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
x : α
right : Eq (α := Set α) (preimage (β := Ultrafilter α) pure {u : Ultrafilter α | {x} ∈ u}) {x}
⊢ IsOpen[induced pure Ultrafilter.topologicalSpace] {x}

Tactic:
use { u : Ultrafilter α | {x} ∈ u }, ultrafilter_isOpen_basic _

Premises used: ultrafilter_isOpen_basic, Ultrafilter
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
x : α
⊢ Eq (α := Set α) (preimage (β := Ultrafilter α) pure {u : Ultrafilter α | {x} ∈ u}) {x}

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
⊢ IsDenseInducing.{u, u} (α := α) (β := Ultrafilter α) pure

Tactic:
letI : TopologicalSpace α := ⊥
  ⟨⟨induced_topology_pure.symm⟩, denseRange_pure⟩

Premises used: denseRange_pure, induced_topology_pure, IsDenseInducing.mk, Topology.IsInducing.mk, Eq.symm
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
⊢ IsDenseEmbedding.{u, u} (α := α) (β := Ultrafilter α) pure

Tactic:
letI : TopologicalSpace α := ⊥
  { isDenseInducing_pure with injective := Ultrafilter.pure_injective }

Premises used: IsDenseEmbedding.mk, Ultrafilter.pure_injective, isDenseInducing_pure
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
f : α → γ
this : TopologicalSpace α := ⊥
⊢ DiscreteTopology α

Tactic:
haveI : DiscreteTopology α := ⟨rfl⟩
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
f : α → γ
this_1 : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ Ultrafilter.extend f ∘ pure = f

Tactic:
funext (isDenseInducing_pure.extend_eq continuous_of_discreteTopology)

Premises used: funext, isDenseInducing_pure, continuous_of_discreteTopology, IsDenseInducing.extend_eq
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
f : α → γ
this_1 : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ Ultrafilter.extend f ∘ pure = f

Tactic:
exact funext (isDenseInducing_pure.extend_eq continuous_of_discreteTopology)

Premises used: funext, isDenseInducing_pure, continuous_of_discreteTopology, IsDenseInducing.extend_eq
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
f : α → γ
a : α
⊢ Ultrafilter.extend f (pure a) = f a

Tactic:
congr_fun (ultrafilter_extend_extends f) a

Premises used: Classical.epsilon, ultrafilter_extend_extends, Ultrafilter.extend, Filter.lim, congr_fun, Filter.limUnder, IsDenseInducing.extend
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
b : Ultrafilter α
rw : univ ∈ (↑(Ultrafilter.map f b) : Filter γ)
⊢ (↑(Ultrafilter.map f b) : Filter γ) ≤ 𝓟 univ

Tactic:
rw [le_principal_iff]

Premises used: Filter.le_principal_iff
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ univ ∈ (↑(Ultrafilter.map f b) : Filter γ)

Tactic:
univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ univ ∈ (↑(Ultrafilter.map f b) : Filter γ)

Tactic:
exact univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
⊢ ∀ (b : Ultrafilter α), ∃ (c : γ), Tendsto f (comap pure (𝓝 b)) (𝓝 c)

Tactic:
have h (b : Ultrafilter α) : ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c) :=
    -- 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'⟩
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ (c : γ), Tendsto f (comap pure (𝓝 b)) (𝓝 c)
x : TopologicalSpace α := ⊥
⊢ Continuous[_, inst] (Ultrafilter.extend f)

Tactic:
isDenseInducing_pure.continuous_extend h

Premises used: IsDenseInducing.continuous_extend, isDenseInducing_pure, Ultrafilter.extend
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ (c : γ), Tendsto f (comap pure (𝓝 b)) (𝓝 c)
x : TopologicalSpace α := ⊥
⊢ Continuous[_, inst] (Ultrafilter.extend f)

Tactic:
exact isDenseInducing_pure.continuous_extend h

Premises used: IsDenseInducing.continuous_extend, isDenseInducing_pure
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
⊢ (↑b' : Filter (Ultrafilter α)) ≤ 𝓝 b

Tactic:
have t : ↑b' ≤ 𝓝 b := ultrafilter_converges_iff.mpr (bind_pure _).symm
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : (↑b' : Filter (Ultrafilter α)) ≤ 𝓝 b
rw : (↑(Ultrafilter.map f b) : Filter γ) ≤ 𝓝 (Ultrafilter.extend f b)
⊢ (↑(Ultrafilter.map f b) : Filter γ) ≤ 𝓝 c

Tactic:
rw [← h]
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : (↑b' : Filter (Ultrafilter α)) ≤ 𝓝 b
⊢ Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))

Tactic:
have := (continuous_ultrafilter_extend f).tendsto b
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : (↑b' : Filter (Ultrafilter α)) ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ (↑(Ultrafilter.map f b) : Filter γ) ≤ 𝓝 (Ultrafilter.extend f b)

Tactic:
le_trans ?_ (le_trans (map_mono t) this)

Premises used: Filter.map_mono, le_trans
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : (↑b' : Filter (Ultrafilter α)) ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
refine : (↑(Ultrafilter.map f b) : Filter γ) ≤ map (Ultrafilter.extend f) (↑b' : Filter (Ultrafilter α))
⊢ (↑(Ultrafilter.map f b) : Filter γ) ≤ 𝓝 (Ultrafilter.extend f b)

Tactic:
refine le_trans ?_ (le_trans (map_mono t) this)

Premises used: Filter.map_mono, le_trans
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : (↑b' : Filter (Ultrafilter α)) ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
change : (↑(Ultrafilter.map f b) : Filter γ) ≤ map (Ultrafilter.extend f ∘ pure) (↑b : Filter α)
⊢ (↑(Ultrafilter.map f b) : Filter γ) ≤ map (Ultrafilter.extend f) (↑b' : Filter (Ultrafilter α))

Tactic:
change _ ≤ map (Ultrafilter.extend f ∘ pure) ↑b

Premises used: Pure.pure, Filter.map, Function.comp, Ultrafilter.extend, Ultrafilter.toFilter
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : (↑b' : Filter (Ultrafilter α)) ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
rw : (↑(Ultrafilter.map f b) : Filter γ) ≤ map f (↑b : Filter α)
⊢ (↑(Ultrafilter.map f b) : Filter γ) ≤ map (Ultrafilter.extend f ∘ pure) (↑b : Filter α)

Tactic:
rw [ultrafilter_extend_extends]

Premises used: ultrafilter_extend_extends
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : (↑b' : Filter (Ultrafilter α)) ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ (↑(Ultrafilter.map f b) : Filter γ) ≤ map f (↑b : Filter α)

Tactic:
le_rfl

Premises used: le_rfl, Set.Mem
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : (↑b' : Filter (Ultrafilter α)) ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ (↑(Ultrafilter.map f b) : Filter γ) ≤ map f (↑b : Filter α)

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
⊢ CompactSpace.{u} (PreStoneCech α)

Tactic:
Quot.compactSpace

Premises used: PreStoneCech, Quot.compactSpace
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
x : α
g : Ultrafilter α
gx : (↑g : Filter α) ≤ 𝓝 x
rw : g >>= pure = joinM (Ultrafilter.map pure (g >>= pure))
⊢ (↑(Ultrafilter.map pure g) : Filter (Ultrafilter α)) ≤ 𝓝 g

Tactic:
rw [ultrafilter_converges_iff, ← bind_pure g]

Premises used: bind_pure, ultrafilter_converges_iff
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
x : α
g : Ultrafilter α
gx : (↑g : Filter α) ≤ 𝓝 x
⊢ g >>= pure = joinM (Ultrafilter.map pure (g >>= pure))

Tactic:
rfl
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
x : α
g : Ultrafilter α
gx : (↑g : Filter α) ≤ 𝓝 x
⊢ (↑(Ultrafilter.map pure g) : Filter (Ultrafilter α)) ≤ 𝓝 g

Tactic:
have : (g.map pure).toFilter ≤ 𝓝 g := by
      rw [ultrafilter_converges_iff, ← bind_pure g]
      rfl
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
x : α
g : Ultrafilter α
gx : (↑g : Filter α) ≤ 𝓝 x
this : (↑(Ultrafilter.map pure g) : Filter (Ultrafilter α)) ≤ 𝓝 g
⊢ LE.le (α := Filter (PreStoneCech α)) (map preStoneCechUnit (↑g : Filter α))
    (𝓝 (Quot.mk (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) g))

Tactic:
have : (map preStoneCechUnit g : Filter (PreStoneCech α)) ≤ 𝓝 (Quot.mk _ g) :=
      (map_mono this).trans (continuous_quot_mk.tendsto _)
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
x : α
g : Ultrafilter α
gx : (↑g : Filter α) ≤ 𝓝 x
this_1 : (↑(Ultrafilter.map pure g) : Filter (Ultrafilter α)) ≤ 𝓝 g
this :
  LE.le (α := Filter (PreStoneCech α)) (map preStoneCechUnit (↑g : Filter α))
    (𝓝 (Quot.mk (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) g))
⊢ LE.le (α := Filter (PreStoneCech α)) (map preStoneCechUnit (↑g : Filter α))
    (𝓝 (Quot.mk (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) g))

Tactic:
this
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
x : α
g : Ultrafilter α
gx : (↑g : Filter α) ≤ 𝓝 x
this_1 : (↑(Ultrafilter.map pure g) : Filter (Ultrafilter α)) ≤ 𝓝 g
this :
  LE.le (α := Filter (PreStoneCech α)) (map preStoneCechUnit (↑g : Filter α))
    (𝓝 (Quot.mk (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) g))
h :
  Eq (α := PreStoneCech α) (preStoneCechUnit x)
    (Quot.mk (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) g)
⊢ Tendsto (β := PreStoneCech α) preStoneCechUnit (↑g : Filter α) (𝓝 (preStoneCechUnit x))

Tactic:
convert! this
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
x : α
g : Ultrafilter α
gx : (↑g : Filter α) ≤ 𝓝 x
this_1 : (↑(Ultrafilter.map pure g) : Filter (Ultrafilter α)) ≤ 𝓝 g
this :
  LE.le (α := Filter (PreStoneCech α)) (map preStoneCechUnit (↑g : Filter α))
    (𝓝 (Quot.mk (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) g))
⊢ Eq (α := PreStoneCech α) (preStoneCechUnit x)
    (Quot.mk (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) g)

Tactic:
Quot.sound ⟨x, pure_le_nhds x, gx⟩

Premises used: Quot.sound, pure_le_nhds, preStoneCechUnit, PreStoneCech, And.intro, Exists.intro