awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h : 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
⊢ ∀ (x : X),
    Summable (α := ℝ) fun (n : ℕ) ↦ HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)

Tactic:
have hsx (x : X) : Summable fun n => f n x * (1 / 2 / 2 ^ n) :=
      (summable_geometric_two' 1).of_norm_bounded fun n => hsb x n
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h : 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)
n : ℕ
⊢ Continuous[inst, _] fun (x : X) ↦ HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)

Tactic:
fun_prop
-- 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 := ⋯ }
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
⟨h, ?_, fun x => ⟨?_, ?_⟩⟩

Premises used: And.intro, Exists.intro
-- 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 := ⋯ }
refine_1 : s = preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}
refine_2 : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((h : (a : X) → ℝ) x : ℝ)
refine_3 : ∀ (x : X), LE.le (α := ℝ) ((h : (a : X) → ℝ) x : ℝ) (1 : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
refine ⟨h, ?_, fun x => ⟨?_, ?_⟩⟩
-- 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 := ⋯ }
refine_1 : ∀ (x : X), x ∈ s ↔ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}) x
⊢ s = preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}

Tactic:
ext x
-- 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
⊢ x ∈ s ↔ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}) x

Tactic:
⟨fun hp => ?_, fun hp => ?_⟩

Premises used: Iff.intro
-- 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
refine_1 : ∀ (hp : x ∈ s), Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}) x
refine_1₁ : ∀ (hp : Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}) x), x ∈ s
⊢ x ∈ s ↔ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}) x

Tactic:
refine ⟨fun hp => ?_, fun hp => ?_⟩
-- 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_1 : ∀ (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
hp : x ∈ s
this : ∀ (n : ℕ), Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}) x

Tactic:
simp [h, this]
-- 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
hp : x ∈ s
refine_1 : ∀ (n : ℕ), Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}) x

Tactic:
suffices ∀ n, f n x = 0 from by simp [h, this]
-- 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
hp : x ∈ s
⊢ ∀ (n : ℕ), Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
fun n => hfs n hp
-- 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
hp : x ∈ s
⊢ ∀ (n : ℕ), Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
exact fun n => hfs n hp
-- 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
hp : Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}) x
refine_1 :
  ∀ (h : x ∉ s),
    x ∉
      preimage (β := ℝ)
        (⇑{
              toFun := fun (x : X) ↦
                ∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n),
              continuous_toFun := ⋯ } :
          (a : X) → ℝ)
        {0}
⊢ x ∈ s

Tactic:
contrapose h
-- 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)
x : X
h : x ∉ s
refine_1 :
  LT.lt (α := ℝ) 0 (∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n))
⊢ ¬Eq (α := ℝ) (∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)) 0

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- 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)
x : X
h : x ∉ s
refine_1 :
  ∀ (i : ℕ) (hi : x ∈ (U i)ᶜ),
    LT.lt (α := ℝ) 0 (∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n))
⊢ LT.lt (α := ℝ) 0 (∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n))

Tactic:
obtain ⟨i, hi⟩ := mem_iUnion.1 <| compl_iInter _ ▸ mem_compl (hu ▸ h)

Premises used: Set.mem_iUnion, Iff.mp
-- 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)
x : X
h : x ∉ s
i : ℕ
hi : x ∈ (U i)ᶜ
⊢ 0 < 1 / 2 / HPow.hPow (α := ℝ) 2 i

Tactic:
positivity
-- 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)
x : X
h : x ∉ s
i : ℕ
hi : x ∈ (U i)ᶜ
⊢ 1 / 2 / HPow.hPow (α := ℝ) 2 i = HMul.hMul (α := ℝ) ((f i : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 i)

Tactic:
simp [hfu i hi]
-- 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)
x : X
h : x ∉ s
i : ℕ
hi : x ∈ (U i)ᶜ
j : ℕ
hj : j ≠ i
positivity positivity₁ positivity₂ positivity₃ :
  LE.le (α := ℝ) (0 : ℝ) ((f j : (a : X) → ℝ) x : ℝ) →
    0 ≤ HMul.hMul (α := ℝ) ((f j : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 j)
⊢ 0 ≤ HMul.hMul (α := ℝ) ((f j : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 j)

Tactic:
positivity [(hfr j x).1]

Premises used: And.left
-- 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)
x : X
h : x ∉ s
i : ℕ
hi : x ∈ (U i)ᶜ
_ : 0 < 1 / 2 / HPow.hPow (α := ℝ) 2 i
_₁ : 1 / 2 / HPow.hPow (α := ℝ) 2 i = HMul.hMul (α := ℝ) ((f i : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 i)
⊢ LT.lt (α := ℝ) 0 (∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n))

Tactic:
calc
        _ < 1 / 2 / 2 ^ i := by positivity
        _ = f i x * (1 / 2 / 2 ^ i) := by simp [hfu i hi]
        _ ≤ _ := (hsx x).le_tsum i fun j hj => by positivity [(hfr j x).1]

Premises used: HDiv.hDiv, HPow.hPow, Summable.le_tsum, OfNat.ofNat, DFunLike.coe
-- 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 : ℕ
⊢ 0 ≤ HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)

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

Premises used: And.left
-- 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
⊢ LE.le (α := ℝ) (0 : ℝ) ((h : (a : X) → ℝ) x : ℝ)

Tactic:
exact tsum_nonneg fun n => by simp [(hfr n x).1]

Premises used: tsum_nonneg
-- 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) : ℝ)

Tactic:
simp [h]