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

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)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, 0 < g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, 0 < g₂ x
y : X
⊢ ((↑(algebraMapCLM ℝ≥0 𝕜)).comp (g₁ + g₂)) y = ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g₁ + (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₂) y

Tactic:
simp only [coe_add, Pi.add_apply, map_add, coe_comp, Function.comp_apply,
  ContinuousMap.coe_coe]

Result:
no goals

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)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : g x ≠ 0
this : ∀ᶠ (z : X) in nhds x, g z ≠ 0
a✝ : X
⊢ (algebraMap ℝ≥0 𝕜) ‖g a✝‖₊ ^ 2 = (starRingEnd 𝕜) (g a✝) * g a✝

Tactic:
simp only [normSq_eq_def', RCLike.conj_mul, ofReal_pow]

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
⊢ (algebraMap ℝ≥0 𝕜) ‖g a✝‖₊ ^ 2 = ↑‖g a✝‖ ^ 2

Proof state:
case refine_1
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', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ ∅, 0 < g' x

Tactic:
refine ⟨0, ?_, fun x hx => False.elim hx⟩

Result:
case refine_1
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)ᶜ
⊢ (↑(algebraMapCLM ℝ≥0 𝕜)).comp 0 ∈ I

Proof state:
case refine_3.intro.intro.intro.intro.refine_2.inr
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)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, 0 < g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, 0 < g₂ x
x : X
hx : x ∈ s₂
⊢ 0 < (g₁ + g₂) x

Tactic:
simpa only [zero_add] using add_lt_add_of_le_of_lt zero_le' (hgt₂ x hx)

Result:
no goals

Proof state:
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

Tactic:
refine ⟨g * g', ?_, hg, hgc.mono hgc'⟩

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}
⊢ (↑(algebraMapCLM ℝ≥0 𝕜)).comp (g * g') ∈ I

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
⊢ Disjoint t (setOfIdeal I)ᶜ

Tactic:
refine Set.subset_compl_iff_disjoint_left.mp fun x hx => ?_

Result:
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
x : X
hx : x ∈ (setOfIdeal I)ᶜ
⊢ x ∈ tᶜ

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‖₊ ≤ ε / 2

Tactic:
have :=
  calc
    ‖((1 - (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) x : 𝕜)‖₊ =
        ‖1 - algebraMap ℝ≥0 𝕜 (g x)‖₊ := by
      simp only [coe_sub, coe_one, coe_comp, ContinuousMap.coe_coe, Pi.sub_apply,
        Pi.one_apply, Function.comp_apply, algebraMapCLM_apply]
    _ = ‖algebraMap ℝ≥0 𝕜 (1 - g x)‖₊ := by
      simp only [Algebra.algebraMap_eq_smul_one, NNReal.smul_def, NNReal.coe_sub (hg x),
        NNReal.coe_one, sub_smul, one_smul]
    _ ≤ 1 := (nnnorm_algebraMap_nnreal 𝕜 (1 - g x)).trans_le tsub_le_self

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
this : ‖(1 - (↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ ≤ 1
⊢ ‖f x - f x * ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ ≤ ε / 2

Proof state:
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 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
⊢ ∃ b ∈ ↑I, nndist f b < ε

Tactic:
have htI : Disjoint t (setOfIdeal I)ᶜ := by
  refine Set.subset_compl_iff_disjoint_left.mp fun x hx => ?_
  simpa only [t, Set.mem_setOf, Set.mem_compl_iff, not_le] using
    (nnnorm_eq_zero.mpr (mem_idealOfSet.mp hf hx)).trans_lt (half_pos hε)

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 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
⊢ ∃ b ∈ ↑I, nndist f b < ε