awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)

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
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)
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 : ℝ)
⊢ ∃ (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
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)
n : ℕ
⊢ LT.lt (α := ℝ) 0 ((fun (n : ℕ) ↦ 1 / 2 / HPow.hPow (α := ℝ) 2 n) n)

Tactic:
positivity
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)
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 : ℝ)
⊢ ∃ (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⟩
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℕ
⊢ mᶜ ⊆ (U n ∩ interior m)ᶜ

Tactic:
simpa using inter_subset_right.trans interior_subset

Premises used: interior_subset, HasSubset.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℕ
⊢ mᶜ ⊆ (U n ∩ interior m)ᶜ

Tactic:
have : mᶜ ⊆ (U n ∩ interior m)ᶜ := by
        simpa using inter_subset_right.trans interior_subset
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℕ
this : mᶜ ⊆ (U n ∩ interior m)ᶜ
⊢ Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
fm n (this hx)
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℕ
this : mᶜ ⊆ (U n ∩ interior m)ᶜ
⊢ Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
exact fm n (this hx)
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)

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)
-- Module: Mathlib.Topology.UrysohnsLemma
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ᶜ
B : ∀ (n : ℕ), Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ g x = 0 x

Tactic:
simp [g, B]
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)
⊢ 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]
-- Module: Mathlib.Topology.UrysohnsLemma
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ᶜ
⊢ ∀ (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
-- Module: Mathlib.Topology.UrysohnsLemma
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
⊢ ∀ (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
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)

Tactic:
⟨⟨g, ?_⟩, ?_, hgmc.mono (subset_compl_comm.mp mt), ?_, fun x ↦ ⟨?_, ?_⟩⟩

Premises used: ContinuousMap.mk, Set.subset_compl_comm, And.intro, Exists.intro, Iff.mp, Set.EqOn.mono
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)
refine_5 : ∀ (x : X), LE.le (α := ℝ) (({ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) 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 : ℝ)

Tactic:
refine ⟨⟨g, ?_⟩, ?_, hgmc.mono (subset_compl_comm.mp mt), ?_, fun x ↦ ⟨?_, ?_⟩⟩
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)
n : ℕ
⊢ Continuous[inst, _] fun (x : X) ↦ HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)
apply : ∀ (n : ℕ) (x : X), ‖HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)‖ ≤ u n
⊢ Continuous[inst, _] g

Tactic:
apply continuous_tsum (fun n ↦ by fun_prop) u_sum (fun n x ↦ ?_)

Premises used: continuous_tsum
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)
n : ℕ
x : X
⊢ ‖HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)‖ ≤ u n

Tactic:
simpa [abs_of_nonneg, (u_pos n).le, (f_range n x).1] using I n x

Premises used: LT.lt.le, And.left, abs_of_nonneg
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)
x : X
hx : x ∈ s
⊢ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1}) x

Tactic:
simp [g, fs _ hx, hu]