awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Sphere (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
have have₁ have₂ have₃ : (this : Nonempty ι) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have₄ :
  (this : Nonempty ι) →
    let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
    (hv : ‖v‖ = 1) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have₅ :
  (this : Nonempty ι) →
    let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
    (hv : ‖v‖ = 1) → (hv₀ : v ≠ 0) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have₆ :
  (this : Nonempty ι) →
    let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
    (hv : ‖v‖ = 1) →
      (hv₀ : v ≠ 0) →
        (this : Fact (finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1)) →
          Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
⊢ Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have have₇ : (this : Nonempty ι) →
  let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
  (hv : ‖v‖ = 1) →
    (hv₀ : v ≠ 0) →
      (this : Fact (finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1)) →
        (hV : finrank ℝ V = finrank.{0, u_1} ℝ ↥(ℝ ∙ v)ᗮ) →
          Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
Tactic: classical
  have : Nonempty ι := Fintype.card_pos_iff.mp <| by lia
  let v : EuclideanSpace ℝ ι := .single (Classical.arbitrary ι) 1
  have hv : ‖v‖ = 1 := by simp [v]
  have hv₀ : v ≠ 0 := fun contra ↦ by simp [contra] at hv
  have : Fact (finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1) := ⟨by simp [h]⟩
  have hV : finrank ℝ V = finrank ℝ (ℝ ∙ v)ᗮ := (finrank_orthogonal_span_singleton hv₀).symm
  letI e : V ≃ₜ (ℝ ∙ v)ᗮ := (FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq hV).some
  exact e.onePointCongr.trans <| onePointHyperplaneHomeoUnitSphere hv
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
a b : Set α
u : Ultrafilter α
ua :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    u
ub :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b)
    u
⊢ ∃ t₃ ∈ ultrafilterBasis α,
    u ∈ t₃ ∧
      t₃ ⊆
        (fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a ∩
          (fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b
have refine_1 : ∀ (v : Ultrafilter α)
  (hv :
    Membership.mem (γ := Set (Ultrafilter α))
      ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) (a ∩ b)) v),
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    v
Tactic: refine ⟨_, ⟨a ∩ b, rfl⟩, inter_mem ua ub, fun v hv ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
a b : Set α
u : Ultrafilter α
ua :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    u
ub :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b)
    u
refine_1 :
  ∀ (v : Ultrafilter α)
    (hv :
      Membership.mem (γ := Set (Ultrafilter α))
        ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) (a ∩ b)) v),
    Membership.mem (γ := Set (Ultrafilter α))
      ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a) v
⊢ ∃ t₃ ∈ ultrafilterBasis α,
    u ∈ t₃ ∧
      t₃ ⊆
        (fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a ∩
          (fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b
have refine_2 : ∀ (v : Ultrafilter α)
  (hv :
    Membership.mem (γ := Set (Ultrafilter α))
      ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) (a ∩ b)) v),
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b)
    v
Tactic: refine ⟨_, ⟨a ∩ b, rfl⟩, inter_mem ua ub, fun v hv ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
a b : Set α
u : Ultrafilter α
ua :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    u
ub :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b)
    u
v : Ultrafilter α
hv :
  Membership.mem (γ := Set (Ultrafilter α))
    ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) (a ∩ b)) v
⊢ Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    v
have refine_1 : a ∩ b ⊆ a
Tactic: apply mem_of_superset hv
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
a b : Set α
u : Ultrafilter α
ua :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    u
ub :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b)
    u
v : Ultrafilter α
hv :
  Membership.mem (γ := Set (Ultrafilter α))
    ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) (a ∩ b)) v
⊢ Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b)
    v
have refine_2 : a ∩ b ⊆ b
Tactic: apply mem_of_superset hv
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
s : Set α
⊢ IsClosed.{u} (X := Ultrafilter α) {u : Ultrafilter α | s ∈ u}
have rw : IsOpen.{u} (X := Ultrafilter α) {u : Ultrafilter α | s ∈ u}ᶜ
Tactic: rw [← isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
s : Set α
⊢ IsOpen.{u} (X := Ultrafilter α) {u : Ultrafilter α | s ∈ u}ᶜ
have h : Eq.{u + 1} (α := Set (Ultrafilter α)) {u : Ultrafilter α | s ∈ u}ᶜ {u : Ultrafilter α | sᶜ ∈ u}
Tactic: convert! ultrafilter_isOpen_basic sᶜ using 1
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
s : Set α
⊢ Eq.{u + 1} (α := Set (Ultrafilter α)) {u : Ultrafilter α | s ∈ u}ᶜ {u : Ultrafilter α | sᶜ ∈ u}
have h : ∀ (u : Ultrafilter α),
  Membership.mem (γ := Set (Ultrafilter α)) {u : Ultrafilter α | s ∈ u}ᶜ u ↔
    Membership.mem (γ := Set (Ultrafilter α)) {u : Ultrafilter α | sᶜ ∈ u} u
Tactic: ext u
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (↑u : Filter (Ultrafilter α)) ≤ 𝓝 x ↔ x = joinM u
have rw : (↑u : Filter (Ultrafilter α)) ≤ 𝓝 x ↔ (↑(joinM u) : Filter α) ≤ (↑x : Filter α)
Tactic: rw [eq_comm, ← Ultrafilter.coe_le_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (↑u : Filter (Ultrafilter α)) ≤ 𝓝 x ↔ (↑(joinM u) : Filter α) ≤ (↑x : Filter α)
have change : (↑u : Filter (Ultrafilter α)) ≤ 𝓝 x ↔ ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
Tactic: change ↑u ≤ 𝓝 x ↔ ∀ s ∈ x, { v : Ultrafilter α | s ∈ v } ∈ u
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (↑u : Filter (Ultrafilter α)) ≤ 𝓝 x ↔ ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
have simp : (∀ (i : Set (Ultrafilter α))
    (i_1 :
      x ∈ i ∧ Membership.mem (γ := Set (Set (Ultrafilter α))) (range fun (s : Set α) ↦ {u : Ultrafilter α | s ∈ u}) i),
    i ∈ (↑u : Filter (Ultrafilter α))) ↔
  ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
Tactic: simp only [TopologicalSpace.nhds_generateFrom, le_iInf_iff, ultrafilterBasis, le_principal_iff,
    mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α))
      (i_1 :
        x ∈ i ∧
          Membership.mem (γ := Set (Set (Ultrafilter α))) (range fun (s : Set α) ↦ {u : Ultrafilter α | s ∈ u}) i),
      i ∈ (↑u : Filter (Ultrafilter α))) ↔
    ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
have mp : (∀ (i : Set (Ultrafilter α))
    (i_1 :
      x ∈ i ∧ Membership.mem (γ := Set (Set (Ultrafilter α))) (range fun (s : Set α) ↦ {u : Ultrafilter α | s ∈ u}) i),
    i ∈ (↑u : Filter (Ultrafilter α))) →
  ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
mp :
  (∀ (i : Set (Ultrafilter α))
      (i_1 :
        x ∈ i ∧
          Membership.mem (γ := Set (Set (Ultrafilter α))) (range fun (s : Set α) ↦ {u : Ultrafilter α | s ∈ u}) i),
      i ∈ (↑u : Filter (Ultrafilter α))) →
    ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
⊢ (∀ (i : Set (Ultrafilter α))
      (i_1 :
        x ∈ i ∧
          Membership.mem (γ := Set (Set (Ultrafilter α))) (range fun (s : Set α) ↦ {u : Ultrafilter α | s ∈ u}) i),
      i ∈ (↑u : Filter (Ultrafilter α))) ↔
    ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
have mpr : (∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u) →
  ∀ (i : Set (Ultrafilter α))
    (i_1 :
      x ∈ i ∧ Membership.mem (γ := Set (Set (Ultrafilter α))) (range fun (s : Set α) ↦ {u : Ultrafilter α | s ∈ u}) i),
    i ∈ (↑u : Filter (Ultrafilter α))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
⊢ TotallyDisconnectedSpace.{u} (Ultrafilter α)
have rw : ∀ (x : Ultrafilter α), connectedComponent x = {x}
Tactic: rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
A : Ultrafilter α
⊢ connectedComponent A = {A}
have simp : ∀ x ∈ connectedComponent A, x = A
Tactic: simp only [Set.eq_singleton_iff_unique_mem, mem_connectedComponent, true_and]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
⊢ B = A
have rw : (↑B : Filter α) ≤ (↑A : Filter α)
Tactic: rw [← Ultrafilter.coe_le_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
s : Set α
hs : s ∈ (↑A : Filter α)
⊢ s ∈ (↑B : Filter α)
have rw : ∀ (hB : ∀ (i : { s : Set (Ultrafilter α) // IsClopen s ∧ A ∈ s }), B ∈ (↑i : Set (Ultrafilter α))) ⦃s : Set α⦄
  (hs : s ∈ (↑A : Filter α)), s ∈ (↑B : Filter α)
Tactic: rw [connectedComponent_eq_iInter_isClopen, Set.mem_iInter] at hB
Cleared hypotheses: hB, s, hs
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (hypothesis)
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}
⊢ s ∈ (↑B : Filter α)
have hZ : IsClopen Z
Tactic: have hZ : IsClopen Z := ⟨ultrafilter_isClosed_basic s, ultrafilter_isOpen_basic s⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
b : Ultrafilter α
⊢ Tendsto pure (↑b : Filter α) (𝓝 b)
have rw : b = joinM (map pure b)
Tactic: rw [Tendsto, ← coe_map, ultrafilter_converges_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
b : Ultrafilter α
⊢ b = joinM (map pure b)
have h : ∀ (s : Set α), s ∈ b ↔ s ∈ joinM (map pure b)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
b : Ultrafilter α
s : Set α
⊢ s ∈ b ↔ s ∈ joinM (map pure b)
have h : s ∈ b ↔ Membership.mem (γ := Ultrafilter (Ultrafilter α)) (map pure b) {t : Ultrafilter α | s ∈ t}
Tactic: change s ∈ b ↔ {t | s ∈ t} ∈ map pure b
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
b : Ultrafilter α
s : Set α
⊢ s ∈ b ↔ Membership.mem (γ := Ultrafilter (Ultrafilter α)) (map pure b) {t : Ultrafilter α | s ∈ t}
have h : s ∈ b ↔ preimage (β := Ultrafilter α) pure {t : Ultrafilter α | s ∈ t} ∈ b
Tactic: simp_rw [mem_map, preimage_setOf_eq, mem_pure, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
b : Ultrafilter α
s : Set α
h : s ∈ b ↔ preimage (β := Ultrafilter α) pure {t : Ultrafilter α | s ∈ t} ∈ b
⊢ s ∈ b ↔ Membership.mem (γ := Ultrafilter (Ultrafilter α)) (map pure b) {t : Ultrafilter α | s ∈ t}
have h₁ : s ∈ b ↔ {a : α | Membership.mem (γ := Ultrafilter α) (pure a) s} ∈ b
Tactic: simp_rw [mem_map, preimage_setOf_eq, mem_pure, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
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
⊢ s ∈ b ↔ Membership.mem (γ := Ultrafilter (Ultrafilter α)) (map pure b) {t : Ultrafilter α | s ∈ t}
have h₂ : s ∈ b ↔ {a : α | a ∈ s} ∈ b
Tactic: simp_rw [mem_map, preimage_setOf_eq, mem_pure, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
b : Ultrafilter α
⊢ comap pure (𝓝 b) ≤ (↑b : Filter α)
have rw : comap (β := Ultrafilter α) pure
    (⨅ (s : Set (Ultrafilter α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α} s),
        𝓟 s) ≤
  (↑b : Filter α)
Tactic: rw [TopologicalSpace.nhds_generateFrom]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
b : Ultrafilter α
⊢ comap (β := Ultrafilter α) pure
      (⨅ (s : Set (Ultrafilter α)),
        ⨅ (_ :
          Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α} s),
          𝓟 s) ≤
    (↑b : Filter α)
have simp : ⨅ (i : Set (Ultrafilter α)),
    ⨅ (_ :
      Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α} i),
      𝓟 (pure ⁻¹' i) ≤
  (↑b : Filter α)
Tactic: simp only [comap_iInf, comap_principal]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ (↑b : Filter α)
⊢ Membership.mem (γ := Filter α)
    (⨅ (i : Set (Ultrafilter α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α} i),
        𝓟 (pure ⁻¹' i))
    s
have rw : ⨅ (i : Set (Ultrafilter α)),
    ⨅ (_ :
      Membership.mem (γ := Set (Set (Ultrafilter α))) {s : Set (Ultrafilter α) | b ∈ s ∧ s ∈ ultrafilterBasis α} i),
      𝓟 (pure ⁻¹' i) ≤
  𝓟 s
Tactic: rw [← le_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
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
have 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
Tactic: refine iInf_le_of_le { u | s ∈ u } ?_
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
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
have refine : 𝓟 (preimage (β := Ultrafilter α) pure {u : Ultrafilter α | s ∈ u}) ≤ 𝓟 s
Tactic: refine iInf_le_of_le ⟨hs, ⟨s, rfl⟩⟩ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
⊢ Eq.{u + 1} (α := TopologicalSpace α) (induced pure Ultrafilter.topologicalSpace) ⊥
have h : ∀ (x : α), IsOpen[induced pure Ultrafilter.topologicalSpace] {x}
Tactic: apply eq_bot_of_singletons_open
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
x : α
⊢ IsOpen[induced pure Ultrafilter.topologicalSpace] {x}
have right : Eq (α := Set α) (preimage (β := Ultrafilter α) pure {u : Ultrafilter α | {x} ∈ u}) {x}
Tactic: use { u : Ultrafilter α | {x} ∈ u }, ultrafilter_isOpen_basic _
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (hypothesis)
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
f : α → γ
this : TopologicalSpace α := ⊥
⊢ Ultrafilter.extend f ∘ pure = f
have this₁ : DiscreteTopology α
Tactic: haveI : DiscreteTopology α := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ (↑(Ultrafilter.map f b) : Filter γ) ≤ 𝓟 univ
have rw : univ ∈ (↑(Ultrafilter.map f b) : Filter γ)
Tactic: rw [le_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (hypothesis)
Goal:
α : Type u
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : T2Space γ
inst_2 : CompactSpace γ
f : α → γ
⊢ Continuous[_, inst] (Ultrafilter.extend f)
have h : ∀ (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'⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (hypothesis)
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
⊢ (↑(Ultrafilter.map f b) : Filter γ) ≤ 𝓝 c
have t : (↑b' : Filter (Ultrafilter α)) ≤ 𝓝 b
Tactic: have t : ↑b' ≤ 𝓝 b := ultrafilter_converges_iff.mpr (bind_pure _).symm
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
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
⊢ (↑(Ultrafilter.map f b) : Filter γ) ≤ 𝓝 c
have rw : (↑(Ultrafilter.map f b) : Filter γ) ≤ 𝓝 (Ultrafilter.extend f b)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (hypothesis)
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
⊢ (↑(Ultrafilter.map f b) : Filter γ) ≤ 𝓝 (Ultrafilter.extend f b)
have this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
Tactic: have := (continuous_ultrafilter_extend f).tendsto b
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
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)
have refine : (↑(Ultrafilter.map f b) : Filter γ) ≤ map (Ultrafilter.extend f) (↑b' : Filter (Ultrafilter α))
Tactic: refine le_trans ?_ (le_trans (map_mono t) this)
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
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 (Ultrafilter.extend f) (↑b' : Filter (Ultrafilter α))
have change : (↑(Ultrafilter.map f b) : Filter γ) ≤ map (Ultrafilter.extend f ∘ pure) (↑b : Filter α)
Tactic: change _ ≤ map (Ultrafilter.extend f ∘ pure) ↑b
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
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 (Ultrafilter.extend f ∘ pure) (↑b : Filter α)
have rw : (↑(Ultrafilter.map f b) : Filter γ) ≤ map f (↑b : Filter α)
Tactic: rw [ultrafilter_extend_extends]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
g : Ultrafilter α
gx : (↑g : Filter α) ≤ 𝓝 x
⊢ (↑(Ultrafilter.map pure g) : Filter (Ultrafilter α)) ≤ 𝓝 g
have rw : g >>= pure = joinM (Ultrafilter.map pure (g >>= pure))
Tactic: rw [ultrafilter_converges_iff, ← bind_pure g]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
g : Ultrafilter α
gx : (↑g : Filter α) ≤ 𝓝 x
⊢ Tendsto (β := PreStoneCech α) preStoneCechUnit (↑g : Filter α) (𝓝 (preStoneCechUnit x))
have this : (↑(Ultrafilter.map pure g) : Filter (Ultrafilter α)) ≤ 𝓝 g
Tactic: have : (g.map pure).toFilter ≤ 𝓝 g := by
      rw [ultrafilter_converges_iff, ← bind_pure g]
      rfl
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
g : Ultrafilter α
gx : (↑g : Filter α) ≤ 𝓝 x
this : (↑(Ultrafilter.map pure g) : Filter (Ultrafilter α)) ≤ 𝓝 g
⊢ Tendsto (β := PreStoneCech α) preStoneCechUnit (↑g : Filter α) (𝓝 (preStoneCechUnit x))
have this₁ : 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 _)
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
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))
⊢ Tendsto (β := PreStoneCech α) preStoneCechUnit (↑g : Filter α) (𝓝 (preStoneCechUnit x))
have h : Eq (α := PreStoneCech α) (preStoneCechUnit x)
  (Quot.mk (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) g)
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
g₁ g₂ : PreStoneCech α → β
h₁ : Continuous[_, inst_1] g₁
h₂ : Continuous[_, inst_1] g₂
h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit
⊢ g₁ = g₂
have apply : EqOn g₁ g₂ (range preStoneCechUnit)
Tactic: apply Continuous.ext_on denseRange_preStoneCechUnit h₁ h₂