awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ)
⊢ Continuous[inst, _] g
have apply : ∀ (n : ℕ) (x : X), ‖HMul.hMul (β := ℝ) (u n) ((f n : (a : X) → ℝ) x : ℝ)‖ ≤ u n
Tactic: apply continuous_tsum (fun n ↦ by fun_prop) u_sum (fun n 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 : ℝ)
⊢ s = preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1}
have apply : preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := sorry } : (a : X) → ℝ) {1} ⊆ s
Tactic: apply Subset.antisymm (fun x hx ↦ by simp [g, fs _ hx, 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
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 : ℝ)
⊢ preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1} ⊆ s
have apply : sᶜ ⊆ (preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := sorry } : (a : X) → ℝ) {1})ᶜ
Tactic: apply compl_subset_compl.1
-- 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 : ℝ)
x : X
hx : x ∈ sᶜ
⊢ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1})ᶜ x
have obtain : ∀ (n : ℕ) (hn : x ∉ U n),
  Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := sorry } : (a : X) → ℝ) {1})ᶜ x
Tactic: obtain ⟨n, hn⟩ : ∃ n, x ∉ U n := by simpa [hU] using 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 : ℝ)
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
⊢ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1})ᶜ x
have fnx : Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)
Tactic: have fnx : f n x = 0 := fm _ (by simp [hn])
-- 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 : ℝ)
x : X
hx : x ∈ sᶜ
n : ℕ
hn : x ∉ U n
fnx : Eq (α := ℝ) ((f n : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ g x < 1
have apply : g x < ∑' (i : ℕ), u i
Tactic: apply lt_of_lt_of_le ?_ hu.le
-- 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
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 : ℝ)
⊢ Membership.mem (γ := Set X) (preimage (β := ℝ) (⇑{ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) {1})ᶜ x
have this : 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
-- 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 : ℝ)
x : X
⊢ LE.le (α := ℝ) (({ toFun := g, continuous_toFun := ⋯ } : (a : X) → ℝ) x : ℝ) (1 : ℝ)
have apply : LE.le (α := ℝ) (({ toFun := g, continuous_toFun := sorry } : (a : X) → ℝ) x : ℝ) (∑' (i : ℕ), u i : ℝ)
Tactic: apply le_trans _ hu.le
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
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
⊢ ∃ (f : C(X, ℝ)),
    tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have hscp₁ : IsCompact (closure[inst] sᶜᶜ)
Tactic: rw [← compl_compl s] at hscp
Cleared hypotheses: hscp, ht, hst
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
⊢ ∃ (f : C(X, ℝ)),
    tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have obtain : ∀ (u v : Set X) (huIsOpen : IsOpen[inst] u) (hvIsOpen : IsOpen[inst] v) (hscompl_subset_u : sᶜ ⊆ u)
  (ht_subset_v : t ⊆ v) (hDisjointuv : Disjoint u v),
  ∃ (f : C(X, ℝ)),
    tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: obtain ⟨u, v, huIsOpen, hvIsOpen, hscompl_subset_u, ht_subset_v, hDisjointuv⟩ :=
    SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed (isClosed_compl_iff.mpr hs)
    hscp ht (HasSubset.Subset.disjoint_compl_left hst)
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
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
u v : Set X
huIsOpen : IsOpen[inst] u
hvIsOpen : IsOpen[inst] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : Disjoint u v
⊢ ∃ (f : C(X, ℝ)),
    tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have hDisjointuv₁ : u ⊆ vᶜ
Tactic: rw [← subset_compl_iff_disjoint_right] at hDisjointuv
Cleared hypotheses: hDisjointuv
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
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
u v : Set X
huIsOpen : IsOpen[inst] u
hvIsOpen : IsOpen[inst] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
⊢ ∃ (f : C(X, ℝ)),
    tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have huvc : closure[inst] u ⊆ vᶜ
Tactic: have huvc : closure u ⊆ vᶜ := closure_minimal hDisjointuv hvIsOpen.isClosed_compl
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
u v : Set X
huIsOpen : IsOpen[inst] u
hvIsOpen : IsOpen[inst] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst] u ⊆ vᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed[inst] c
Pc : P c u0
u0IsOpen : IsOpen[inst] u0
csubu0 : c ⊆ u0
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u0 ∧ P c v ∧ P (closure[inst] v) u0
have obtain : ∀ (u1 : Set X) (hu1 : ∃ (V : Set X), IsOpen[inst] u1 ∧ IsOpen[inst] V ∧ c ⊆ u1 ∧ u0ᶜ ⊆ V ∧ Disjoint u1 V),
  ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u0 ∧ P c v ∧ P (closure[inst] v) u0
Tactic: obtain ⟨u1, hu1⟩ := SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed cIsClosed
        (IsCompact.of_isClosed_subset hscp isClosed_closure
        (closure_mono (compl_subset_compl.mpr Pc)))
        (isClosed_compl_iff.mpr u0IsOpen) (HasSubset.Subset.disjoint_compl_right csubu0)
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
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
u v : Set X
huIsOpen : IsOpen[inst] u
hvIsOpen : IsOpen[inst] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst] u ⊆ vᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed[inst] c
Pc : P c u0
u0IsOpen : IsOpen[inst] u0
csubu0 : c ⊆ u0
u1 : Set X
hu1 : ∃ (V : Set X), IsOpen[inst] u1 ∧ IsOpen[inst] V ∧ c ⊆ u1 ∧ u0ᶜ ⊆ V ∧ Disjoint u1 V
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u0 ∧ P c v ∧ P (closure[inst] v) u0
have hu1₁ : ∃ (V : Set X), IsOpen[inst] u1 ∧ IsOpen[inst] V ∧ c ⊆ u1 ∧ Vᶜ ⊆ u0 ∧ u1 ⊆ Vᶜ
Tactic: simp_rw [← subset_compl_iff_disjoint_right, compl_subset_comm (s := u0)] at hu1
Cleared hypotheses: hu1
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
u v : Set X
huIsOpen : IsOpen[inst] u
hvIsOpen : IsOpen[inst] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst] u ⊆ vᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed[inst] c
Pc : P c u0
u0IsOpen : IsOpen[inst] u0
csubu0 : c ⊆ u0
u1 : Set X
hu1 : ∃ (V : Set X), IsOpen[inst] u1 ∧ IsOpen[inst] V ∧ c ⊆ u1 ∧ Vᶜ ⊆ u0 ∧ u1 ⊆ Vᶜ
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u0 ∧ P c v ∧ P (closure[inst] v) u0
have obtain : ∀ (v1 : Set X) (hu1 : IsOpen[inst] u1) (hv1 : IsOpen[inst] v1) (hcu1 : c ⊆ u1) (hv1u : v1ᶜ ⊆ u0) (hu1v1 : u1 ⊆ v1ᶜ),
  ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u0 ∧ P c v ∧ P (closure[inst] v) u0
Tactic: obtain ⟨v1, hu1, hv1, hcu1, hv1u, hu1v1⟩ := hu1
Cleared hypotheses: hu1
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
u v : Set X
huIsOpen : IsOpen[inst] u
hvIsOpen : IsOpen[inst] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst] u ⊆ vᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed[inst] c
Pc : P c u0
u0IsOpen : IsOpen[inst] u0
csubu0 : c ⊆ u0
u1 v1 : Set X
hu1 : IsOpen[inst] u1
hv1 : IsOpen[inst] v1
hcu1 : c ⊆ u1
hv1u : v1ᶜ ⊆ u0
hu1v1 : u1 ⊆ v1ᶜ
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u0 ∧ P c v ∧ P (closure[inst] v) u0
have refine : closure[inst] u1 ⊆ u0
Tactic: refine ⟨u1, hu1, hcu1, ?_, Pc, (Pc.trans hcu1).trans subset_closure⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
u v : Set X
huIsOpen : IsOpen[inst] u
hvIsOpen : IsOpen[inst] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst] u ⊆ vᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ sᶜ ⊆ C
c : Urysohns.CU P := Urysohns.CU.mk (P := P) (closure[inst] u) tᶜ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ ∃ (f : C(X, ℝ)),
    tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have h : tsupport (α := ℝ) (⇑{ toFun := c.lim (P := P), continuous_toFun := sorry : C(X, ℝ) } : (a : X) → ℝ) ⊆ s ∧
  EqOn (β := ℝ) (⇑{ toFun := c.lim (P := P), continuous_toFun := sorry : C(X, ℝ) } : (a : X) → ℝ) 1 t ∧
    ∀ (x : X),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
        (({ toFun := c.lim (P := P), continuous_toFun := sorry : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
Tactic: use ⟨c.lim, c.continuous_lim⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
u v : Set X
huIsOpen : IsOpen[inst] u
hvIsOpen : IsOpen[inst] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst] u ⊆ vᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ sᶜ ⊆ C
c : Urysohns.CU P := Urysohns.CU.mk (P := P) (closure[inst] u) tᶜ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ tsupport (c.lim (P := P)) ⊆ s ∧
    EqOn (c.lim (P := P)) 1 t ∧ ∀ (x : X), Membership.mem (γ := Set ℝ) (Icc 0 1) (c.lim (P := P) x)
have h : tsupport (c.lim (P := P)) ⊆ s
Tactic: refine ⟨?_, ?_, Urysohns.CU.lim_mem_Icc c⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
u v : Set X
huIsOpen : IsOpen[inst] u
hvIsOpen : IsOpen[inst] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst] u ⊆ vᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ sᶜ ⊆ C
c : Urysohns.CU P := Urysohns.CU.mk (P := P) (closure[inst] u) tᶜ ⋯ ⋯ ⋯ ⋯ ⋯
h : tsupport (c.lim (P := P)) ⊆ s
⊢ tsupport (c.lim (P := P)) ⊆ s ∧
    EqOn (c.lim (P := P)) 1 t ∧ ∀ (x : X), Membership.mem (γ := Set ℝ) (Icc 0 1) (c.lim (P := P) x)
have h₁ : EqOn (c.lim (P := P)) 1 t
Tactic: refine ⟨?_, ?_, Urysohns.CU.lim_mem_Icc c⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
u v : Set X
huIsOpen : IsOpen[inst] u
hvIsOpen : IsOpen[inst] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst] u ⊆ vᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ sᶜ ⊆ C
c : Urysohns.CU P := Urysohns.CU.mk (P := P) (closure[inst] u) tᶜ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ tsupport (c.lim (P := P)) ⊆ s
have apply : tsupport (c.lim (P := P)) ⊆ uᶜ
Tactic: apply Subset.trans _ (compl_subset_comm.mp hscompl_subset_u)
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
u v : Set X
huIsOpen : IsOpen[inst] u
hvIsOpen : IsOpen[inst] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst] u ⊆ vᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ sᶜ ⊆ C
c : Urysohns.CU P := Urysohns.CU.mk (P := P) (closure[inst] u) tᶜ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ tsupport (c.lim (P := P)) ⊆ uᶜ
have rw : tsupport (c.lim (P := P)) ⊆ closure[inst] uᶜ
Tactic: rw [← IsClosed.closure_eq (isClosed_compl_iff.mpr huIsOpen)]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
u v : Set X
huIsOpen : IsOpen[inst] u
hvIsOpen : IsOpen[inst] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst] u ⊆ vᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ sᶜ ⊆ C
c : Urysohns.CU P := Urysohns.CU.mk (P := P) (closure[inst] u) tᶜ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ tsupport (c.lim (P := P)) ⊆ closure[inst] uᶜ
have h : Function.support (c.lim (P := P)) ⊆ uᶜ
Tactic: apply closure_mono
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
u v : Set X
huIsOpen : IsOpen[inst] u
hvIsOpen : IsOpen[inst] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst] u ⊆ vᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ sᶜ ⊆ C
c : Urysohns.CU P := Urysohns.CU.mk (P := P) (closure[inst] u) tᶜ ⋯ ⋯ ⋯ ⋯ ⋯
x : X
hx : x ∈ t
⊢ c.lim (P := P) x = 1 x
have h : x ∉ c.U (P := P)
Tactic: apply Urysohns.CU.lim_of_notMem_U
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
K V : Set X
hK : IsCompact K
hV : IsOpen[inst] V
hKV : K ⊆ V
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K ∧
      IsCompact (X := X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) ∧
        tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have obtain : ∀ (U : Set X) (hU1 : IsOpen[inst] U) (hU2 : K ⊆ U) (hU3 : closure[inst] U ⊆ V) (hU4 : IsCompact (closure[inst] U)),
  ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K ∧
      IsCompact (X := X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) ∧
        tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: obtain ⟨U, hU1, hU2, hU3, hU4⟩ := exists_open_between_and_isCompact_closure hK hV hKV