awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ IsGδ s
have neg : ∀ (n : ℕ), IsOpen[inst] ((fun (n : ℕ) ↦ ((⇑f : (a : X) → ℝ) ⁻¹' Iio (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : Set X)) n)
Tactic: refine isGδ_iff_eq_iInter_nat.2 ⟨fun n => f ⁻¹' (Iio (1 / (n + 1))),
          fun n => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
neg :
  ∀ (n : ℕ), IsOpen[inst] ((fun (n : ℕ) ↦ ((⇑f : (a : X) → ℝ) ⁻¹' Iio (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : Set X)) n)
⊢ IsGδ s
have neg₁ : s = ⋂ (n : ℕ), (fun (n : ℕ) ↦ ((⇑f : (a : X) → ℝ) ⁻¹' Iio (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : Set X)) n
Tactic: refine isGδ_iff_eq_iInter_nat.2 ⟨fun n => f ⁻¹' (Iio (1 / (n + 1))),
          fun n => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ s = ⋂ (n : ℕ), (fun (n : ℕ) ↦ ((⇑f : (a : X) → ℝ) ⁻¹' Iio (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : Set X)) n
have neg : Eq (α := Set X) (preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0})
  (preimage (β := ℝ) (⇑f : (a : X) → ℝ)
    (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)))
Tactic: simp only [hf, ← preimage_iInter,
            ← preimage_range_inter (s := ⋂ (n : ℕ), Iio (1 / (n + 1) : ℝ)), inter_iInter]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ Eq (α := Set X) (preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0})
    (preimage (β := ℝ) (⇑f : (a : X) → ℝ)
      (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)))
have neg : Eq (α := Set ℝ) {0} (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1))
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ Eq (α := Set ℝ) {0} (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1))
have neg : Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) 0 ∧
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1))
        x →
      x = 0
Tactic: rw [eq_comm, eq_singleton_iff_unique_mem]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1))
      0 ∧
    ∀ (x : ℝ),
      Membership.mem (γ := Set ℝ)
          (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) x →
        x = 0
have neg : ∀ (n : ℕ), 0 ∈ range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: refine ⟨mem_iInter_of_mem fun n => ?_, fun x h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
neg : ∀ (n : ℕ), 0 ∈ range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1))
      0 ∧
    ∀ (x : ℝ),
      Membership.mem (γ := Set ℝ)
          (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) x →
        x = 0
have neg₁ : ∀ (x : ℝ)
  (h :
    Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1))
      x),
  x = 0
Tactic: refine ⟨mem_iInter_of_mem fun n => ?_, fun x h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : ℝ
h :
  Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) x
⊢ x = 0
have neg : x ≤ 0
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : ℝ
h :
  Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) x
neg : x ≤ 0
⊢ x = 0
have neg₁ : 0 ≤ x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : ℝ
h :
  Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) x
⊢ x ≤ 0
have h₁ : ∀ (i : ℕ), Membership.mem (γ := Set ℝ) (range (ι := X) (⇑f : (a : X) → ℝ)) x ∧ x < 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: simp only [mem_iInter, mem_inter_iff, mem_Iio] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : ℝ
h :
  Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) x
⊢ 0 ≤ x
have neg : ∀ (x : X)
  (h :
    Membership.mem (α := ℝ) (γ := Set ℝ)
      (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1))
      ((f : (a : X) → ℝ) x : ℝ)),
  LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
Tactic: rcases (mem_iInter.1 h 0).1 with ⟨x, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X → Y
he : IsEmbedding e
inst_2 : PerfectlyNormalSpace Y
⊢ PerfectlyNormalSpace X
have rw : ∀ (s : Set X),
  IsClosed[inst] s →
    ∃ (f : C(X, ℝ)),
      s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: rw [perfectlyNormalSpace_iff_forall_isClosed_preimage_zero]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X → Y
he : IsEmbedding e
inst_2 : PerfectlyNormalSpace Y
t : Set X
ht : IsClosed[inst] t
⊢ ∃ (f : C(X, ℝ)),
    t = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have obtain : ∀ (c : Set Y) (hc : IsClosed[inst_1] c ∧ e '' t = c ∩ range e),
  ∃ (f : C(X, ℝ)),
    t = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: obtain ⟨c, hc⟩ : ∃ c, IsClosed c ∧ e '' t = c ∩ range e := he.image_eq_isClosed_inter_range ht
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X → Y
he : IsEmbedding e
inst_2 : PerfectlyNormalSpace Y
t : Set X
ht : IsClosed[inst] t
c : Set Y
hc : IsClosed[inst_1] c ∧ e '' t = c ∩ range e
⊢ ∃ (f : C(X, ℝ)),
    t = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have obtain : ∀ (f : C(Y, ℝ)) (hf : ∀ (x : Y), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : Y) → ℝ) x : ℝ))
  (hc :
    IsClosed[inst_1] (preimage (β := ℝ) (⇑f : (a : Y) → ℝ) {0}) ∧
      e '' t = preimage (β := ℝ) (⇑f : (a : Y) → ℝ) {0} ∩ range e),
  ∃ (f : C(X, ℝ)),
    t = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: obtain ⟨f, rfl, hf⟩ :=
    perfectlyNormalSpace_iff_forall_isClosed_preimage_zero.1 inferInstance c hc.1
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X → Y
he : IsEmbedding e
inst_2 : PerfectlyNormalSpace Y
t : Set X
ht : IsClosed[inst] t
f : C(Y, ℝ)
hf : ∀ (x : Y), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : Y) → ℝ) x : ℝ)
hc :
  IsClosed[inst_1] (preimage (β := ℝ) (⇑f : (a : Y) → ℝ) {0}) ∧
    e '' t = preimage (β := ℝ) (⇑f : (a : Y) → ℝ) {0} ∩ range e
⊢ ∃ (f : C(X, ℝ)),
    t = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have refine : t = preimage (β := ℝ) (⇑{ toFun := (⇑f : (a : Y) → ℝ) ∘ e, continuous_toFun := sorry : C(X, ℝ) } : (a : X) → ℝ) {0}
Tactic: refine ⟨⟨f ∘ e, f.continuous.comp he.continuous⟩, ?_, fun x => hf (e x)⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
⊢ TotallySeparatedSpace X
have isTotallySeparated_univ : IsTotallySeparated.{u_1} (α := X) univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
have isTotallySeparated_univ : ∀ (U : Set X) (hU : IsOpen[inst] U ∧ Xor (x ∈ U) (y ∈ U)),
  ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Tactic: choose U hU using exists_isOpen_xor_mem hxy
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU : IsOpen[inst] U ∧ Xor (x ∈ U) (y ∈ U)
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
have hU₀ : IsOpen[inst] U
Tactic: obtain ⟨hU₀, hU₁⟩ := hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU : IsOpen[inst] U ∧ Xor (x ∈ U) (y ∈ U)
hU₀ : IsOpen[inst] U
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
have hU₁ : Xor (x ∈ U) (y ∈ U)
Tactic: obtain ⟨hU₀, hU₁⟩ := hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst] U
hU₁ : Xor (x ∈ U) (y ∈ U)
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
have isTotallySeparated_univ : ∀ (hx : x ∈ U ∧ y ∉ U),
  ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Tactic: rcases hU₁ with hx | hy
Cleared hypotheses: hU₁
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst] U
hU₁ : Xor (x ∈ U) (y ∈ U)
isTotallySeparated_univ :
  ∀ (hx : x ∈ U ∧ y ∉ U),
    ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
have isTotallySeparated_univ₁ : ∀ (hy : y ∈ U ∧ x ∉ U),
  ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Tactic: rcases hU₁ with hx | hy
Cleared hypotheses: hU₁
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst] U
hx : x ∈ U ∧ y ∉ U
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
have isTotallySeparated_univ : ∀ (V : Set X) (hV : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} V ∧ x ∈ V ∧ V ⊆ U),
  ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Tactic: choose V hV using h.isOpen_iff.mp hU₀ x hx.1
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst] U
hy : y ∈ U ∧ x ∉ U
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
have isTotallySeparated_univ : ∀ (V : Set X) (hV : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} V ∧ y ∈ V ∧ V ⊆ U),
  ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Tactic: choose V hV using h.isOpen_iff.mp hU₀ y hy.1
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
⊢ U ∈ 𝓝 x ↔ ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
have mp : U ∈ 𝓝 x → ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
mp : U ∈ 𝓝 x → ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
⊢ U ∈ 𝓝 x ↔ ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
have mpr : (∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U) → U ∈ 𝓝 x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
⊢ U ∈ 𝓝 x → ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
have hx : connectedComponent x = {x}
Tactic: have hx : connectedComponent x = {x} :=
        totallyDisconnectedSpace_iff_connectedComponent_singleton.mp ‹_› x
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : connectedComponent x = {x}
⊢ U ∈ 𝓝 x → ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
have hx₁ : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
Tactic: rw [connectedComponent_eq_iInter_isClopen] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
⊢ ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
have mp : ∀ (s : Set X) (hs : IsClopen s) (hs' : x ∈ s)
  (hs'' : (↑(Subtype.mk (p := fun (s : Set X) ↦ IsClopen s ∧ x ∈ s) s sorry) : Set X) ⊆ U),
  ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
Tactic: rsuffices ⟨⟨s, hs, hs'⟩, hs''⟩ : ∃ s : N, s.val ⊆ U
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
mp :
  ∀ (s : Set X) (hs : IsClopen s) (hs' : x ∈ s)
    (hs'' : (↑(Subtype.mk (p := fun (s : Set X) ↦ IsClopen s ∧ x ∈ s) s ⋯) : Set X) ⊆ U),
    ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
⊢ ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
have rsuffices : ∃ (s : N), (↑s : Set X) ⊆ U
Tactic: rsuffices ⟨⟨s, hs, hs'⟩, hs''⟩ : ∃ s : N, s.val ⊆ U
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
⊢ ∃ (s : N), (↑s : Set X) ⊆ U
have this : Nonempty N
Tactic: haveI : Nonempty N := ⟨⟨univ, isClopen_univ, mem_univ x⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
this : Nonempty N
⊢ ∃ (s : N), (↑s : Set X) ⊆ U
have hNcl : ∀ (s : N), IsClosed[inst] (↑s : Set X)
Tactic: have hNcl : ∀ s : N, IsClosed s.val := fun s => s.property.1.1
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst] (↑s : Set X)
⊢ ∃ (s : N), (↑s : Set X) ⊆ U
have hdir : Directed (α := Set X) Superset fun (s : N) ↦ (↑s : Set X)
Tactic: have hdir : Directed Superset fun s : N => s.val := by
        rintro ⟨s, hs, hxs⟩ ⟨t, ht, hxt⟩
        exact ⟨⟨s ∩ t, hs.inter ht, ⟨hxs, hxt⟩⟩, inter_subset_left, inter_subset_right⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst] (↑s : Set X)
hdir : Directed (α := Set X) Superset fun (s : N) ↦ (↑s : Set X)
y : X
y_in : Membership.mem (γ := Set X) (⋂ (s : N), (↑s : Set X)) y
⊢ U ∈ 𝓝 y
have y_in₁ : y = x
Tactic: rw [hx, mem_singleton_iff] at y_in
Cleared hypotheses: y_in
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst] (↑s : Set X)
hdir : Directed (α := Set X) Superset fun (s : N) ↦ (↑s : Set X)
⊢ ∃ (s : N), (↑s : Set X) ⊆ U
have h_nhds : ∀ (y : X), Membership.mem (γ := Set X) (⋂ (s : N), (↑s : Set X)) y → U ∈ 𝓝 y
Tactic: have h_nhds : ∀ y ∈ ⋂ s : N, s.val, U ∈ 𝓝 y := fun y y_in => by
        rw [hx, mem_singleton_iff] at y_in
        rwa [y_in]
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U V : Set X
hUV : V ⊆ U
hxV : x ∈ V
V_op : IsOpen[inst] V
⊢ U ∈ 𝓝 x
have mpr : ∃ t ⊆ U, IsOpen[inst] t ∧ x ∈ t
Tactic: rw [mem_nhds_iff]