awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
⊢ Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
    (({ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
have this : 0 ≤ f x ∧ f x ≤ 1
Tactic: have : 0 ≤ f x ∧ f x ≤ 1 := by simpa using h'f x
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have rcases : ∀ (U : ℕ → Set X) (U_open : ∀ (n : ℕ), IsOpen[inst] (U n)) (hU : s = ⋂ (n : ℕ), U n),
  ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: rcases h's.eq_iInter_nat with ⟨U, U_open, hU⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have obtain : ∀ (m : Set X) (m_comp : IsCompact m) (sm : s ⊆ interior m) (mt : m ⊆ tᶜ),
  ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: obtain ⟨m, m_comp, -, sm, mt⟩ : ∃ m, IsCompact m ∧ IsClosed m ∧ s ⊆ interior m ∧ m ⊆ tᶜ :=
    exists_compact_closed_between hs ht.isOpen_compl hd.symm.subset_compl_left
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
n : ℕ
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have apply : Disjoint s (U n ∩ interior m)ᶜ
Tactic: apply exists_continuous_one_zero_of_isCompact hs
      ((U_open n).inter isOpen_interior).isClosed_compl
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
n : ℕ
⊢ Disjoint s (U n ∩ interior m)ᶜ
have rw : s ⊆ U n ∩ interior m
Tactic: rw [disjoint_compl_right_iff_subset]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have A : ∀ (n : ℕ),
  ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: have A n : ∃ f : C(X, ℝ), EqOn f 1 s ∧ EqOn f 0 (U n ∩ interior m)ᶜ ∧ HasCompactSupport f
      ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
    apply exists_continuous_one_zero_of_isCompact hs
      ((U_open n).inter isOpen_interior).isClosed_compl
    rw [disjoint_compl_right_iff_subset]
    exact subset_inter ((hU.subset.trans (iInter_subset U n))) sm
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
A :
  ∀ (n : ℕ),
    ∃ (f : C(X, ℝ)),
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
        EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ ∧
          HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
            ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have choose : ∀ (f : (n : ℕ) → C(X, ℝ)) (fs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 s)
  (fm : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ)
  (_hf : ∀ (n : ℕ), HasCompactSupport (α := X) (β := ℝ) (⇑(f n) : (a : X) → ℝ))
  (f_range : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)),
  ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: choose f fs fm _hf f_range using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : (n : ℕ) → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 s
fm : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport (α := X) (β := ℝ) (⇑(f n) : (a : X) → ℝ)
f_range : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have obtain : ∀ (u : ℕ → ℝ) (u_pos : ∀ (i : ℕ), 0 < u i) (u_sum : Summable u) (hu : Eq (α := ℝ) (∑' (i : ℕ), u i) 1),
  ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: obtain ⟨u, u_pos, u_sum, hu⟩ : ∃ (u : ℕ → ℝ), (∀ i, 0 < u i) ∧ Summable u ∧ ∑' i, u i = 1 :=
    ⟨fun n ↦ 1/2/2^n, fun n ↦ by positivity, summable_geometric_two' 1, tsum_geometric_two' 1⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : (n : ℕ) → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 s
fm : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport (α := X) (β := ℝ) (⇑(f n) : (a : X) → ℝ)
f_range : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : Eq (α := ℝ) (∑' (i : ℕ), u i) 1
g : X → ℝ := fun (x : X) ↦ ∑' (n : ℕ), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
x : X
hx : x ∈ mᶜ
n : ℕ
⊢ Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)
have this : mᶜ ⊆ (U n ∩ interior m)ᶜ
Tactic: have : mᶜ ⊆ (U n ∩ interior m)ᶜ := by
        simpa using inter_subset_right.trans interior_subset
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : (n : ℕ) → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 s
fm : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport (α := X) (β := ℝ) (⇑(f n) : (a : X) → ℝ)
f_range : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : Eq (α := ℝ) (∑' (i : ℕ), u i) 1
g : X → ℝ := fun (x : X) ↦ ∑' (n : ℕ), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
x : X
hx : x ∈ mᶜ
⊢ g x = 0 x
have B : ∀ (n : ℕ), Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)
Tactic: have B n : f n x = 0 := by
      have : mᶜ ⊆ (U n ∩ interior m)ᶜ := by
        simpa using inter_subset_right.trans interior_subset
      exact fm n (this hx)
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : (n : ℕ) → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 s
fm : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport (α := X) (β := ℝ) (⇑(f n) : (a : X) → ℝ)
f_range : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : Eq (α := ℝ) (∑' (i : ℕ), u i) 1
g : X → ℝ := fun (x : X) ↦ ∑' (n : ℕ), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have hgmc : EqOn g 0 mᶜ
Tactic: have hgmc : EqOn g 0 mᶜ := by
    intro x hx
    have B n : f n x = 0 := by
      have : mᶜ ⊆ (U n ∩ interior m)ᶜ := by
        simpa using inter_subset_right.trans interior_subset
      exact fm n (this hx)
    simp [g, B]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : (n : ℕ) → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 s
fm : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport (α := X) (β := ℝ) (⇑(f n) : (a : X) → ℝ)
f_range : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : Eq (α := ℝ) (∑' (i : ℕ), u i) 1
g : X → ℝ := fun (x : X) ↦ ∑' (n : ℕ), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
hgmc : EqOn g 0 mᶜ
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have I : ∀ (n : ℕ) (x : X), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ) ≤ u n
Tactic: have I n x : u n * f n x ≤ u n := mul_le_of_le_one_right (u_pos n).le (f_range n x).2
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : (n : ℕ) → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 s
fm : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport (α := X) (β := ℝ) (⇑(f n) : (a : X) → ℝ)
f_range : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : Eq (α := ℝ) (∑' (i : ℕ), u i) 1
g : X → ℝ := fun (x : X) ↦ ∑' (n : ℕ), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ) ≤ u n
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have S : ∀ (x : X), Summable (α := ℝ) fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
Tactic: have S x : Summable (fun n ↦ u n * f n x) := Summable.of_nonneg_of_le
      (fun n ↦ mul_nonneg (u_pos n).le (f_range n x).1) (fun n ↦ I n x) u_sum
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : (n : ℕ) → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 s
fm : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport (α := X) (β := ℝ) (⇑(f n) : (a : X) → ℝ)
f_range : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : Eq (α := ℝ) (∑' (i : ℕ), u i) 1
g : X → ℝ := fun (x : X) ↦ ∑' (n : ℕ), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ) ≤ u n
S : ∀ (x : X), Summable (α := ℝ) fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have refine_1 : Continuous[inst, _] g
Tactic: refine ⟨⟨g, ?_⟩, ?_, hgmc.mono (subset_compl_comm.mp mt), ?_, fun x ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : (n : ℕ) → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 s
fm : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport (α := X) (β := ℝ) (⇑(f n) : (a : X) → ℝ)
f_range : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : Eq (α := ℝ) (∑' (i : ℕ), u i) 1
g : X → ℝ := fun (x : X) ↦ ∑' (n : ℕ), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ) ≤ u n
S : ∀ (x : X), Summable (α := ℝ) fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
refine_1 : Continuous[inst, _] g
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have refine_2 : s = preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := sorry } : (a : X) → ℝ) {1}
Tactic: refine ⟨⟨g, ?_⟩, ?_, hgmc.mono (subset_compl_comm.mp mt), ?_, fun x ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : (n : ℕ) → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 s
fm : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport (α := X) (β := ℝ) (⇑(f n) : (a : X) → ℝ)
f_range : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : Eq (α := ℝ) (∑' (i : ℕ), u i) 1
g : X → ℝ := fun (x : X) ↦ ∑' (n : ℕ), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ) ≤ u n
S : ∀ (x : X), Summable (α := ℝ) fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
refine_1 : Continuous[inst, _] g
refine_2 : s = preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1}
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have refine_3 : HasCompactSupport (α := X) (β := ℝ) (⇑{ toFun := g, continuous_toFun := sorry } : (a : X) → ℝ)
Tactic: refine ⟨⟨g, ?_⟩, ?_, hgmc.mono (subset_compl_comm.mp mt), ?_, fun x ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : (n : ℕ) → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 s
fm : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport (α := X) (β := ℝ) (⇑(f n) : (a : X) → ℝ)
f_range : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : Eq (α := ℝ) (∑' (i : ℕ), u i) 1
g : X → ℝ := fun (x : X) ↦ ∑' (n : ℕ), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ) ≤ u n
S : ∀ (x : X), Summable (α := ℝ) fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
refine_1 : Continuous[inst, _] g
refine_2 : s = preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1}
refine_3 : HasCompactSupport (α := X) (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ)
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have refine_4 : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) (({ toFun := g, continuous_toFun := sorry } : (a : X) → ℝ) x : ℝ)
Tactic: refine ⟨⟨g, ?_⟩, ?_, hgmc.mono (subset_compl_comm.mp mt), ?_, fun x ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst] (U n)
hU : s = ⋂ (n : ℕ), U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : (n : ℕ) → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 1 s
fm : ∀ (n : ℕ), EqOn (β := ℝ) (⇑(f n) : (a : X) → ℝ) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport (α := X) (β := ℝ) (⇑(f n) : (a : X) → ℝ)
f_range : ∀ (n : ℕ) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f n : (a : X) → ℝ) x : ℝ)
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : Eq (α := ℝ) (∑' (i : ℕ), u i) 1
g : X → ℝ := fun (x : X) ↦ ∑' (n : ℕ), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ) ≤ u n
S : ∀ (x : X), Summable (α := ℝ) fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)
refine_1 : Continuous[inst, _] g
refine_2 : s = preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1}
refine_3 : HasCompactSupport (α := X) (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ)
refine_4 : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) (({ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have refine_5 : ∀ (x : X), LE.le (α := ℝ) (({ toFun := g, continuous_toFun := sorry } : (a : X) → ℝ) x : ℝ) (1 : ℝ)
Tactic: refine ⟨⟨g, ?_⟩, ?_, hgmc.mono (subset_compl_comm.mp mt), ?_, fun x ↦ ⟨?_, ?_⟩⟩