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
ht : IsClosed[inst] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 s
hgt : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 1 t
hicc : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (1 : ℝ)
x : X
hx : x ∈ s
h : Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((1 - g : (a : X) → ℝ) x : ℝ) (1 x : ℝ)

Tactic:
simp only [ContinuousMap.sub_apply, ContinuousMap.one_apply, Pi.one_apply, sub_eq_self]

Premises used: Pi.one_apply, ContinuousMap.one_apply, sub_eq_self, ContinuousMap.sub_apply
-- 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
ht : IsClosed[inst] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 s
hgt : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 1 t
hicc : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (1 : ℝ)
x : X
hx : x ∈ s
⊢ Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
hgs 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
ht : IsClosed[inst] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 s
hgt : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 1 t
hicc : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (1 : ℝ)
x : X
hx : x ∈ s
⊢ Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
exact hgs 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
ht : IsClosed[inst] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 s
hgt : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 1 t
hicc : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (1 : ℝ)
x : X
⊢ Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((1 - g : (a : X) → ℝ) x : ℝ)

Tactic:
simpa [and_comm] using hicc x

Premises used: and_comm
-- 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
ht : IsClosed[inst] t
hd : Disjoint s t
obtain :
  ∀ (k : Set X) (k_comp : IsCompact k) (k_closed : IsClosed[inst] k) (sk : s ⊆ interior k) (kt : k ⊆ tᶜ),
    ∃ (f : C(X, ℝ)),
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
        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, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
      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 ⟨k, k_comp, k_closed, sk, kt⟩ : ∃ k, IsCompact k ∧ IsClosed k ∧ s ⊆ interior k ∧ k ⊆ tᶜ :=
    exists_compact_closed_between hs ht.isOpen_compl hd.symm.subset_compl_left

Premises used: IsClosed.isOpen_compl, exists_compact_closed_between, Disjoint.symm, Disjoint.subset_compl_left
-- 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
rcases :
  ∀ (f : X → ℝ) (hf : Continuous[inst, _] f)
    (hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s)
    (hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ)
    (h'f :
      ∀ (x : X),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
          (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)),
    ∃ (f : C(X, ℝ)),
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
        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, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
rcases exists_continuous_zero_one_of_isCompact hs isOpen_interior.isClosed_compl
    (disjoint_compl_right_iff_subset.mpr sk) with ⟨⟨f, hf⟩, hfs, hft, h'f⟩

Premises used: Iff.mpr, isOpen_interior, Set.disjoint_compl_right_iff_subset, IsOpen.isClosed_compl, exists_continuous_zero_one_of_isCompact
-- 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
⊢ t ⊆ (interior k)ᶜ

Tactic:
have A : t ⊆ (interior k)ᶜ := subset_compl_comm.mpr (interior_subset.trans kt)
-- 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
⊢ Continuous[inst, _] fun (x : X) ↦ 1 - f 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∈ s
⊢ Eq (α := ℝ) (({ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) x : ℝ) (1 x : ℝ)

Tactic:
simpa using hfs 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∈ t
⊢ Eq (α := ℝ) (({ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) x : ℝ) (0 x : ℝ)

Tactic:
simpa [sub_eq_zero] using (hft (A hx)).symm

Premises used: sub_eq_zero, Eq.symm
-- 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
refine_1 :
  HasCompactSupport (α := X) (β := ℝ)
    (⇑{ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ)
refine_2 :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
      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 ⟨⟨fun x ↦ 1 - f x, by fun_prop⟩, fun x hx ↦ by simpa using hfs hx,
    fun x hx ↦ by simpa [sub_eq_zero] using (hft (A hx)).symm, ?_, 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
apply :
  ∀ (x : X) (hx : x ∉ k),
    Eq (α := ℝ) (({ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ HasCompactSupport (α := X) (β := ℝ)
    (⇑{ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ)

Tactic:
apply HasCompactSupport.intro' k_comp k_closed (fun x hx ↦ ?_)

Premises used: HasCompactSupport.intro'
-- 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∉ k
simp : 1 = f x
⊢ Eq (α := ℝ) (({ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
simp only [ContinuousMap.coe_mk, sub_eq_zero]

Premises used: sub_eq_zero, ContinuousMap.coe_mk
-- 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∉ k
apply : x ∈ (interior k)ᶜ
⊢ 1 = f x

Tactic:
apply (hft _).symm

Premises used: Eq.symm
-- 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∉ k
contrapose : ∀ (hx : x ∉ (interior k)ᶜ), x ∈ k
⊢ x ∈ (interior k)ᶜ

Tactic:
contrapose 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∉ (interior k)ᶜ
⊢ x ∈ interior k

Tactic:
simp only [mem_compl_iff, not_not] at hx

Premises used: Classical.not_not, Set.mem_compl_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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∈ interior k
⊢ x ∈ k

Tactic:
interior_subset hx

Premises used: 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∈ interior k
⊢ x ∈ k

Tactic:
exact interior_subset hx

Premises used: 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
⊢ 0 ≤ f x ∧ f x ≤ 1

Tactic:
simpa using h'f 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
⊢ 0 ≤ f x ∧ f x ≤ 1

Tactic:
have : 0 ≤ f x ∧ f x ≤ 1 := by simpa using h'f 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
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
this : 0 ≤ f x ∧ f x ≤ 1
⊢ Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
    (({ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)

Tactic:
simp [this]
-- 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
rcases :
  ∀ (U : ℕ → Set X) (U_open : ∀ (n : ℕ), IsOpen[inst] (U n)) (hU : s = ⋂ (n : ℕ), U n),
    ∃ (f : C(X, ℝ)),
      s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
        EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
          HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
            ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
rcases h's.eq_iInter_nat with ⟨U, U_open, hU⟩

Premises used: IsGδ.eq_iInter_nat
-- 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), IsCompact m ∧ IsClosed[inst] m ∧ s ⊆ interior m ∧ m ⊆ tᶜ

Tactic:
exists_compact_closed_between hs ht.isOpen_compl hd.symm.subset_compl_left

Premises used: IsClosed.isOpen_compl, exists_compact_closed_between, Disjoint.symm, Disjoint.subset_compl_left
-- 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
obtain :
  ∀ (m : Set X) (m_comp : IsCompact m) (sm : s ⊆ interior m) (mt : m ⊆ tᶜ),
    ∃ (f : C(X, ℝ)),
      s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
        EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
          HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
            ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {1} ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
obtain ⟨m, m_comp, -, sm, mt⟩ : ∃ m, IsCompact m ∧ IsClosed m ∧ s ⊆ interior m ∧ m ⊆ tᶜ :=
    exists_compact_closed_between hs ht.isOpen_compl hd.symm.subset_compl_left

Premises used: IsClosed.isOpen_compl, exists_compact_closed_between, mt, Disjoint.symm, Disjoint.subset_compl_left
-- 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 : ℕ
apply : Disjoint s (U n ∩ interior m)ᶜ
⊢ ∃ (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:
apply exists_continuous_one_zero_of_isCompact hs
      ((U_open n).inter isOpen_interior).isClosed_compl

Premises used: isOpen_interior, exists_continuous_one_zero_of_isCompact, IsOpen.isClosed_compl, IsOpen.inter
-- 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 : ℕ
rw : s ⊆ U n ∩ interior m
⊢ Disjoint s (U n ∩ interior m)ᶜ

Tactic:
rw [disjoint_compl_right_iff_subset]

Premises used: Set.disjoint_compl_right_iff_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ᶜ
n : ℕ
⊢ s ⊆ U n ∩ interior m

Tactic:
subset_inter ((hU.subset.trans (iInter_subset U n))) sm

Premises used: HasSubset.Subset.trans, Eq.subset, Set.subset_inter, Set.iInter_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ᶜ
n : ℕ
⊢ s ⊆ U n ∩ interior m

Tactic:
exact subset_inter ((hU.subset.trans (iInter_subset U n))) sm

Premises used: HasSubset.Subset.trans, Eq.subset, Set.subset_inter, Set.iInter_subset