awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hu : s = ⋂ (n : ℕ), U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
f : (n : ℕ) → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 s
hfu : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
hsb :
  ∀ (x : X) (n : ℕ),
    ‖HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)‖ ≤ 1 / 2 / HPow.hPow (α := ℝ) 2 n
hsx :
  ∀ (x : X),
    Summable (α := ℝ) fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)
h : C(X, ℝ) :=
  { toFun := fun (x : X) ↦ ∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n),
    continuous_toFun := ⋯ }
x : X
n : ℕ
⊢ HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n) ≤ 1 / 2 / HPow.hPow (α := ℝ) 2 n

Tactic:
simp [(hfr n x).2]

Premises used: And.right
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hu : s = ⋂ (n : ℕ), U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
f : (n : ℕ) → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 s
hfu : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
hsb :
  ∀ (x : X) (n : ℕ),
    ‖HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)‖ ≤ 1 / 2 / HPow.hPow (α := ℝ) 2 n
hsx :
  ∀ (x : X),
    Summable (α := ℝ) fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)
h : C(X, ℝ) :=
  { toFun := fun (x : X) ↦ ∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n),
    continuous_toFun := ⋯ }
x : X
⊢ Eq (α := ℝ) (∑' (n : ℕ), 1 / 2 / HPow.hPow (α := ℝ) 2 n) 1

Tactic:
tsum_geometric_two' 1

Premises used: tsum_geometric_two', OfNat.ofNat
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hu : s = ⋂ (n : ℕ), U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
f : (n : ℕ) → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 s
hfu : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
hsb :
  ∀ (x : X) (n : ℕ),
    ‖HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)‖ ≤ 1 / 2 / HPow.hPow (α := ℝ) 2 n
hsx :
  ∀ (x : X),
    Summable (α := ℝ) fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)
h : C(X, ℝ) :=
  { toFun := fun (x : X) ↦ ∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n),
    continuous_toFun := ⋯ }
x : X
_ :
  Eq (α := ℝ) ((h : (a : X) → ℝ) x : ℝ)
    (∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n) : ℝ)
⊢ LE.le (α := ℝ) ((h : (a : X) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
calc
      _ = ∑' n, f n x * (1 / 2 / 2 ^ n) := by simp [h]
      _ ≤ ∑' n, 1 / 2 / 2 ^ n :=
        (hsx x).tsum_le_tsum (fun n => by simp [(hfr n x).2]) (summable_geometric_two' 1)
      _ = _ := tsum_geometric_two' 1

Premises used: Summable.tsum_le_tsum, tsum_geometric_two', summable_geometric_two', OfNat.ofNat
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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
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
⊢ SeparatedNhds s t

Tactic:
obtain ⟨f, hf, hfr⟩ := h s hs
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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 : ℝ)
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
⊢ SeparatedNhds s t

Tactic:
obtain ⟨g, hg, hgr⟩ := h t ht
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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 (X := ℝ) {0} {1}

Tactic:
have hsn : SeparatedNhds {(0 : ℝ)} {1} :=
          SeparatedNhds.of_finite (finite_singleton _) (finite_singleton _)
          (disjoint_singleton.2 zero_ne_one)
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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
⊢ ∀ (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]

Premises used: Set.mem_singleton_iff, Set.preimage
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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 : ℝ)
⊢ IsClosed[inst] {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}

Tactic:
simp_all only [preimage, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, Set.preimage
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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 : ℝ)}
⊢ IsClosed[inst] {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}

Tactic:
simp_all only [preimage, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, Set.preimage
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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 : ℝ)}
⊢ 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]

Premises used: Set.mem_singleton_iff, Set.preimage
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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 : ℝ)}
⊢ s = {x : X | Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)}

Tactic:
simp_all only [preimage, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, Set.preimage
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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 : ℝ)}
⊢ ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
simp_all only [preimage, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, Set.preimage
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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 : ℝ)
⊢ t = {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}

Tactic:
simp_all only [preimage, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, Set.preimage
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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 : ℝ)
hg₁ : t = {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
⊢ ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)

Tactic:
simp_all only [preimage, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, Set.preimage
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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 : ℝ)
hg₁ : t = {x : X | Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
hgr₁ : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : X) → ℝ) x : ℝ)
⊢ SeparatedNhds (X := ℝ) {0} {1}

Tactic:
simp_all only [preimage, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, Set.preimage
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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
neg :
  ∀ (hfx : Ne (α := ℝ) ((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

Tactic:
by_cases! hfx : f x = 0

Premises used: DFunLike.coe
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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 : Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0

Tactic:
simpa [hfx] using hst.notMem_of_mem_left hfx

Premises used: Disjoint.notMem_of_mem_left
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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
neg₃ 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
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) ≠ 0

Tactic:
positivity [(hgr x).1, (hfr x).1]

Premises used: And.left
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
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

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]