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 t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
⊢ SeparatedNhds s t
have obtain : ∀ (f : C(X, ℝ)) (hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0})
  (hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)), SeparatedNhds s t
Tactic: obtain ⟨f, hf, hfr⟩ := h s hs
-- 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 t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ SeparatedNhds s t
have obtain : ∀ (g : C(X, ℝ)) (hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0})
  (hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)), SeparatedNhds s t
Tactic: obtain ⟨g, hg, hgr⟩ := h t ht
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
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 t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
⊢ SeparatedNhds s t
have hsn : SeparatedNhds (X := ℝ) {0} {1}
Tactic: have hsn : SeparatedNhds {(0 : ℝ)} {1} :=
          SeparatedNhds.of_finite (finite_singleton _) (finite_singleton _)
          (disjoint_singleton.2 zero_ne_one)
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
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 t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
x : X
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
have h₁ : ∀ (s : Set X),
  IsClosed[inst] s →
    ∃ (f : C(X, ℝ)),
      s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)} ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: simp_all only [preimage, mem_singleton_iff]
Cleared hypotheses: h, hs, ht, hst, hf, hfr, hg, hgr, hsn
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
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 t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
x : X
h₁ :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
have hs₁ : IsClosed[inst] {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
Tactic: simp_all only [preimage, mem_singleton_iff]
Cleared hypotheses: h, hs, ht, hst, hf, hfr, hg, hgr, hsn
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
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 t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
x : X
h₁ :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs₁ : IsClosed[inst] {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
have ht₁ : IsClosed[inst] {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
Tactic: simp_all only [preimage, mem_singleton_iff]
Cleared hypotheses: h, hs, ht, hst, hf, hfr, hg, hgr, hsn
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
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 t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
x : X
h₁ :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs₁ : IsClosed[inst] {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
ht₁ : IsClosed[inst] {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
have hst₁ : Disjoint.{u_1} (α := Set X) {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
  {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
Tactic: simp_all only [preimage, mem_singleton_iff]
Cleared hypotheses: h, hs, ht, hst, hf, hfr, hg, hgr, hsn
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
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 t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
x : X
h₁ :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs₁ : IsClosed[inst] {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
ht₁ : IsClosed[inst] {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hst₁ :
  Disjoint.{u_1} (α := Set X) {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
    {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
have hf₁ : s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
Tactic: simp_all only [preimage, mem_singleton_iff]
Cleared hypotheses: h, hs, ht, hst, hf, hfr, hg, hgr, hsn
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
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 t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
x : X
h₁ :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs₁ : IsClosed[inst] {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
ht₁ : IsClosed[inst] {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hst₁ :
  Disjoint.{u_1} (α := Set X) {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
    {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hf₁ : s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hfr₁ : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
have hg₁ : t = {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
Tactic: simp_all only [preimage, mem_singleton_iff]
Cleared hypotheses: h, hs, ht, hst, hf, hfr, hg, hgr, hsn
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
f g : C(X, ℝ)
x : X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsClosed[inst] {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
ht : IsClosed[inst] {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hst :
  Disjoint.{u_1} (α := Set X) {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
    {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hf : s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hg : t = {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
have pos : ∀ (hfx : Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)),
  HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
Tactic: by_cases! hfx : f x = 0
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
f g : C(X, ℝ)
x : X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsClosed[inst] {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
ht : IsClosed[inst] {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hst :
  Disjoint.{u_1} (α := Set X) {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
    {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hf : s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hg : t = {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
pos :
  ∀ (hfx : Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)),
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
have neg : ∀ (hfx : Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)),
  HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
Tactic: by_cases! hfx : f x = 0
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
f g : C(X, ℝ)
x : X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsClosed[inst] {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
ht : IsClosed[inst] {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hst :
  Disjoint.{u_1} (α := Set X) {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
    {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hf : s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hg : t = {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
hfx : Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
have neg : LE.le (α := ℝ) (0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) →
  HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
Tactic: positivity [(hgr x).1, (hfr x).1]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
f g : C(X, ℝ)
x : X
h :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsClosed[inst] {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
ht : IsClosed[inst] {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hst :
  Disjoint.{u_1} (α := Set X) {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
    {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hf : s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hg : t = {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
hfx : Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
neg neg₁ neg₂ :
  LE.le (α := ℝ) (0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) →
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
have neg₃ : LE.le (α := ℝ) (0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) →
  LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ) →
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
Tactic: positivity [(hgr x).1, (hfr x).1]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
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 t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
⊢ SeparatedNhds s t
have hfg : ∀ (x : X), HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
Tactic: have hfg (x : X) : f x + g x ≠ 0 := by
          simp_all only [preimage, mem_singleton_iff]
          by_cases! hfx : f x = 0
          · simpa [hfx] using hst.notMem_of_mem_left hfx
          · positivity [(hgr x).1, (hfr x).1]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
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 t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
hfg : ∀ (x : X), HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
⊢ SeparatedNhds s t
have hp : s =
  preimage (β := ℝ)
    (fun (a : X) ↦
      HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
    {0}
Tactic: have hp : s = (fun a => f a / (f a + g a)) ⁻¹' {0} := by simp_all [preimage]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
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 t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
hfg : ∀ (x : X), HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
hp :
  s =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {0}
⊢ SeparatedNhds s t
have this : t =
  preimage (β := ℝ)
    (fun (a : X) ↦
      HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
    {1}
Tactic: have : t = (fun a => f a / (f a + g a)) ⁻¹' {1} := by simp_all [preimage, div_eq_one_iff_eq]
-- 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 t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
g : C(X, ℝ)
hg : t = preimage (β := ℝ) (⇑g : (a : X) → ℝ) {0}
hgr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
hsn : SeparatedNhds (X := ℝ) {0} {1}
hfg : ∀ (x : X), HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0
hp :
  s =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {0}
this :
  t =
    preimage (β := ℝ)
      (fun (a : X) ↦
        HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
      {1}
⊢ SeparatedNhds s t
have rw : SeparatedNhds.{u_1} (X := X)
  (preimage (β := ℝ)
    (fun (a : X) ↦
      HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
    {0})
  (preimage (β := ℝ)
    (fun (a : X) ↦
      HDiv.hDiv (α := ℝ) ((f : (a : X) → ℝ) a : ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) a : ℝ) ((g : (a : X) → ℝ) a : ℝ)))
    {1})
Tactic: rw [hp, this]
-- 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
⊢ IsGδ s
have pos : ∀ (hse : s = ∅), IsGδ s
Tactic: by_cases! hse : s = ∅
-- 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
pos : ∀ (hse : s = ∅), IsGδ s
⊢ IsGδ s
have neg : ∀ (hse : s.Nonempty), IsGδ s
Tactic: by_cases! hse : s = ∅
-- 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
⊢ IsGδ s
have neg : ∀ (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
Tactic: obtain ⟨f, hf, hfr⟩ := h s hs