-- Mathlib/Topology/UrysohnsLemma.lean
theorem exists_continuous_zero_one_of_isCompact [RegularSpace X] [LocallyCompactSpace X]
    {s t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hd : Disjoint s t) :
    ∃ f : C(X, ℝ), EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
let P : Set X → Prop := IsCompact

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Prop := IsCompact
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Prop := IsCompact
⊢ ∀ {c u : Set X}, IsClosed c → P c → IsOpen u → c ⊆ u → ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)

Tactic:
rintro c u - c_comp u_open cu

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Prop := IsCompact
c u : Set X
c_comp : P c
u_open : IsOpen u
cu : c ⊆ u
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k✝ : Set X
k_comp✝ : IsCompact k✝
k_closed✝ : IsClosed k✝
sk : s ⊆ interior k✝
kt : k✝ ⊆ tᶜ
P : Set X → Prop := IsCompact
c u : Set X
c_comp : P c
u_open : IsOpen u
cu : c ⊆ u
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
ck : c ⊆ interior k
ku : k ⊆ u
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)

Tactic:
have A : closure (interior k) ⊆ k :=
  (IsClosed.closure_subset_iff k_closed).2 interior_subset

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k✝ : Set X
k_comp✝ : IsCompact k✝
k_closed✝ : IsClosed k✝
sk : s ⊆ interior k✝
kt : k✝ ⊆ tᶜ
P : Set X → Prop := IsCompact
c u : Set X
c_comp : P c
u_open : IsOpen u
cu : c ⊆ u
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
ck : c ⊆ interior k
ku : k ⊆ u
A : closure (interior k) ⊆ k
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Prop := IsCompact
c u : Set X
c_comp : P c
u_open : IsOpen u
cu : c ⊆ u
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)

Tactic:
rcases exists_compact_closed_between c_comp u_open cu with ⟨k, k_comp, k_closed, ck, ku⟩

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k✝ : Set X
k_comp✝ : IsCompact k✝
k_closed✝ : IsClosed k✝
sk : s ⊆ interior k✝
kt : k✝ ⊆ tᶜ
P : Set X → Prop := IsCompact
c u : Set X
c_comp : P c
u_open : IsOpen u
cu : c ⊆ u
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
ck : c ⊆ interior k
ku : k ⊆ u
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Prop := IsCompact
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
set c : Urysohns.CU P :=
{ C := k
  U := tᶜ
  P_C := k_comp
  closed_C := k_closed
  open_U := ht.isOpen_compl
  subset := kt
  hP := by
    rintro c u - c_comp u_open cu
    rcases exists_compact_closed_between c_comp u_open cu with ⟨k, k_comp, k_closed, ck, ku⟩
    have A : closure (interior k) ⊆ k :=
      (IsClosed.closure_subset_iff k_closed).2 interior_subset
    refine ⟨interior k, isOpen_interior, ck, A.trans ku,
      k_comp.of_isClosed_subset isClosed_closure A⟩ }

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Prop := IsCompact
c : Urysohns.CU P := { C := k, U := tᶜ, P_C := k_comp, closed_C := k_closed, open_U := ⋯, subset := kt, hP := ⋯ }
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Prop := IsCompact
c : Urysohns.CU P := { C := k, U := tᶜ, P_C := k_comp, closed_C := k_closed, open_U := ⋯, subset := kt, hP := ⋯ }
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
exact ⟨⟨c.lim, c.continuous_lim⟩, fun x hx ↦ c.lim_of_mem_C _ (sk.trans interior_subset hx),
  fun x hx => c.lim_of_nmem_U _ fun h => h hx, c.lim_mem_Icc⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k✝ : Set X
k_comp✝ : IsCompact k✝
k_closed✝ : IsClosed k✝
sk : s ⊆ interior k✝
kt : k✝ ⊆ tᶜ
P : Set X → Prop := IsCompact
c u : Set X
c_comp : P c
u_open : IsOpen u
cu : c ⊆ u
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
ck : c ⊆ interior k
ku : k ⊆ u
A : closure (interior k) ⊆ k
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)

Tactic:
refine ⟨interior k, isOpen_interior, ck, A.trans ku,
  k_comp.of_isClosed_subset isClosed_closure A⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

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

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1