awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.NotNormal (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s d : Set X
hs : IsClosed s
inst_2 : DiscreteTopology.{u} (↑s : Type u)
hd : Dense d
h_closed : ∀ (t : Set X) (ht : t ∈ 𝒫 s), IsClosed t
U V : (t : (↑(𝒫 s) : Type u)) → Set X
hU : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (U t)
hV : ∀ (t : (↑(𝒫 s) : Type u)), IsOpen (V t)
hUs : ∀ (t : (↑(𝒫 s) : Type u)), (↑t : Set X) ⊆ U t
hVs : ∀ (t : (↑(𝒫 s) : Type u)), s \ (↑t : Set X) ⊆ V t
hUV : ∀ (t : (↑(𝒫 s) : Type u)), Disjoint (U t) (V t)
hUd : ∀ {t₁ t₂ : (↑(𝒫 s) : Type u)} (h : U t₁ ∩ d = U t₂ ∩ d), (↑t₁ : Set X) ⊆ (↑t₂ : Set X)
h_inj : Injective (β := Set X) fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d
⊢ (range fun (x : (↑(𝒫 s) : Type u)) ↦ U x ∩ d) ⊆ 𝒫 d
have h : ∀ (y : (↑(𝒫 s) : Type u)), U y ∩ d ∈ 𝒫 d
Tactic: rw [range_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst] s
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have obtain : ∀ (U : ℕ → Set X) (ho : ∀ (n : ℕ), IsOpen[inst] (U n)) (hu : s = ⋂ (n : ℕ), U n),
  ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: obtain ⟨U, ho, hu⟩ := isGδ_iff_eq_iInter_nat.1 hs.isGδ
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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
n : ℕ
⊢ Disjoint s (U n)ᶜ
have a : s ⊆ U n
Tactic: apply HasSubset.Subset.disjoint_compl_right
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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
n : ℕ
⊢ s ⊆ U n
have a : ⋂ (n : ℕ), U n ⊆ U n
Tactic: grw [hu, iInter_subset]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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
n : ℕ
a : ⋂ (n : ℕ), U n ⊆ U n
⊢ s ⊆ U n
have a₁ : U n ⊆ U n
Tactic: grw [hu, iInter_subset]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
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
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
Tactic: have (n : ℕ) : Disjoint s (U n)ᶜ := by
      apply HasSubset.Subset.disjoint_compl_right
      grw [hu, iInter_subset]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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 : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have choose : ∀ (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 : ℝ)),
  ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: choose f hfs hfu hfr using fun n =>
      exists_continuous_zero_one_of_isClosed hs (ho n).isClosed_compl (this n)
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
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 : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have hsb : ∀ (x : X) (n : ℕ),
  ‖HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)‖ ≤ 1 / 2 / HPow.hPow (α := ℝ) 2 n
Tactic: have hsb (x : X) (n : ℕ) : ‖(f n) x * (1 / 2 / 2 ^ n)‖ ≤ 1 / 2 / 2 ^ n := by
      simp [abs_of_nonneg (hfr n x).1, (hfr n x).2]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (hypothesis)
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
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have hsx : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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 : ℝ)
have refine_1 : s = preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}
Tactic: refine ⟨h, ?_, fun x => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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}
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have refine_2 : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((h : (a : X) → ℝ) x : ℝ)
Tactic: refine ⟨h, ?_, fun x => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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 : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have refine_3 : ∀ (x : X), LE.le (α := ℝ) ((h : (a : X) → ℝ) x : ℝ) (1 : ℝ)
Tactic: refine ⟨h, ?_, fun x => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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 := ⋯ }
⊢ s = preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}
have refine_1 : ∀ (x : X), x ∈ s ↔ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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
have refine_1 : ∀ (hp : x ∈ s), Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}) x
Tactic: refine ⟨fun hp => ?_, fun hp => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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
⊢ x ∈ s ↔ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}) x
have refine_1₁ : ∀ (hp : Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}) x), x ∈ s
Tactic: refine ⟨fun hp => ?_, fun hp => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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
⊢ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑h : (a : X) → ℝ) {0}) x
have refine_1 : ∀ (n : ℕ), Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)
Tactic: suffices ∀ n, f n x = 0 from by simp [h, this]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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
⊢ x ∈ s
have 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 := sorry } :
        (a : X) → ℝ)
      {0}
Tactic: contrapose h
Cleared hypotheses: h, hp
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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
⊢ ¬Eq (α := ℝ) (∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n)) 0
have refine_1 : LT.lt (α := ℝ) 0 (∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n))
Tactic: apply ne_of_gt
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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
⊢ LT.lt (α := ℝ) 0 (∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n))
have refine_1 : ∀ (i : ℕ) (hi : x ∈ (U i)ᶜ),
  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)
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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
⊢ 0 ≤ HMul.hMul (α := ℝ) ((f j : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 j)
have positivity : LE.le (α := ℝ) (0 : ℝ) ((f j : (a : X) → ℝ) x : ℝ) →
  0 ≤ HMul.hMul (α := ℝ) ((f j : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 j)
Tactic: positivity [(hfr j x).1]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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)ᶜ
⊢ LT.lt (α := ℝ) 0 (∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n))
have _ : 0 < 1 / 2 / HPow.hPow (α := ℝ) 2 i
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]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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
⊢ LT.lt (α := ℝ) 0 (∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n))
have _₁ : 1 / 2 / HPow.hPow (α := ℝ) 2 i = HMul.hMul (α := ℝ) ((f i : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 i)
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]
-- Lean 4 proof step from Mathlib.Topology.Separation.PerfectlyNormal (goal)
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 (α := ℝ) ((h : (a : X) → ℝ) x : ℝ) (1 : ℝ)
have _ : Eq (α := ℝ) ((h : (a : X) → ℝ) x : ℝ)
  (∑' (n : ℕ), HMul.hMul (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (1 / 2 / HPow.hPow (α := ℝ) 2 n) : ℝ)
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