-- 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:
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
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u0 ∧ P (closure v)

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)

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 ∧ u0ᶜ ⊆ V ∧ Disjoint u1 V
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u0 ∧ P (closure v)

Proof state:
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
⊢ ∃ f, tsupport ⇑f ⊆ s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
rw [← compl_compl s] at hscp

Result:
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
⊢ ∃ f, tsupport ⇑f ⊆ s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Proof state:
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 c.lim ⊆ closure uᶜ

Tactic:
apply closure_mono

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 := ⋯ }
⊢ Function.support c.lim ⊆ 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ᶜ
⊢ closure u1 ⊆ u0

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

Result:
no goals

Proof state:
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
⊢ ∃ f, tsupport ⇑f ⊆ s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
obtain ⟨u, v, huIsOpen, hvIsOpen, hscompl_subset_u, ht_subset_v, hDjsjointuv⟩ :=
  SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed (isClosed_compl_iff.mpr hs)
  hscp ht (HasSubset.Subset.disjoint_compl_left hst)

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 : Disjoint u v
⊢ ∃ f, tsupport ⇑f ⊆ s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Proof state:
case h.refine_1
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 c.lim ⊆ s

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

Result:
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 c.lim ⊆ uᶜ

Proof state:
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 u : Set X}, IsClosed c → P c → IsOpen u → c ⊆ u → ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)

Tactic:
intro c u0 cIsClosed Pc u0IsOpen csubu0

Result:
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
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u0 ∧ P (closure v)

Proof state:
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 := ⋯ }
⊢ Function.support c.lim ⊆ uᶜ

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

Result:
no goals