-- Mathlib/Topology/UrysohnsLemma.lean
theorem exists_continuous_zero_one_of_isClosed [NormalSpace X]
    {s t : Set X} (hs : IsClosed 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:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
P : Set X → Prop := fun x => True
c u : Set X
c_closed : IsClosed c
u_open : IsOpen u
cu : c ⊆ u
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)

Tactic:
rcases normal_exists_closure_subset c_closed u_open cu with ⟨v, v_open, cv, hv⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
P : Set X → Prop := fun x => True
c u : Set X
c_closed : IsClosed c
u_open : IsOpen u
cu : c ⊆ u
v : Set X
v_open : IsOpen v
cv : c ⊆ v
hv : closure v ⊆ u
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
P : Set X → Prop := fun x => True
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
set c : Urysohns.CU P :=
{ C := s
  U := tᶜ
  P_C := trivial
  closed_C := hs
  open_U := ht.isOpen_compl
  subset := disjoint_left.1 hd
  hP := by
    rintro c u c_closed - u_open cu
    rcases normal_exists_closure_subset c_closed u_open cu with ⟨v, v_open, cv, hv⟩
    exact ⟨v, v_open, cv, hv, trivial⟩ }

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
P : Set X → Prop := fun x => True
c : Urysohns.CU P := { C := s, U := tᶜ, P_C := trivial, closed_C := hs, open_U := ⋯, subset := ⋯, hP := ⋯ }
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
P : Set X → Prop := fun x => True
c u : Set X
c_closed : IsClosed c
u_open : IsOpen u
cu : c ⊆ u
v : Set X
v_open : IsOpen v
cv : c ⊆ v
hv : closure v ⊆ u
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)

Tactic:
exact ⟨v, v_open, cv, hv, trivial⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
P : Set X → Prop := fun x => True
c : Urysohns.CU P := { C := s, U := tᶜ, P_C := trivial, closed_C := hs, open_U := ⋯, subset := ⋯, hP := ⋯ }
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
exact ⟨⟨c.lim, c.continuous_lim⟩, c.lim_of_mem_C, fun x hx => c.lim_of_nmem_U _ fun h => h hx,
  c.lim_mem_Icc⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed 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:
let P : Set X → Prop := fun _ ↦ True

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
P : Set X → Prop := fun x => True
⊢ ∃ 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✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
P : Set X → Prop := fun x => True
⊢ ∀ {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_closed - u_open cu

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
P : Set X → Prop := fun x => True
c u : Set X
c_closed : IsClosed c
u_open : IsOpen u
cu : c ⊆ u
⊢ ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)