-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem idealOfSet_ofIdeal_eq_closure (I : Ideal C(X, 𝕜)) :
    idealOfSet 𝕜 (setOfIdeal I) = I.closure

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
this : ∃ g, (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I ∧ (∀ (x : X), g x ≤ 1) ∧ Set.EqOn (⇑g) 1 t
⊢ ∃ b ∈ ↑I, nndist f b < ε

Tactic:
obtain ⟨g, hgI, hg, hgt⟩ := this

Result:
case intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
⊢ ∃ b ∈ ↑I, nndist f b < ε

Proof state:
case neg
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
x : X
hx : x ∉ t
⊢ ‖f x - f x * ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ < ε

Tactic:
refine lt_of_le_of_lt ?_ (half_lt_self hε)

Result:
case neg
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
x : X
hx : x ∉ t
⊢ ‖f x - f x * ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ ≤ ε / 2

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ
hε : ε > 0
⊢ ∃ b ∈ ↑I, dist f b < ε

Tactic:
lift ε to ℝ≥0 using hε.lt.le

Result:
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : ↑ε > 0
⊢ ∃ b ∈ ↑I, dist f b < ↑ε

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g' : C(X, ℝ≥0)
hI' : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I
hgt' : ∀ x ∈ t, 0 < g' x
c : ℝ≥0
hc : c > 0
hgc' : ∀ y ∈ t, c ≤ g' y
⊢ ∃ g, (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I ∧ (∀ (x : X), g x ≤ 1) ∧ Set.EqOn (⇑g) 1 t

Tactic:
obtain ⟨g, hg, hgc⟩ := exists_mul_le_one_eqOn_ge g' hc

Result:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g' : C(X, ℝ≥0)
hI' : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I
hgt' : ∀ x ∈ t, 0 < g' x
c : ℝ≥0
hc : c > 0
hgc' : ∀ y ∈ t, c ≤ g' y
g : C(X, ℝ≥0)
hg : ∀ (x : X), (g * g') x ≤ 1
hgc : Set.EqOn (⇑(g * g')) 1 {x | c ≤ g' x}
⊢ ∃ g, (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I ∧ (∀ (x : X), g x ≤ 1) ∧ Set.EqOn (⇑g) 1 t

Proof state:
case refine_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
hx : x ∈ t
⊢ ∃ t_1 ∈ nhdsWithin x t, ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ t_1, 0 < g' x

Tactic:
replace hx := htI.subset_compl_right hx

Result:
case refine_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
hx : x ∈ (setOfIdeal I)ᶜᶜ
⊢ ∃ t_1 ∈ nhdsWithin x t, ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ t_1, 0 < g' x

Proof state:
case h.e'_5.h
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
a✝ : X
⊢ ((↑(algebraMapCLM ℝ≥0 𝕜)).comp 0) a✝ = 0 a✝

Tactic:
simp only [comp_apply, zero_apply, ContinuousMap.coe_coe, map_zero]

Result:
no goals

Proof state:
case intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
x : X
⊢ ‖(f - f * (↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ < ε

Tactic:
simp only [coe_sub, coe_mul, Pi.sub_apply, Pi.mul_apply]

Result:
case intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
x : X
⊢ ‖f x - f x * ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ < ε

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
x : X
hx : x ∉ t
this : ‖(1 - (↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ ≤ 1
⊢ ‖f x - f x * ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ = ‖f x * (1 - (↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊

Tactic:
simp only [mul_sub, coe_sub, coe_one, Pi.sub_apply, Pi.one_apply, mul_one]

Result:
no goals

Proof state:
case h.e'_5
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : g x ≠ 0
this : ∀ᶠ (z : X) in nhds x, g z ≠ 0
⊢ (↑(algebraMapCLM ℝ≥0 𝕜)).comp { toFun := fun x => ‖g x‖₊ ^ 2, continuous_toFun := ⋯ } = star g * g

Tactic:
ext

Result:
case h.e'_5.h
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : g x ≠ 0
this : ∀ᶠ (z : X) in nhds x, g z ≠ 0
a✝ : X
⊢ ((↑(algebraMapCLM ℝ≥0 𝕜)).comp { toFun := fun x => ‖g x‖₊ ^ 2, continuous_toFun := ⋯ }) a✝ = (star g * g) a✝