-- Mathlib/Topology/UrysohnsLemma.lean
/-- A variation of Urysohn's lemma. In a `T2Space X`, for a closed set `t` and a relatively
compact open set `s` such that `t ⊆ s`, there is a continuous function `f` supported in `s`,
`f x = 1` on `t` and `0 ≤ f x ≤ 1`. -/
lemma exists_tsupport_one_of_isOpen_isClosed [T2Space X] {s t : Set X}
    (hs : IsOpen s) (hscp : IsCompact (closure s)) (ht : IsClosed t) (hst : t ⊆ s) :
    ∃ f : C(X, ℝ), tsupport f ⊆ s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
⊢ ∃ f, tsupport ⇑f ⊆ s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
set c : Urysohns.CU P :=
{ C := closure u
  U := tᶜ
  P_C := hscompl_subset_u.trans subset_closure
  closed_C := isClosed_closure
  open_U := ht.isOpen_compl
  subset := subset_compl_comm.mp
    (Subset.trans ht_subset_v (subset_compl_comm.mp huvc))
  hP := by
    intro c u0 cIsClosed Pc u0IsOpen csubu0
    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)
    simp_rw [← subset_compl_iff_disjoint_right, compl_subset_comm (s := u0)] at hu1
    obtain ⟨v1, hu1, hv1, hcu1, hv1u, hu1v1⟩ := hu1
    refine ⟨u1, hu1, hcu1, ?_, (Pc.trans hcu1).trans subset_closure⟩
    exact closure_minimal hu1v1 hv1.isClosed_compl |>.trans hv1u }

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
c : Urysohns.CU P := { C := closure u, U := tᶜ, P_C := ⋯, closed_C := ⋯, open_U := ⋯, subset := ⋯, hP := ⋯ }
⊢ ∃ f, tsupport ⇑f ⊆ s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Proof state:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed c
Pc : P c
u0IsOpen : IsOpen u0
csubu0 : c ⊆ u0
u1 : Set X
hu1 : ∃ V, IsOpen u1 ∧ IsOpen V ∧ c ⊆ u1 ∧ u0ᶜ ⊆ V ∧ Disjoint u1 V
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u0 ∧ P (closure v)

Tactic:
simp_rw [← subset_compl_iff_disjoint_right, compl_subset_comm (s := u0)] at hu1

Result:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed c
Pc : P c
u0IsOpen : IsOpen u0
csubu0 : c ⊆ u0
u1 : Set X
hu1 : ∃ V, IsOpen u1 ∧ IsOpen V ∧ c ⊆ u1 ∧ Vᶜ ⊆ u0 ∧ u1 ⊆ Vᶜ
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u0 ∧ P (closure v)

Proof state:
case h.refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
c : Urysohns.CU P := { C := closure u, U := tᶜ, P_C := ⋯, closed_C := ⋯, open_U := ⋯, subset := ⋯, hP := ⋯ }
x : X
hx : x ∈ t
⊢ c.lim x = 1 x

Tactic:
apply Urysohns.CU.lim_of_nmem_U

Result:
case h.refine_2.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
c : Urysohns.CU P := { C := closure u, U := tᶜ, P_C := ⋯, closed_C := ⋯, open_U := ⋯, subset := ⋯, hP := ⋯ }
x : X
hx : x ∈ t
⊢ x ∉ c.U

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed c
Pc : P c
u0IsOpen : IsOpen u0
csubu0 : c ⊆ u0
u1 v1 : Set X
hu1 : IsOpen u1
hv1 : IsOpen v1
hcu1 : c ⊆ u1
hv1u : v1ᶜ ⊆ u0
hu1v1 : u1 ⊆ v1ᶜ
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u0 ∧ P (closure v)

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

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
c u0 : Set X
cIsClosed : IsClosed c
Pc : P c
u0IsOpen : IsOpen u0
csubu0 : c ⊆ u0
u1 v1 : Set X
hu1 : IsOpen u1
hv1 : IsOpen v1
hcu1 : c ⊆ u1
hv1u : v1ᶜ ⊆ u0
hu1v1 : u1 ⊆ v1ᶜ
⊢ closure u1 ⊆ u0

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
c : Urysohns.CU P := { C := closure u, U := tᶜ, P_C := ⋯, closed_C := ⋯, open_U := ⋯, subset := ⋯, hP := ⋯ }
⊢ ∃ f, tsupport ⇑f ⊆ s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
use ⟨c.lim, c.continuous_lim⟩

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
c : Urysohns.CU P := { C := closure u, U := tᶜ, P_C := ⋯, closed_C := ⋯, open_U := ⋯, subset := ⋯, hP := ⋯ }
⊢ tsupport ⇑{ toFun := c.lim, continuous_toFun := ⋯ } ⊆ s ∧
    EqOn (⇑{ toFun := c.lim, continuous_toFun := ⋯ }) 1 t ∧
      ∀ (x : X), { toFun := c.lim, continuous_toFun := ⋯ } x ∈ Icc 0 1

Proof state:
case h.refine_2.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
c : Urysohns.CU P := { C := closure u, U := tᶜ, P_C := ⋯, closed_C := ⋯, open_U := ⋯, subset := ⋯, hP := ⋯ }
x : X
hx : x ∈ t
⊢ x ∉ c.U

Tactic:
exact not_mem_compl_iff.mpr hx

Result:
no goals