awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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ᶜᶜ)
ht₁ : IsClosed[inst] t
⊢ t ⊆ 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
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 : ℝ)
⊢ ∃ (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)

Premises used: Iff.mpr, SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed, HasSubset.Subset.disjoint_compl_left, isClosed_compl_iff
-- 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
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
⊢ u ⊆ vᶜ

Tactic:
rw [← subset_compl_iff_disjoint_right] at hDisjointuv

Premises used: Set.subset_compl_iff_disjoint_right
-- 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
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ᶜ
⊢ closure[inst] u ⊆ vᶜ

Tactic:
have huvc : closure u ⊆ vᶜ := closure_minimal hDisjointuv hvIsOpen.isClosed_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
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
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
⊢ ∃ (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)

Premises used: Iff.mpr, HasSubset.Subset.disjoint_compl_right, SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed, closure_mono, Set.compl_subset_compl, IsCompact.of_isClosed_subset, isClosed_closure, isClosed_compl_iff
-- 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
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] 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

Premises used: Set.subset_compl_iff_disjoint_right, Set.compl_subset_comm
-- 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
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ᶜ
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
⊢ ∃ (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
-- 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
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

Tactic:
⟨u1, hu1, hcu1, ?_, Pc, (Pc.trans hcu1).trans subset_closure⟩

Premises used: subset_closure, HasSubset.Subset.trans, And.intro, Exists.intro
-- 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
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ᶜ
refine : closure[inst] u1 ⊆ u0
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u0 ∧ P c v ∧ P (closure[inst] v) u0

Tactic:
refine ⟨u1, hu1, hcu1, ?_, Pc, (Pc.trans hcu1).trans subset_closure⟩
-- 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
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ᶜ
⊢ closure[inst] u1 ⊆ u0

Tactic:
closure_minimal hu1v1 hv1.isClosed_compl |>.trans hv1u

Premises used: closure_minimal, HasSubset.Subset.trans, IsOpen.isClosed_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
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ᶜ
⊢ closure[inst] u1 ⊆ u0

Tactic:
exact closure_minimal hu1v1 hv1.isClosed_compl |>.trans hv1u

Premises used: closure_minimal, HasSubset.Subset.trans, IsOpen.isClosed_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
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 (α := ℝ) (⇑{ toFun := c.lim (P := P), continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) ⊆ s ∧
    EqOn (β := ℝ) (⇑{ toFun := c.lim (P := P), continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) 1 t ∧
      ∀ (x : X),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
          (({ toFun := c.lim (P := P), continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
⊢ ∃ (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:
use ⟨c.lim, c.continuous_lim⟩
-- 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
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)

Tactic:
⟨?_, ?_, Urysohns.CU.lim_mem_Icc c⟩

Premises used: And.intro, Urysohns.CU.lim_mem_Icc
-- 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
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
h₁ : EqOn (c.lim (P := P)) 1 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)

Tactic:
refine ⟨?_, ?_, Urysohns.CU.lim_mem_Icc c⟩
-- 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
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ᶜ ⋯ ⋯ ⋯ ⋯ ⋯
apply : tsupport (c.lim (P := P)) ⊆ uᶜ
⊢ tsupport (c.lim (P := P)) ⊆ s

Tactic:
apply Subset.trans _ (compl_subset_comm.mp hscompl_subset_u)

Premises used: Set.Subset.trans, Set.compl_subset_comm, Iff.mp
-- 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
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ᶜ ⋯ ⋯ ⋯ ⋯ ⋯
rw : tsupport (c.lim (P := P)) ⊆ closure[inst] uᶜ
⊢ tsupport (c.lim (P := P)) ⊆ uᶜ

Tactic:
rw [← IsClosed.closure_eq (isClosed_compl_iff.mpr huIsOpen)]

Premises used: Iff.mpr, IsClosed.closure_eq, isClosed_compl_iff
-- 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
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 : Function.support (c.lim (P := P)) ⊆ uᶜ
⊢ tsupport (c.lim (P := P)) ⊆ closure[inst] uᶜ

Tactic:
apply closure_mono

Premises used: closure_mono
-- 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
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ᶜ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ Function.support (c.lim (P := P)) ⊆ uᶜ

Tactic:
Disjoint.subset_compl_right (disjoint_of_subset_right subset_closure
      (Disjoint.symm (Urysohns.CU.disjoint_C_support_lim c)))

Premises used: Disjoint.subset_compl_right, subset_closure, Disjoint.symm, Urysohns.CU.disjoint_C_support_lim, Set.disjoint_of_subset_right
-- 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
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ᶜ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ Function.support (c.lim (P := P)) ⊆ uᶜ

Tactic:
exact Disjoint.subset_compl_right (disjoint_of_subset_right subset_closure
      (Disjoint.symm (Urysohns.CU.disjoint_C_support_lim c)))

Premises used: Disjoint.subset_compl_right, subset_closure, Disjoint.symm, Urysohns.CU.disjoint_C_support_lim, Set.disjoint_of_subset_right
-- 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
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
h : x ∉ c.U (P := P)
⊢ c.lim (P := P) x = 1 x

Tactic:
apply Urysohns.CU.lim_of_notMem_U

Premises used: Urysohns.CU.lim_of_notMem_U
-- 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
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
⊢ x ∉ c.U (P := P)

Tactic:
notMem_compl_iff.mpr hx

Premises used: Iff.mpr, Set.Mem, Set.notMem_compl_iff
-- 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
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
⊢ x ∉ c.U (P := P)

Tactic:
exact notMem_compl_iff.mpr hx

Premises used: Iff.mpr, Set.notMem_compl_iff
-- Module: Mathlib.Topology.UrysohnsLemma
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
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 : ℝ)
⊢ ∃ (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

Premises used: exists_open_between_and_isCompact_closure
-- Module: Mathlib.Topology.UrysohnsLemma
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
U : Set X
hU1 : IsOpen[inst] U
hU2 : K ⊆ U
hU3 : closure[inst] U ⊆ V
hU4 : IsCompact (closure[inst] U)
obtain :
  ∀ (f : C(X, ℝ)) (hf1 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ U)
    (hf2 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 (closure[inst] K))
    (hf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)),
    ∃ (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 : ℝ)
⊢ ∃ (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 ⟨f, hf1, hf2, hf3⟩ := exists_tsupport_one_of_isOpen_isClosed hU1 hU4
    isClosed_closure (hK.closure_subset_of_isOpen hU1 hU2)

Premises used: IsCompact.closure_subset_of_isOpen, exists_tsupport_one_of_isOpen_isClosed, isClosed_closure
-- Module: Mathlib.Topology.UrysohnsLemma
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
U : Set X
hU1 : IsOpen[inst] U
hU2 : K ⊆ U
hU3 : closure[inst] U ⊆ V
hU4 : IsCompact (closure[inst] U)
f : C(X, ℝ)
hf1 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ U
hf2 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 (closure[inst] K)
hf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ closure[inst] U

Tactic:
have hfU : tsupport f ⊆ closure U := hf1.trans subset_closure
-- Module: Mathlib.Topology.UrysohnsLemma
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
U : Set X
hU1 : IsOpen[inst] U
hU2 : K ⊆ U
hU3 : closure[inst] U ⊆ V
hU4 : IsCompact (closure[inst] U)
f : C(X, ℝ)
hf1 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ U
hf2 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 (closure[inst] K)
hf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfU : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ 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:
⟨f, hf2.mono subset_closure,
    .of_isClosed_subset hU4 isClosed_closure hfU, hfU.trans hU3, hf3⟩

Premises used: subset_closure, HasSubset.Subset.trans, IsCompact.of_isClosed_subset, And.intro, Exists.intro, isClosed_closure, Set.EqOn.mono
-- Module: Mathlib.Topology.UrysohnsLemma
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
U : Set X
hU1 : IsOpen[inst] U
hU2 : K ⊆ U
hU3 : closure[inst] U ⊆ V
hU4 : IsCompact (closure[inst] U)
f : C(X, ℝ)
hf1 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ U
hf2 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 (closure[inst] K)
hf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfU : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ 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:
exact ⟨f, hf2.mono subset_closure,
    .of_isClosed_subset hU4 isClosed_closure hfU, hfU.trans hU3, hf3⟩
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
x : X
rcases :
  ∀ (k : Set X) (hk : IsCompact k) (k_mem : k ∈ 𝓝 x),
    ∃ (f : C(X, ℝ)),
      HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
        LE.le (α := (a : X) → ℝ) 0 (⇑f : (a : X) → ℝ) ∧ Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
      LE.le (α := (a : X) → ℝ) 0 (⇑f : (a : X) → ℝ) ∧ Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
rcases exists_compact_mem_nhds x with ⟨k, hk, k_mem⟩

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
rcases :
  ∀ (f : C(X, ℝ)) (fk : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 k)
    (f_comp : HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ))
    (hf : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)),
    ∃ (f : C(X, ℝ)),
      HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
        LE.le (α := (a : X) → ℝ) 0 (⇑f : (a : X) → ℝ) ∧ Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
      LE.le (α := (a : X) → ℝ) 0 (⇑f : (a : X) → ℝ) ∧ Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
rcases exists_continuous_one_zero_of_isCompact hk isClosed_empty (disjoint_empty k)
    with ⟨f, fk, -, f_comp, hf⟩

Premises used: exists_continuous_one_zero_of_isCompact, isClosed_empty, Set.disjoint_empty