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ᶜ
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 : preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1} ⊆ s
⊢ s = preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1}

Tactic:
apply Subset.antisymm (fun x hx ↦ by simp [g, fs _ hx, hu]) ?_

Premises used: Set.Subset.antisymm
-- 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 : sᶜ ⊆ (preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1})ᶜ
⊢ preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1} ⊆ s

Tactic:
apply compl_subset_compl.1

Premises used: Set.compl_subset_compl, Iff.mp
-- 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ᶜ
⊢ ∃ (n : ℕ), x ∉ U n

Tactic:
simpa [hU] using 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 : ℝ)
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ᶜ
obtain :
  ∀ (n : ℕ) (hn : x ∉ U n),
    Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1})ᶜ x
⊢ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1})ᶜ x

Tactic:
obtain ⟨n, hn⟩ : ∃ n, x ∉ U n := by simpa [hU] using 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 : ℝ)
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ᶜ
n : ℕ
hn : x ∉ U n
⊢ x ∈ (U n ∩ interior m)ᶜ

Tactic:
simp [hn]
-- 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ᶜ
n : ℕ
hn : x ∉ U n
⊢ Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
have fnx : f n x = 0 := fm _ (by simp [hn])
-- 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ᶜ
n : ℕ
hn : x ∉ U n
fnx : Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)
apply : g x < ∑' (i : ℕ), u i
⊢ g x < 1

Tactic:
apply lt_of_lt_of_le ?_ hu.le

Premises used: Eq.le, lt_of_lt_of_le
-- 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ᶜ
n : ℕ
hn : x ∉ U n
fnx : Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ) < u n

Tactic:
simp [fnx, u_pos n]
-- 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ᶜ
n : ℕ
hn : x ∉ U n
fnx : Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ g x < ∑' (i : ℕ), u i

Tactic:
exact (S x).tsum_lt_tsum (i := n) (fun i ↦ I i x) (by simp [fnx, u_pos n]) u_sum

Premises used: Summable.tsum_lt_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 : ℝ)
x : X
hx : x ∈ sᶜ
n : ℕ
hn : x ∉ U n
fnx : Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ g x < 1

Tactic:
have : g x < 1 := by
      apply lt_of_lt_of_le ?_ hu.le
      exact (S x).tsum_lt_tsum (i := n) (fun i ↦ I i x) (by simp [fnx, u_pos n]) 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 : ℝ)
x : X
hx : x ∈ sᶜ
n : ℕ
hn : x ∉ U n
fnx : Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)
this : g x < 1
⊢ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1})ᶜ x

Tactic:
simpa using this.ne

Premises used: LT.lt.ne
-- 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 : ℝ)
⊢ HasCompactSupport (α := X) (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ)

Tactic:
HasCompactSupport.of_support_subset_isCompact m_comp
      (Function.support_subset_iff'.mpr hgmc)

Premises used: Iff.mpr, HasCompactSupport.of_support_subset_isCompact, Function.support_subset_iff'
-- 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 : ℝ)
⊢ HasCompactSupport (α := X) (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ)

Tactic:
exact HasCompactSupport.of_support_subset_isCompact m_comp
      (Function.support_subset_iff'.mpr hgmc)

Premises used: Iff.mpr, HasCompactSupport.of_support_subset_isCompact, Function.support_subset_iff'
-- 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
⊢ LE.le (α := ℝ) (0 : ℝ) (({ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) x : ℝ)

Tactic:
tsum_nonneg (fun n ↦ mul_nonneg (u_pos n).le (f_range n x).1)

Premises used: mul_nonneg, LT.lt.le, And.left, tsum, tsum_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
⊢ LE.le (α := ℝ) (0 : ℝ) (({ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) x : ℝ)

Tactic:
exact tsum_nonneg (fun n ↦ mul_nonneg (u_pos n).le (f_range n x).1)

Premises used: mul_nonneg, LT.lt.le, And.left, tsum_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
apply : LE.le (α := ℝ) (({ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) x : ℝ) (∑' (i : ℕ), u i : ℝ)
⊢ LE.le (α := ℝ) (({ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
apply le_trans _ hu.le

Premises used: Eq.le, le_trans
-- 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
⊢ LE.le (α := ℝ) (({ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) x : ℝ) (∑' (i : ℕ), u i : ℝ)

Tactic:
(S x).tsum_le_tsum (fun n ↦ I n x) u_sum

Premises used: Summable.tsum_le_tsum, 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 : ℝ)
x : X
⊢ LE.le (α := ℝ) (({ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) x : ℝ) (∑' (i : ℕ), u i : ℝ)

Tactic:
exact (S x).tsum_le_tsum (fun n ↦ I n x) u_sum

Premises used: Summable.tsum_le_tsum
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s t : Set X
hs : IsOpen[inst] s
hscp : IsCompact (closure[inst] s)
ht : IsClosed[inst] t
hst : t ⊆ s
⊢ IsCompact (closure[inst] sᶜᶜ)

Tactic:
rw [← compl_compl s] at hscp

Premises used: compl_compl
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s t : Set X
hs : IsOpen[inst] s
hscp : IsCompact (closure[inst] s)
ht : IsClosed[inst] t
hst : t ⊆ s
hscp₁ : IsCompact (closure[inst] sᶜᶜ)
⊢ IsClosed[inst] t

Tactic:
rw [← compl_compl s] at hscp

Premises used: compl_compl