-- Mathlib/Topology/UrysohnsLemma.lean
theorem exists_continuous_nonneg_pos [RegularSpace X] [LocallyCompactSpace X] (x : X) :
    ∃ f : C(X, ℝ), HasCompactSupport f ∧ 0 ≤ (f : X → ℝ) ∧ f x ≠ 0

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (⇑f) 1 k
f_comp : HasCompactSupport ⇑f
hf : ∀ (x : X), f x ∈ Icc 0 1
⊢ f x ≠ 0

Tactic:
have := fk (mem_of_mem_nhds k_mem)

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (⇑f) 1 k
f_comp : HasCompactSupport ⇑f
hf : ∀ (x : X), f x ∈ Icc 0 1
this : f x = 1 x
⊢ f x ≠ 0

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (⇑f) 1 k
f_comp : HasCompactSupport ⇑f
hf : ∀ (x : X), f x ∈ Icc 0 1
⊢ ∃ f, HasCompactSupport ⇑f ∧ 0 ≤ ⇑f ∧ f x ≠ 0

Tactic:
refine ⟨f, f_comp, fun x ↦ (hf x).1, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (⇑f) 1 k
f_comp : HasCompactSupport ⇑f
hf : ∀ (x : X), f x ∈ Icc 0 1
⊢ f x ≠ 0

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (⇑f) 1 k
f_comp : HasCompactSupport ⇑f
hf : ∀ (x : X), f x ∈ Icc 0 1
this : f x = 1
⊢ f x ≠ 0

Tactic:
simp [this]

Result:
no goals

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
⊢ ∃ f, HasCompactSupport ⇑f ∧ 0 ≤ ⇑f ∧ f x ≠ 0

Tactic:
rcases exists_compact_mem_nhds x with ⟨k, hk, k_mem⟩

Result:
case intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
⊢ ∃ f, HasCompactSupport ⇑f ∧ 0 ≤ ⇑f ∧ f x ≠ 0

Proof state:
case intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
⊢ ∃ f, HasCompactSupport ⇑f ∧ 0 ≤ ⇑f ∧ f x ≠ 0

Tactic:
rcases exists_continuous_one_zero_of_isCompact hk isClosed_empty (disjoint_empty k)
  with ⟨f, fk, -, f_comp, hf⟩

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (⇑f) 1 k
f_comp : HasCompactSupport ⇑f
hf : ∀ (x : X), f x ∈ Icc 0 1
⊢ ∃ f, HasCompactSupport ⇑f ∧ 0 ≤ ⇑f ∧ f x ≠ 0

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (⇑f) 1 k
f_comp : HasCompactSupport ⇑f
hf : ∀ (x : X), f x ∈ Icc 0 1
this : f x = 1 x
⊢ f x ≠ 0

Tactic:
simp only [ContinuousMap.coe_mk, Pi.one_apply] at this

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (⇑f) 1 k
f_comp : HasCompactSupport ⇑f
hf : ∀ (x : X), f x ∈ Icc 0 1
this : f x = 1
⊢ f x ≠ 0