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

Tactic:
rw [← subset_compl_iff_disjoint_right] at hDjsjointuv

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

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 := ⋯ }
⊢ tsupport c.lim ⊆ s ∧ EqOn c.lim 1 t ∧ ∀ (x : X), c.lim x ∈ Icc 0 1

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

Result:
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

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 := ⋯ }
⊢ EqOn c.lim 1 t

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 ⊆ uᶜ

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

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

Tactic:
have huvc : closure u ⊆ vᶜ := closure_minimal hDjsjointuv hvIsOpen.isClosed_compl

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

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 := ⋯ }
⊢ 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

Tactic:
simp only [ContinuousMap.coe_mk]

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 c.lim ⊆ s ∧ EqOn c.lim 1 t ∧ ∀ (x : X), c.lim 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 ∧ Vᶜ ⊆ u0 ∧ u1 ⊆ Vᶜ
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u0 ∧ P (closure v)

Tactic:
obtain ⟨v1, hu1, hv1, hcu1, hv1u, hu1v1⟩ := hu1

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