[GOAL]
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
s : Set X
f g : C(X, R)
hf : f ∈ {f | ∀ (x : X), x ∈ sᶜ → ↑f x = 0}
hg : g ∈ {f | ∀ (x : X), x ∈ sᶜ → ↑f x = 0}
x : X
hx : x ∈ sᶜ
⊢ ↑(f + g) x = 0
[PROOFSTEP]
simp [hf x hx, hg x hx, coe_add, Pi.add_apply, add_zero]
[GOAL]
X : Type u_1
R : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : T2Space R
s : Set X
⊢ IsClosed ↑(idealOfSet R s)
[PROOFSTEP]
simp only [idealOfSet, Submodule.coe_set_mk, Set.setOf_forall]
[GOAL]
X : Type u_1
R : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : T2Space R
s : Set X
⊢ IsClosed
    ↑{
        toAddSubsemigroup :=
          { carrier := ⋂ (i : X) (_ : i ∈ sᶜ), {x | ↑x i = 0},
            add_mem' :=
              (_ :
                ∀ {a b : C(X, R)},
                  a ∈ ⋂ (i : X) (_ : i ∈ sᶜ), {x | ↑x i = 0} →
                    b ∈ ⋂ (i : X) (_ : i ∈ sᶜ), {x | ↑x i = 0} → a + b ∈ ⋂ (i : X) (_ : i ∈ sᶜ), {x | ↑x i = 0}) },
        zero_mem' :=
          (_ :
            0 ∈
              { carrier := ⋂ (i : X) (_ : i ∈ sᶜ), {x | ↑x i = 0},
                  add_mem' :=
                    (_ :
                      ∀ {a b : C(X, R)},
                        a ∈ ⋂ (i : X) (_ : i ∈ sᶜ), {x | ↑x i = 0} →
                          b ∈ ⋂ (i : X) (_ : i ∈ sᶜ), {x | ↑x i = 0} →
                            a + b ∈ ⋂ (i : X) (_ : i ∈ sᶜ), {x | ↑x i = 0}) }.carrier) }
[PROOFSTEP]
exact isClosed_iInter fun x => isClosed_iInter fun _ => isClosed_eq (continuous_eval_const x) continuous_const
[GOAL]
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
s : Set X
f : C(X, R)
⊢ f ∈ idealOfSet R s ↔ ∀ ⦃x : X⦄, x ∈ sᶜ → ↑f x = 0
[PROOFSTEP]
convert Iff.rfl
[GOAL]
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
s : Set X
f : C(X, R)
⊢ ¬f ∈ idealOfSet R s ↔ ∃ x, x ∈ sᶜ ∧ ↑f x ≠ 0
[PROOFSTEP]
simp_rw [mem_idealOfSet]
[GOAL]
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
s : Set X
f : C(X, R)
⊢ (¬∀ ⦃x : X⦄, x ∈ sᶜ → ↑f x = 0) ↔ ∃ x, x ∈ sᶜ ∧ ↑f x ≠ 0
[PROOFSTEP]
push_neg
[GOAL]
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
s : Set X
f : C(X, R)
⊢ (Exists fun ⦃x⦄ => x ∈ sᶜ ∧ ↑f x ≠ 0) ↔ ∃ x, x ∈ sᶜ ∧ ↑f x ≠ 0
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ ¬x ∈ setOfIdeal I ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → ↑f x = 0
[PROOFSTEP]
rw [← Set.mem_compl_iff, setOfIdeal, compl_compl, Set.mem_setOf]
[GOAL]
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ x ∈ setOfIdeal I ↔ ∃ f, f ∈ I ∧ ↑f x ≠ 0
[PROOFSTEP]
simp_rw [setOfIdeal, Set.mem_compl_iff, Set.mem_setOf]
[GOAL]
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ (¬∀ (f : C(X, R)), f ∈ I → ↑f x = 0) ↔ ∃ f, f ∈ I ∧ ↑f x ≠ 0
[PROOFSTEP]
push_neg
[GOAL]
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ (∃ f, f ∈ I ∧ ↑f x ≠ 0) ↔ ∃ f, f ∈ I ∧ ↑f x ≠ 0
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
R : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : T2Space R
I : Ideal C(X, R)
⊢ IsOpen (setOfIdeal I)
[PROOFSTEP]
simp only [setOfIdeal, Set.setOf_forall, isOpen_compl_iff]
[GOAL]
X : Type u_1
R : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
inst✝ : T2Space R
I : Ideal C(X, R)
⊢ IsClosed (⋂ (i : C(X, R)) (_ : i ∈ I), {x | ↑i x = 0})
[PROOFSTEP]
exact isClosed_iInter fun f => isClosed_iInter fun _ => isClosed_eq (map_continuous f) continuous_const
[GOAL]
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
f : C(X, R)
⊢ f ∈ idealOfSet R ∅ ↔ f ∈ ⊥
[PROOFSTEP]
simp only [mem_idealOfSet, Set.compl_empty, Set.mem_univ, forall_true_left, Ideal.mem_bot, FunLike.ext_iff, zero_apply]
[GOAL]
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
x : X
f : C(X, R)
⊢ f ∈ idealOfSet R {x}ᶜ ↔ ↑f x = 0
[PROOFSTEP]
simp only [mem_idealOfSet, compl_compl, Set.mem_singleton_iff, forall_eq]
[GOAL]
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
⊢ GaloisConnection setOfIdeal (idealOfSet R)
[PROOFSTEP]
refine' fun I s => ⟨fun h f hf => _, fun h x hx => _⟩
[GOAL]
case refine'_1
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ≤ s
f : C(X, R)
hf : f ∈ I
⊢ f ∈ idealOfSet R s
[PROOFSTEP]
by_contra h'
[GOAL]
case refine'_1
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ≤ s
f : C(X, R)
hf : f ∈ I
h' : ¬f ∈ idealOfSet R s
⊢ False
[PROOFSTEP]
rcases not_mem_idealOfSet.mp h' with ⟨x, hx, hfx⟩
[GOAL]
case refine'_1.intro.intro
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ≤ s
f : C(X, R)
hf : f ∈ I
h' : ¬f ∈ idealOfSet R s
x : X
hx : x ∈ sᶜ
hfx : ↑f x ≠ 0
⊢ False
[PROOFSTEP]
exact hfx (not_mem_setOfIdeal.mp (mt (@h x) hx) hf)
[GOAL]
case refine'_2
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
⊢ x ∈ s
[PROOFSTEP]
obtain ⟨f, hf, hfx⟩ := mem_setOfIdeal.mp hx
[GOAL]
case refine'_2.intro.intro
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
f : C(X, R)
hf : f ∈ I
hfx : ↑f x ≠ 0
⊢ x ∈ s
[PROOFSTEP]
by_contra hx'
[GOAL]
case refine'_2.intro.intro
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
f : C(X, R)
hf : f ∈ I
hfx : ↑f x ≠ 0
hx' : ¬x ∈ s
⊢ False
[PROOFSTEP]
exact not_mem_idealOfSet.mpr ⟨x, hx', hfx⟩ (h hf)
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : TopologicalSpace X
f : C(X, ℝ≥0)
c : ℝ≥0
hc : 0 < c
x : X
hx : x ∈ {x | c ≤ ↑f x}
⊢ ↑(mk (↑f ⊔ ↑(const X c))⁻¹ * f) x = OfNat.ofNat 1 x
[PROOFSTEP]
simpa only [coe_const, ge_iff_le, mul_apply, coe_mk, Pi.inv_apply, Pi.sup_apply, Function.const_apply,
  sup_eq_left.mpr (Set.mem_setOf.mp hx), ne_eq, Pi.one_apply] using inv_mul_cancel (hc.trans_le hx).ne'
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
⊢ idealOfSet 𝕜 (setOfIdeal I) = Ideal.closure I
[PROOFSTEP]
refine'
  le_antisymm _
    ((idealOfSet_closed 𝕜 <| setOfIdeal I).closure_subset_iff.mpr fun f hf x hx => not_mem_setOfIdeal.mp hx hf)
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
⊢ idealOfSet 𝕜 (setOfIdeal I) ≤ Ideal.closure I
[PROOFSTEP]
refine' (fun f hf => Metric.mem_closure_iff.mpr fun ε hε => _)
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ
hε : ε > 0
⊢ ∃ b, b ∈ ↑I ∧ dist f b < ε
[PROOFSTEP]
lift ε to ℝ≥0 using hε.lt.le
[GOAL]
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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, b ∈ ↑I ∧ dist f b < ↑ε
[PROOFSTEP]
replace hε := show (0 : ℝ≥0) < ε from hε
[GOAL]
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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, b ∈ ↑I ∧ dist f b < ↑ε
[PROOFSTEP]
simp_rw [dist_nndist]
[GOAL]
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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, b ∈ ↑I ∧ ↑(nndist f b) < ↑ε
[PROOFSTEP]
norm_cast
  -- Let `t := {x : X | ε / 2 ≤ ‖f x‖₊}}` which is closed and disjoint from `set_of_ideal I`.
[GOAL]
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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, b ∈ ↑I ∧ nndist f b < ε
[PROOFSTEP]
set t := {x : X | ε / 2 ≤ ‖f x‖₊}
[GOAL]
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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‖₊}
⊢ ∃ b, b ∈ ↑I ∧ nndist f b < ε
[PROOFSTEP]
have ht : IsClosed t := isClosed_le continuous_const (map_continuous f).nnnorm
[GOAL]
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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, b ∈ ↑I ∧ nndist f b < ε
[PROOFSTEP]
have htI : Disjoint t (setOfIdeal I)ᶜ :=
  by
  refine' Set.subset_compl_iff_disjoint_left.mp fun x hx => _
  simpa only [Set.mem_setOf, Set.mem_compl_iff, not_le] using
    (nnnorm_eq_zero.mpr (mem_idealOfSet.mp hf hx)).trans_lt
      (half_pos hε)
        /- It suffices to produce `g : C(X, ℝ≥0)` which takes values in `[0,1]` and is constantly `1` on
            `t` such that when composed with the natural embedding of `ℝ≥0` into `𝕜` lies in the ideal `I`.
            Indeed, then `‖f - f * ↑g‖ ≤ ‖f * (1 - ↑g)‖ ≤ ⨆ ‖f * (1 - ↑g) x‖`. When `x ∉ t`, `‖f x‖ < ε / 2`
            and `‖(1 - ↑g) x‖ ≤ 1`, and when `x ∈ t`, `(1 - ↑g) x = 0`, and clearly `f * ↑g ∈ I`. -/
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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)ᶜ
[PROOFSTEP]
refine' Set.subset_compl_iff_disjoint_left.mp fun x hx => _
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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ᶜ
[PROOFSTEP]
simpa only [Set.mem_setOf, Set.mem_compl_iff, not_le] using
  (nnnorm_eq_zero.mpr (mem_idealOfSet.mp hf hx)).trans_lt
    (half_pos hε)
      /- It suffices to produce `g : C(X, ℝ≥0)` which takes values in `[0,1]` and is constantly `1` on
          `t` such that when composed with the natural embedding of `ℝ≥0` into `𝕜` lies in the ideal `I`.
          Indeed, then `‖f - f * ↑g‖ ≤ ‖f * (1 - ↑g)‖ ≤ ⨆ ‖f * (1 - ↑g) x‖`. When `x ∉ t`, `‖f x‖ < ε / 2`
          and `‖(1 - ↑g) x‖ ≤ 1`, and when `x ∈ t`, `(1 - ↑g) x = 0`, and clearly `f * ↑g ∈ I`. -/
[GOAL]
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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, b ∈ ↑I ∧ nndist f b < ε
[PROOFSTEP]
suffices ∃ g : C(X, ℝ≥0), (algebraMapClm ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g ∈ I ∧ (∀ x, g x ≤ 1) ∧ t.EqOn g 1
  by
  obtain ⟨g, hgI, hg, hgt⟩ := this
  refine' ⟨f * (algebraMapClm ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g, I.mul_mem_left f hgI, _⟩
  rw [nndist_eq_nnnorm]
  refine' (nnnorm_lt_iff _ hε).2 fun x => _
  simp only [coe_sub, coe_mul, Pi.sub_apply, Pi.mul_apply]
  by_cases hx : x ∈ t
  ·
    simpa only [hgt hx, comp_apply, Pi.one_apply, ContinuousMap.coe_coe, algebraMapClm_apply, map_one, mul_one,
      sub_self, nnnorm_zero] using hε
  · refine' lt_of_le_of_lt _ (half_lt_self hε)
    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, ge_iff_le, NNReal.coe_sub (hg x), NNReal.coe_one,
            sub_smul, one_smul]
        _ ≤ 1 := (nnnorm_algebraMap_nNReal 𝕜 (1 - g x)).trans_le tsub_le_self
    calc
      ‖f x - f x * (algebraMapClm ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g x‖₊ =
          ‖f x * (1 - (algebraMapClm ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) x‖₊ :=
        by simp only [mul_sub, coe_sub, coe_one, Pi.sub_apply, Pi.one_apply, mul_one]
      _ ≤ ε / 2 * ‖(1 - (algebraMapClm ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) x‖₊ :=
        ((nnnorm_mul_le _ _).trans (mul_le_mul_right' (not_le.mp <| show ¬ε / 2 ≤ ‖f x‖₊ from hx).le _))
      _ ≤ ε / 2 := by
        simpa only [mul_one] using
          mul_le_mul_left' this
            _
              /- There is some `g' : C(X, ℝ≥0)` which is strictly positive on `t` such that the composition
                  `↑g` with the natural embedding of `ℝ≥0` into `𝕜` lies in `I`. This follows from compactness of
                  `t` and that we can do it in any neighborhood of a point `x ∈ t`. Indeed, since `x ∈ t`, then
                  `fₓ x ≠ 0` for some `fₓ ∈ I` and so `fun y ↦ ‖(star fₓ * fₓ) y‖₊` is strictly posiive in a
                  neighborhood of `y`. Moreover, `(‖(star fₓ * fₓ) y‖₊ : 𝕜) = (star fₓ * fₓ) y`, so composition of
                  this map with the natural embedding is just `star fₓ * fₓ ∈ I`. -/
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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, comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I ∧ (∀ (x : X), ↑g x ≤ 1) ∧ Set.EqOn (↑g) 1 t
⊢ ∃ b, b ∈ ↑I ∧ nndist f b < ε
[PROOFSTEP]
obtain ⟨g, hgI, hg, hgt⟩ := this
[GOAL]
case intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hg : ∀ (x : X), ↑g x ≤ 1
hgt : Set.EqOn (↑g) 1 t
⊢ ∃ b, b ∈ ↑I ∧ nndist f b < ε
[PROOFSTEP]
refine' ⟨f * (algebraMapClm ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g, I.mul_mem_left f hgI, _⟩
[GOAL]
case intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hg : ∀ (x : X), ↑g x ≤ 1
hgt : Set.EqOn (↑g) 1 t
⊢ nndist f (f * comp (↑(algebraMapClm ℝ≥0 𝕜)) g) < ε
[PROOFSTEP]
rw [nndist_eq_nnnorm]
[GOAL]
case intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hg : ∀ (x : X), ↑g x ≤ 1
hgt : Set.EqOn (↑g) 1 t
⊢ ‖f - f * comp (↑(algebraMapClm ℝ≥0 𝕜)) g‖₊ < ε
[PROOFSTEP]
refine' (nnnorm_lt_iff _ hε).2 fun x => _
[GOAL]
case intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hg : ∀ (x : X), ↑g x ≤ 1
hgt : Set.EqOn (↑g) 1 t
x : X
⊢ ‖↑(f - f * comp (↑(algebraMapClm ℝ≥0 𝕜)) g) x‖₊ < ε
[PROOFSTEP]
simp only [coe_sub, coe_mul, Pi.sub_apply, Pi.mul_apply]
[GOAL]
case intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hg : ∀ (x : X), ↑g x ≤ 1
hgt : Set.EqOn (↑g) 1 t
x : X
⊢ ‖↑f x - ↑f x * ↑(comp (↑(algebraMapClm ℝ≥0 𝕜)) g) x‖₊ < ε
[PROOFSTEP]
by_cases hx : x ∈ t
[GOAL]
case pos
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hg : ∀ (x : X), ↑g x ≤ 1
hgt : Set.EqOn (↑g) 1 t
x : X
hx : x ∈ t
⊢ ‖↑f x - ↑f x * ↑(comp (↑(algebraMapClm ℝ≥0 𝕜)) g) x‖₊ < ε
[PROOFSTEP]
simpa only [hgt hx, comp_apply, Pi.one_apply, ContinuousMap.coe_coe, algebraMapClm_apply, map_one, mul_one, sub_self,
  nnnorm_zero] using hε
[GOAL]
case neg
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hg : ∀ (x : X), ↑g x ≤ 1
hgt : Set.EqOn (↑g) 1 t
x : X
hx : ¬x ∈ t
⊢ ‖↑f x - ↑f x * ↑(comp (↑(algebraMapClm ℝ≥0 𝕜)) g) x‖₊ < ε
[PROOFSTEP]
refine' lt_of_le_of_lt _ (half_lt_self hε)
[GOAL]
case neg
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hg : ∀ (x : X), ↑g x ≤ 1
hgt : Set.EqOn (↑g) 1 t
x : X
hx : ¬x ∈ t
⊢ ‖↑f x - ↑f x * ↑(comp (↑(algebraMapClm ℝ≥0 𝕜)) g) x‖₊ ≤ ε / 2
[PROOFSTEP]
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, ge_iff_le, NNReal.coe_sub (hg x), NNReal.coe_one,
        sub_smul, one_smul]
    _ ≤ 1 := (nnnorm_algebraMap_nNReal 𝕜 (1 - g x)).trans_le tsub_le_self
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hg : ∀ (x : X), ↑g x ≤ 1
hgt : Set.EqOn (↑g) 1 t
x : X
hx : ¬x ∈ t
⊢ ‖↑(1 - comp (↑(algebraMapClm ℝ≥0 𝕜)) g) x‖₊ = ‖1 - ↑(algebraMap ℝ≥0 𝕜) (↑g x)‖₊
[PROOFSTEP]
simp only [coe_sub, coe_one, coe_comp, ContinuousMap.coe_coe, Pi.sub_apply, Pi.one_apply, Function.comp_apply,
  algebraMapClm_apply]
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hg : ∀ (x : X), ↑g x ≤ 1
hgt : Set.EqOn (↑g) 1 t
x : X
hx : ¬x ∈ t
⊢ ‖1 - ↑(algebraMap ℝ≥0 𝕜) (↑g x)‖₊ = ‖↑(algebraMap ℝ≥0 𝕜) (1 - ↑g x)‖₊
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, NNReal.smul_def, ge_iff_le, NNReal.coe_sub (hg x), NNReal.coe_one, sub_smul,
  one_smul]
[GOAL]
case neg
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hg : ∀ (x : X), ↑g x ≤ 1
hgt : Set.EqOn (↑g) 1 t
x : X
hx : ¬x ∈ t
this : ‖↑(1 - comp (↑(algebraMapClm ℝ≥0 𝕜)) g) x‖₊ ≤ 1
⊢ ‖↑f x - ↑f x * ↑(comp (↑(algebraMapClm ℝ≥0 𝕜)) g) x‖₊ ≤ ε / 2
[PROOFSTEP]
calc
  ‖f x - f x * (algebraMapClm ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g x‖₊ =
      ‖f x * (1 - (algebraMapClm ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) x‖₊ :=
    by simp only [mul_sub, coe_sub, coe_one, Pi.sub_apply, Pi.one_apply, mul_one]
  _ ≤ ε / 2 * ‖(1 - (algebraMapClm ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) x‖₊ :=
    ((nnnorm_mul_le _ _).trans (mul_le_mul_right' (not_le.mp <| show ¬ε / 2 ≤ ‖f x‖₊ from hx).le _))
  _ ≤ ε / 2 := by
    simpa only [mul_one] using
      mul_le_mul_left' this
        _
          /- There is some `g' : C(X, ℝ≥0)` which is strictly positive on `t` such that the composition
              `↑g` with the natural embedding of `ℝ≥0` into `𝕜` lies in `I`. This follows from compactness of
              `t` and that we can do it in any neighborhood of a point `x ∈ t`. Indeed, since `x ∈ t`, then
              `fₓ x ≠ 0` for some `fₓ ∈ I` and so `fun y ↦ ‖(star fₓ * fₓ) y‖₊` is strictly posiive in a
              neighborhood of `y`. Moreover, `(‖(star fₓ * fₓ) y‖₊ : 𝕜) = (star fₓ * fₓ) y`, so composition of
              this map with the natural embedding is just `star fₓ * fₓ ∈ I`. -/
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hg : ∀ (x : X), ↑g x ≤ 1
hgt : Set.EqOn (↑g) 1 t
x : X
hx : ¬x ∈ t
this : ‖↑(1 - comp (↑(algebraMapClm ℝ≥0 𝕜)) g) x‖₊ ≤ 1
⊢ ‖↑f x - ↑f x * ↑(comp (↑(algebraMapClm ℝ≥0 𝕜)) g) x‖₊ = ‖↑f x * ↑(1 - comp (↑(algebraMapClm ℝ≥0 𝕜)) g) x‖₊
[PROOFSTEP]
simp only [mul_sub, coe_sub, coe_one, Pi.sub_apply, Pi.one_apply, mul_one]
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hg : ∀ (x : X), ↑g x ≤ 1
hgt : Set.EqOn (↑g) 1 t
x : X
hx : ¬x ∈ t
this : ‖↑(1 - comp (↑(algebraMapClm ℝ≥0 𝕜)) g) x‖₊ ≤ 1
⊢ ε / 2 * ‖↑(1 - comp (↑(algebraMapClm ℝ≥0 𝕜)) g) x‖₊ ≤ ε / 2
[PROOFSTEP]
simpa only [mul_one] using
  mul_le_mul_left' this
    _
      /- There is some `g' : C(X, ℝ≥0)` which is strictly positive on `t` such that the composition
          `↑g` with the natural embedding of `ℝ≥0` into `𝕜` lies in `I`. This follows from compactness of
          `t` and that we can do it in any neighborhood of a point `x ∈ t`. Indeed, since `x ∈ t`, then
          `fₓ x ≠ 0` for some `fₓ ∈ I` and so `fun y ↦ ‖(star fₓ * fₓ) y‖₊` is strictly posiive in a
          neighborhood of `y`. Moreover, `(‖(star fₓ * fₓ) y‖₊ : 𝕜) = (star fₓ * fₓ) y`, so composition of
          this map with the natural embedding is just `star fₓ * fₓ ∈ I`. -/
[GOAL]
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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, comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I ∧ (∀ (x : X), ↑g x ≤ 1) ∧ Set.EqOn (↑g) 1 t
[PROOFSTEP]
have : ∃ g' : C(X, ℝ≥0), (algebraMapClm ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g' ∈ I ∧ ∀ x ∈ t, 0 < g' x :=
  by
  refine' ht.isCompact.induction_on _ _ _ _
  · refine' ⟨0, _, fun x hx => False.elim hx⟩
    convert I.zero_mem
    ext
    simp only [comp_apply, zero_apply, ContinuousMap.coe_coe, map_zero]
  · rintro s₁ s₂ hs ⟨g, hI, hgt⟩; exact ⟨g, hI, fun x hx => hgt x (hs hx)⟩
  · rintro s₁ s₂ ⟨g₁, hI₁, hgt₁⟩ ⟨g₂, hI₂, hgt₂⟩
    refine' ⟨g₁ + g₂, _, fun x hx => _⟩
    · convert I.add_mem hI₁ hI₂
      ext y
      simp only [coe_add, Pi.add_apply, map_add, coe_comp, Function.comp_apply, ContinuousMap.coe_coe]
    · rcases hx with (hx | hx)
      simpa only [zero_add] using add_lt_add_of_lt_of_le (hgt₁ x hx) zero_le'
      simpa only [zero_add] using add_lt_add_of_le_of_lt zero_le' (hgt₂ x hx)
  · intro x hx
    replace hx := htI.subset_compl_right hx
    rw [compl_compl, mem_setOfIdeal] at hx
    obtain ⟨g, hI, hgx⟩ := hx
    have := (map_continuous g).continuousAt.eventually_ne hgx
    refine'
      ⟨{y : X | g y ≠ 0} ∩ t, mem_nhdsWithin_iff_exists_mem_nhds_inter.mpr ⟨_, this, Set.Subset.rfl⟩,
        ⟨⟨fun x => ‖g x‖₊ ^ 2, (map_continuous g).nnnorm.pow 2⟩, _, fun x hx => pow_pos (norm_pos_iff.mpr hx.1) 2⟩⟩
    convert I.mul_mem_left (star g) hI
    ext
    simp only [comp_apply, ContinuousMap.coe_coe, coe_mk, algebraMapClm_toFun, map_pow, mul_apply, star_apply, star_def]
    simp only [normSq_eq_def', IsROrC.conj_mul, ofReal_pow]
    rfl
      /- Get the function `g'` which is guaranteed to exist above. By the extreme value theorem and
          compactness of `t`, there is some `0 < c` such that `c ≤ g' x` for all `x ∈ t`. Then by
          `exists_mul_le_one_eqOn_ge` there is some `g` for which `g * g'` is the desired function. -/
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ t → 0 < ↑g' x
[PROOFSTEP]
refine' ht.isCompact.induction_on _ _ _ _
[GOAL]
case refine'_1
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ ∅ → 0 < ↑g' x
[PROOFSTEP]
refine' ⟨0, _, fun x hx => False.elim hx⟩
[GOAL]
case refine'_1
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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)ᶜ
⊢ comp (↑(algebraMapClm ℝ≥0 𝕜)) 0 ∈ I
[PROOFSTEP]
convert I.zero_mem
[GOAL]
case h.e'_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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)ᶜ
⊢ comp (↑(algebraMapClm ℝ≥0 𝕜)) 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h.e'_4.h
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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
⊢ ↑(comp (↑(algebraMapClm ℝ≥0 𝕜)) 0) a✝ = ↑0 a✝
[PROOFSTEP]
simp only [comp_apply, zero_apply, ContinuousMap.coe_coe, map_zero]
[GOAL]
case refine'_2
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 t : Set X⦄,
    s ⊆ t →
      (∃ g', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ t → 0 < ↑g' x) →
        ∃ g', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ s → 0 < ↑g' x
[PROOFSTEP]
rintro s₁ s₂ hs ⟨g, hI, hgt⟩
[GOAL]
case refine'_2.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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
hs : s₁ ⊆ s₂
g : C(X, ℝ≥0)
hI : comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I
hgt : ∀ (x : X), x ∈ s₂ → 0 < ↑g x
⊢ ∃ g', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ s₁ → 0 < ↑g' x
[PROOFSTEP]
exact ⟨g, hI, fun x hx => hgt x (hs hx)⟩
[GOAL]
case refine'_3
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 t : Set X⦄,
    (∃ g', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ s → 0 < ↑g' x) →
      (∃ g', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ t → 0 < ↑g' x) →
        ∃ g', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ s ∪ t → 0 < ↑g' x
[PROOFSTEP]
rintro s₁ s₂ ⟨g₁, hI₁, hgt₁⟩ ⟨g₂, hI₂, hgt₂⟩
[GOAL]
case refine'_3.intro.intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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₁ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₁ ∈ I
hgt₁ : ∀ (x : X), x ∈ s₁ → 0 < ↑g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₂ ∈ I
hgt₂ : ∀ (x : X), x ∈ s₂ → 0 < ↑g₂ x
⊢ ∃ g', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ s₁ ∪ s₂ → 0 < ↑g' x
[PROOFSTEP]
refine' ⟨g₁ + g₂, _, fun x hx => _⟩
[GOAL]
case refine'_3.intro.intro.intro.intro.refine'_1
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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₁ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₁ ∈ I
hgt₁ : ∀ (x : X), x ∈ s₁ → 0 < ↑g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₂ ∈ I
hgt₂ : ∀ (x : X), x ∈ s₂ → 0 < ↑g₂ x
⊢ comp (↑(algebraMapClm ℝ≥0 𝕜)) (g₁ + g₂) ∈ I
[PROOFSTEP]
convert I.add_mem hI₁ hI₂
[GOAL]
case h.e'_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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₁ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₁ ∈ I
hgt₁ : ∀ (x : X), x ∈ s₁ → 0 < ↑g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₂ ∈ I
hgt₂ : ∀ (x : X), x ∈ s₂ → 0 < ↑g₂ x
⊢ comp (↑(algebraMapClm ℝ≥0 𝕜)) (g₁ + g₂) = comp (↑(algebraMapClm ℝ≥0 𝕜)) g₁ + comp (↑(algebraMapClm ℝ≥0 𝕜)) g₂
[PROOFSTEP]
ext y
[GOAL]
case h.e'_4.h
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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₁ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₁ ∈ I
hgt₁ : ∀ (x : X), x ∈ s₁ → 0 < ↑g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₂ ∈ I
hgt₂ : ∀ (x : X), x ∈ s₂ → 0 < ↑g₂ x
y : X
⊢ ↑(comp (↑(algebraMapClm ℝ≥0 𝕜)) (g₁ + g₂)) y =
    ↑(comp (↑(algebraMapClm ℝ≥0 𝕜)) g₁ + comp (↑(algebraMapClm ℝ≥0 𝕜)) g₂) y
[PROOFSTEP]
simp only [coe_add, Pi.add_apply, map_add, coe_comp, Function.comp_apply, ContinuousMap.coe_coe]
[GOAL]
case refine'_3.intro.intro.intro.intro.refine'_2
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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₁ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₁ ∈ I
hgt₁ : ∀ (x : X), x ∈ s₁ → 0 < ↑g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₂ ∈ I
hgt₂ : ∀ (x : X), x ∈ s₂ → 0 < ↑g₂ x
x : X
hx : x ∈ s₁ ∪ s₂
⊢ 0 < ↑(g₁ + g₂) x
[PROOFSTEP]
rcases hx with (hx | hx)
[GOAL]
case refine'_3.intro.intro.intro.intro.refine'_2.inl
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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₁ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₁ ∈ I
hgt₁ : ∀ (x : X), x ∈ s₁ → 0 < ↑g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₂ ∈ I
hgt₂ : ∀ (x : X), x ∈ s₂ → 0 < ↑g₂ x
x : X
hx : x ∈ s₁
⊢ 0 < ↑(g₁ + g₂) x
case refine'_3.intro.intro.intro.intro.refine'_2.inr
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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₁ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₁ ∈ I
hgt₁ : ∀ (x : X), x ∈ s₁ → 0 < ↑g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₂ ∈ I
hgt₂ : ∀ (x : X), x ∈ s₂ → 0 < ↑g₂ x
x : X
hx : x ∈ s₂
⊢ 0 < ↑(g₁ + g₂) x
[PROOFSTEP]
simpa only [zero_add] using add_lt_add_of_lt_of_le (hgt₁ x hx) zero_le'
[GOAL]
case refine'_3.intro.intro.intro.intro.refine'_2.inr
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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₁ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₁ ∈ I
hgt₁ : ∀ (x : X), x ∈ s₁ → 0 < ↑g₁ x
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapClm ℝ≥0 𝕜)) g₂ ∈ I
hgt₂ : ∀ (x : X), x ∈ s₂ → 0 < ↑g₂ x
x : X
hx : x ∈ s₂
⊢ 0 < ↑(g₁ + g₂) x
[PROOFSTEP]
simpa only [zero_add] using add_lt_add_of_le_of_lt zero_le' (hgt₂ x hx)
[GOAL]
case refine'_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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),
    x ∈ t → ∃ t_1, t_1 ∈ nhdsWithin x t ∧ ∃ g', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ t_1 → 0 < ↑g' x
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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, t_1 ∈ nhdsWithin x t ∧ ∃ g', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ t_1 → 0 < ↑g' x
[PROOFSTEP]
replace hx := htI.subset_compl_right hx
[GOAL]
case refine'_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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, t_1 ∈ nhdsWithin x t ∧ ∃ g', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ t_1 → 0 < ↑g' x
[PROOFSTEP]
rw [compl_compl, mem_setOfIdeal] at hx
[GOAL]
case refine'_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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 : ∃ f, f ∈ I ∧ ↑f x ≠ 0
⊢ ∃ t_1, t_1 ∈ nhdsWithin x t ∧ ∃ g', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ t_1 → 0 < ↑g' x
[PROOFSTEP]
obtain ⟨g, hI, hgx⟩ := hx
[GOAL]
case refine'_4.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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
⊢ ∃ t_1, t_1 ∈ nhdsWithin x t ∧ ∃ g', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ t_1 → 0 < ↑g' x
[PROOFSTEP]
have := (map_continuous g).continuousAt.eventually_ne hgx
[GOAL]
case refine'_4.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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
⊢ ∃ t_1, t_1 ∈ nhdsWithin x t ∧ ∃ g', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ t_1 → 0 < ↑g' x
[PROOFSTEP]
refine'
  ⟨{y : X | g y ≠ 0} ∩ t, mem_nhdsWithin_iff_exists_mem_nhds_inter.mpr ⟨_, this, Set.Subset.rfl⟩,
    ⟨⟨fun x => ‖g x‖₊ ^ 2, (map_continuous g).nnnorm.pow 2⟩, _, fun x hx => pow_pos (norm_pos_iff.mpr hx.1) 2⟩⟩
[GOAL]
case refine'_4.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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
⊢ comp (↑(algebraMapClm ℝ≥0 𝕜)) (mk fun x => ‖↑g x‖₊ ^ 2) ∈ I
[PROOFSTEP]
convert I.mul_mem_left (star g) hI
[GOAL]
case h.e'_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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
⊢ comp (↑(algebraMapClm ℝ≥0 𝕜)) (mk fun x => ‖↑g x‖₊ ^ 2) = star g * g
[PROOFSTEP]
ext
[GOAL]
case h.e'_4.h
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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
⊢ ↑(comp (↑(algebraMapClm ℝ≥0 𝕜)) (mk fun x => ‖↑g x‖₊ ^ 2)) a✝ = ↑(star g * g) a✝
[PROOFSTEP]
simp only [comp_apply, ContinuousMap.coe_coe, coe_mk, algebraMapClm_toFun, map_pow, mul_apply, star_apply, star_def]
[GOAL]
case h.e'_4.h
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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✝
[PROOFSTEP]
simp only [normSq_eq_def', IsROrC.conj_mul, ofReal_pow]
[GOAL]
case h.e'_4.h
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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
[PROOFSTEP]
rfl
  /- Get the function `g'` which is guaranteed to exist above. By the extreme value theorem and
      compactness of `t`, there is some `0 < c` such that `c ≤ g' x` for all `x ∈ t`. Then by
      `exists_mul_le_one_eqOn_ge` there is some `g` for which `g * g'` is the desired function. -/
[GOAL]
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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', comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I ∧ ∀ (x : X), x ∈ t → 0 < ↑g' x
⊢ ∃ g, comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I ∧ (∀ (x : X), ↑g x ≤ 1) ∧ Set.EqOn (↑g) 1 t
[PROOFSTEP]
obtain ⟨g', hI', hgt'⟩ := this
[GOAL]
case intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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' : comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I
hgt' : ∀ (x : X), x ∈ t → 0 < ↑g' x
⊢ ∃ g, comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I ∧ (∀ (x : X), ↑g x ≤ 1) ∧ Set.EqOn (↑g) 1 t
[PROOFSTEP]
obtain ⟨c, hc, hgc'⟩ : ∃ (c : _) (_ : 0 < c), ∀ y : X, y ∈ t → c ≤ g' y :=
  t.eq_empty_or_nonempty.elim (fun ht' => ⟨1, zero_lt_one, fun y hy => False.elim (by rwa [ht'] at hy )⟩) fun ht' =>
    let ⟨x, hx, hx'⟩ := ht.isCompact.exists_forall_le ht' (map_continuous g').continuousOn
    ⟨g' x, hgt' x hx, hx'⟩
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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' : comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I
hgt' : ∀ (x : X), x ∈ t → 0 < ↑g' x
ht' : t = ∅
y : X
hy : y ∈ t
⊢ False
[PROOFSTEP]
rwa [ht'] at hy
[GOAL]
case intro.intro.intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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' : comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I
hgt' : ∀ (x : X), x ∈ t → 0 < ↑g' x
c : ℝ≥0
hc : 0 < c
hgc' : ∀ (y : X), y ∈ t → c ≤ ↑g' y
⊢ ∃ g, comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I ∧ (∀ (x : X), ↑g x ≤ 1) ∧ Set.EqOn (↑g) 1 t
[PROOFSTEP]
obtain ⟨g, hg, hgc⟩ := exists_mul_le_one_eqOn_ge g' hc
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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' : comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I
hgt' : ∀ (x : X), x ∈ t → 0 < ↑g' x
c : ℝ≥0
hc : 0 < c
hgc' : ∀ (y : X), 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, comp (↑(algebraMapClm ℝ≥0 𝕜)) g ∈ I ∧ (∀ (x : X), ↑g x ≤ 1) ∧ Set.EqOn (↑g) 1 t
[PROOFSTEP]
refine' ⟨g * g', _, hg, hgc.mono hgc'⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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' : comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I
hgt' : ∀ (x : X), x ∈ t → 0 < ↑g' x
c : ℝ≥0
hc : 0 < c
hgc' : ∀ (y : X), 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}
⊢ comp (↑(algebraMapClm ℝ≥0 𝕜)) (g * g') ∈ I
[PROOFSTEP]
convert I.mul_mem_left ((algebraMapClm ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) hI'
[GOAL]
case h.e'_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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' : comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I
hgt' : ∀ (x : X), x ∈ t → 0 < ↑g' x
c : ℝ≥0
hc : 0 < c
hgc' : ∀ (y : X), 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}
⊢ comp (↑(algebraMapClm ℝ≥0 𝕜)) (g * g') = comp (↑(algebraMapClm ℝ≥0 𝕜)) g * comp (↑(algebraMapClm ℝ≥0 𝕜)) g'
[PROOFSTEP]
ext
[GOAL]
case h.e'_4.h
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
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' : comp (↑(algebraMapClm ℝ≥0 𝕜)) g' ∈ I
hgt' : ∀ (x : X), x ∈ t → 0 < ↑g' x
c : ℝ≥0
hc : 0 < c
hgc' : ∀ (y : X), 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}
a✝ : X
⊢ ↑(comp (↑(algebraMapClm ℝ≥0 𝕜)) (g * g')) a✝ =
    ↑(comp (↑(algebraMapClm ℝ≥0 𝕜)) g * comp (↑(algebraMapClm ℝ≥0 𝕜)) g') a✝
[PROOFSTEP]
simp only [algebraMapClm_coe, comp_apply, mul_apply, ContinuousMap.coe_coe, map_mul]
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
⊢ setOfIdeal (idealOfSet 𝕜 s) = interior s
[PROOFSTEP]
refine'
  Set.Subset.antisymm
    ((setOfIdeal_open (idealOfSet 𝕜 s)).subset_interior_iff.mpr fun x hx =>
      let ⟨f, hf, hfx⟩ := mem_setOfIdeal.mp hx
      Set.not_mem_compl_iff.mp (mt (@hf x) hfx))
    fun x hx =>
    _
      -- If `x ∉ closure sᶜ`, we must produce `f : C(X, 𝕜)` which is zero on `sᶜ` and `f x ≠ 0`.
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ interior s
⊢ x ∈ setOfIdeal (idealOfSet 𝕜 s)
[PROOFSTEP]
rw [← compl_compl (interior s), ← closure_compl] at hx
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
⊢ x ∈ setOfIdeal (idealOfSet 𝕜 s)
[PROOFSTEP]
simp_rw [mem_setOfIdeal, mem_idealOfSet]
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
⊢ ∃ f, (∀ ⦃x : X⦄, x ∈ sᶜ → ↑f x = 0) ∧ ↑f x ≠ 0
[PROOFSTEP]
haveI : NormalSpace X := normalOfCompactT2
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
this : NormalSpace X
⊢ ∃ f, (∀ ⦃x : X⦄, x ∈ sᶜ → ↑f x = 0) ∧ ↑f x ≠ 0
[PROOFSTEP]
obtain ⟨g, hgs, hgx : Set.EqOn g 1 { x }, -⟩ :=
  exists_continuous_zero_one_of_closed isClosed_closure isClosed_singleton (Set.disjoint_singleton_right.mpr hx)
[GOAL]
case intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
this : NormalSpace X
g : C(X, ℝ)
hgs : Set.EqOn (↑g) 0 (closure sᶜ)
hgx : Set.EqOn (↑g) 1 {x}
⊢ ∃ f, (∀ ⦃x : X⦄, x ∈ sᶜ → ↑f x = 0) ∧ ↑f x ≠ 0
[PROOFSTEP]
exact
  ⟨⟨fun x => g x, continuous_ofReal.comp (map_continuous g)⟩, by
    simpa only [coe_mk, ofReal_eq_zero] using fun x hx => hgs (subset_closure hx), by
    simpa only [coe_mk, hgx (Set.mem_singleton x), Pi.one_apply, IsROrC.ofReal_one] using one_ne_zero⟩
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
this : NormalSpace X
g : C(X, ℝ)
hgs : Set.EqOn (↑g) 0 (closure sᶜ)
hgx : Set.EqOn (↑g) 1 {x}
⊢ ∀ ⦃x : X⦄, x ∈ sᶜ → ↑(mk fun x => ↑(↑g x)) x = 0
[PROOFSTEP]
simpa only [coe_mk, ofReal_eq_zero] using fun x hx => hgs (subset_closure hx)
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
this : NormalSpace X
g : C(X, ℝ)
hgs : Set.EqOn (↑g) 0 (closure sᶜ)
hgx : Set.EqOn (↑g) 1 {x}
⊢ ↑(mk fun x => ↑(↑g x)) x ≠ 0
[PROOFSTEP]
simpa only [coe_mk, hgx (Set.mem_singleton x), Pi.one_apply, IsROrC.ofReal_one] using one_ne_zero
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Opens X
⊢ Ideal.IsMaximal (idealOfSet 𝕜 ↑s) ↔ IsCoatom s
[PROOFSTEP]
rw [Ideal.isMaximal_def]
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Opens X
⊢ IsCoatom (idealOfSet 𝕜 ↑s) ↔ IsCoatom s
[PROOFSTEP]
refine' (idealOpensGI X 𝕜).isCoatom_iff (fun I hI => _) s
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Opens X
I : Ideal C(X, 𝕜)
hI : IsCoatom I
⊢ idealOfSet 𝕜 ↑(opensOfIdeal I) = I
[PROOFSTEP]
rw [← Ideal.isMaximal_def] at hI
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Opens X
I : Ideal C(X, 𝕜)
hI : Ideal.IsMaximal I
⊢ idealOfSet 𝕜 ↑(opensOfIdeal I) = I
[PROOFSTEP]
exact idealOfSet_ofIdeal_isClosed inferInstance
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : Ideal.IsMaximal I
⊢ ∃ x, setOfIdeal I = {x}ᶜ
[PROOFSTEP]
have h : (idealOfSet 𝕜 (setOfIdeal I)).IsMaximal :=
  (idealOfSet_ofIdeal_isClosed (inferInstance : IsClosed (I : Set C(X, 𝕜)))).symm ▸ hI
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : Ideal.IsMaximal I
h : Ideal.IsMaximal (idealOfSet 𝕜 (setOfIdeal I))
⊢ ∃ x, setOfIdeal I = {x}ᶜ
[PROOFSTEP]
obtain ⟨x, hx⟩ := Opens.isCoatom_iff.1 ((idealOfSet_isMaximal_iff 𝕜 (opensOfIdeal I)).1 h)
[GOAL]
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : Ideal.IsMaximal I
h : Ideal.IsMaximal (idealOfSet 𝕜 (setOfIdeal I))
x : X
hx : opensOfIdeal I = Closeds.compl (Closeds.singleton x)
⊢ ∃ x, setOfIdeal I = {x}ᶜ
[PROOFSTEP]
refine ⟨x, congr_arg (fun (s : Opens X) => (s : Set X)) hx⟩
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
⊢ Ideal.IsMaximal I ↔ ∃ x, idealOfSet 𝕜 {x}ᶜ = I
[PROOFSTEP]
refine'
  ⟨_, fun h =>
    let ⟨x, hx⟩ := h
    hx ▸ idealOf_compl_singleton_isMaximal 𝕜 x⟩
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
⊢ Ideal.IsMaximal I → ∃ x, idealOfSet 𝕜 {x}ᶜ = I
[PROOFSTEP]
intro hI'
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
hI' : Ideal.IsMaximal I
⊢ ∃ x, idealOfSet 𝕜 {x}ᶜ = I
[PROOFSTEP]
obtain ⟨x, hx⟩ := setOfIdeal_eq_compl_singleton I
[GOAL]
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
hI' : Ideal.IsMaximal I
x : X
hx : setOfIdeal I = {x}ᶜ
⊢ ∃ x, idealOfSet 𝕜 {x}ᶜ = I
[PROOFSTEP]
exact
  ⟨x, by simpa only [idealOfSet_ofIdeal_eq_closure, I.closure_eq_of_isClosed hI] using congr_arg (idealOfSet 𝕜) hx.symm⟩
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
hI' : Ideal.IsMaximal I
x : X
hx : setOfIdeal I = {x}ᶜ
⊢ idealOfSet 𝕜 {x}ᶜ = I
[PROOFSTEP]
simpa only [idealOfSet_ofIdeal_eq_closure, I.closure_eq_of_isClosed hI] using congr_arg (idealOfSet 𝕜) hx.symm
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : CommRing 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : TopologicalRing 𝕜
inst✝¹ : Nontrivial 𝕜
inst✝ : NoZeroDivisors 𝕜
x : X
⊢ ContinuousLinearMap.mk
      {
        toAddHom :=
          { toFun := fun f => ↑f x,
            map_add' := (_ : ∀ (f g : C(X, 𝕜)), (fun f => ↑f x) (f + g) = (fun f => ↑f x) (f + g)) },
        map_smul' :=
          (_ :
            ∀ (z : 𝕜) (f : C(X, 𝕜)),
              AddHom.toFun
                  { toFun := fun f => ↑f x,
                    map_add' := (_ : ∀ (f g : C(X, 𝕜)), (fun f => ↑f x) (f + g) = (fun f => ↑f x) (f + g)) }
                  (z • f) =
                AddHom.toFun
                  { toFun := fun f => ↑f x,
                    map_add' := (_ : ∀ (f g : C(X, 𝕜)), (fun f => ↑f x) (f + g) = (fun f => ↑f x) (f + g)) }
                  (z • f)) } ∈
    characterSpace 𝕜 C(X, 𝕜)
[PROOFSTEP]
rw [CharacterSpace.eq_set_map_one_map_mul]
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : CommRing 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : TopologicalRing 𝕜
inst✝¹ : Nontrivial 𝕜
inst✝ : NoZeroDivisors 𝕜
x : X
⊢ ContinuousLinearMap.mk
      {
        toAddHom :=
          { toFun := fun f => ↑f x,
            map_add' := (_ : ∀ (f g : C(X, 𝕜)), (fun f => ↑f x) (f + g) = (fun f => ↑f x) (f + g)) },
        map_smul' :=
          (_ :
            ∀ (z : 𝕜) (f : C(X, 𝕜)),
              AddHom.toFun
                  { toFun := fun f => ↑f x,
                    map_add' := (_ : ∀ (f g : C(X, 𝕜)), (fun f => ↑f x) (f + g) = (fun f => ↑f x) (f + g)) }
                  (z • f) =
                AddHom.toFun
                  { toFun := fun f => ↑f x,
                    map_add' := (_ : ∀ (f g : C(X, 𝕜)), (fun f => ↑f x) (f + g) = (fun f => ↑f x) (f + g)) }
                  (z • f)) } ∈
    {φ | ↑φ 1 = 1 ∧ ∀ (x y : C(X, 𝕜)), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
exact ⟨rfl, fun f g => rfl⟩
[GOAL]
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : IsROrC 𝕜
⊢ Bijective ↑(continuousMapEval X 𝕜)
[PROOFSTEP]
refine' ⟨fun x y hxy => _, fun φ => _⟩
[GOAL]
case refine'_1
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : IsROrC 𝕜
x y : X
hxy : ↑(continuousMapEval X 𝕜) x = ↑(continuousMapEval X 𝕜) y
⊢ x = y
[PROOFSTEP]
contrapose! hxy
[GOAL]
case refine'_1
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : IsROrC 𝕜
x y : X
hxy : x ≠ y
⊢ ↑(continuousMapEval X 𝕜) x ≠ ↑(continuousMapEval X 𝕜) y
[PROOFSTEP]
haveI := @normalOfCompactT2 X _ _ _
[GOAL]
case refine'_1
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : IsROrC 𝕜
x y : X
hxy : x ≠ y
this : NormalSpace X
⊢ ↑(continuousMapEval X 𝕜) x ≠ ↑(continuousMapEval X 𝕜) y
[PROOFSTEP]
rcases exists_continuous_zero_one_of_closed (isClosed_singleton : _root_.IsClosed { x })
    (isClosed_singleton : _root_.IsClosed { y }) (Set.disjoint_singleton.mpr hxy) with
  ⟨f, fx, fy, -⟩
[GOAL]
case refine'_1.intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : IsROrC 𝕜
x y : X
hxy : x ≠ y
this : NormalSpace X
f : C(X, ℝ)
fx : Set.EqOn (↑f) 0 {x}
fy : Set.EqOn (↑f) 1 {y}
⊢ ↑(continuousMapEval X 𝕜) x ≠ ↑(continuousMapEval X 𝕜) y
[PROOFSTEP]
rw [FunLike.ne_iff]
[GOAL]
case refine'_1.intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : IsROrC 𝕜
x y : X
hxy : x ≠ y
this : NormalSpace X
f : C(X, ℝ)
fx : Set.EqOn (↑f) 0 {x}
fy : Set.EqOn (↑f) 1 {y}
⊢ ∃ a, ↑(↑(continuousMapEval X 𝕜) x) a ≠ ↑(↑(continuousMapEval X 𝕜) y) a
[PROOFSTEP]
use(⟨fun (x : ℝ) => (x : 𝕜), IsROrC.continuous_ofReal⟩ : C(ℝ, 𝕜)).comp f
[GOAL]
case h
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : IsROrC 𝕜
x y : X
hxy : x ≠ y
this : NormalSpace X
f : C(X, ℝ)
fx : Set.EqOn (↑f) 0 {x}
fy : Set.EqOn (↑f) 1 {y}
⊢ ↑(↑(continuousMapEval X 𝕜) x) (ContinuousMap.comp (mk fun x => ↑x) f) ≠
    ↑(↑(continuousMapEval X 𝕜) y) (ContinuousMap.comp (mk fun x => ↑x) f)
[PROOFSTEP]
simpa only [continuousMapEval_apply_apply, ContinuousMap.comp_apply, coe_mk, Ne.def, IsROrC.ofReal_inj] using
  ((fx (Set.mem_singleton x)).symm ▸ (fy (Set.mem_singleton y)).symm ▸ zero_ne_one : f x ≠ f y)
[GOAL]
case refine'_2
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : IsROrC 𝕜
φ : ↑(characterSpace 𝕜 C(X, 𝕜))
⊢ ∃ a, ↑(continuousMapEval X 𝕜) a = φ
[PROOFSTEP]
obtain ⟨x, hx⟩ := (ideal_isMaximal_iff (RingHom.ker φ)).mp inferInstance
[GOAL]
case refine'_2.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : IsROrC 𝕜
φ : ↑(characterSpace 𝕜 C(X, 𝕜))
x : X
hx : idealOfSet 𝕜 {x}ᶜ = RingHom.ker φ
⊢ ∃ a, ↑(continuousMapEval X 𝕜) a = φ
[PROOFSTEP]
refine' ⟨x, CharacterSpace.ext_ker <| Ideal.ext fun f => _⟩
[GOAL]
case refine'_2.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : IsROrC 𝕜
φ : ↑(characterSpace 𝕜 C(X, 𝕜))
x : X
hx : idealOfSet 𝕜 {x}ᶜ = RingHom.ker φ
f : C(X, 𝕜)
⊢ f ∈ RingHom.ker (↑(continuousMapEval X 𝕜) x) ↔ f ∈ RingHom.ker φ
[PROOFSTEP]
simpa only [RingHom.mem_ker, continuousMapEval_apply_apply, mem_idealOfSet_compl_singleton, RingHom.mem_ker] using
  SetLike.ext_iff.mp hx f


[GOAL]
X Y Z : TopCat
U : (Opens ↑X)ᵒᵖ
⊢ (map (𝟙 X)).op.obj U = U
[PROOFSTEP]
simp
[GOAL]
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ (map f).obj (iSup U) = iSup ((map f).toPrefunctor.obj ∘ U)
[PROOFSTEP]
ext1
[GOAL]
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑((map f).obj (iSup U)) = ↑(iSup ((map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
rw [iSup_def, iSup_def, map_obj]
[GOAL]
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑{ carrier := ↑f ⁻¹' ⋃ (i : ι), ↑(U i), is_open' := (_ : IsOpen (↑f ⁻¹' ⋃ (i : ι), ↑(U i))) } =
    ↑{ carrier := ⋃ (i : ι), ↑(((map f).toPrefunctor.obj ∘ U) i),
        is_open' := (_ : IsOpen (⋃ (i : ι), ↑(((map f).toPrefunctor.obj ∘ U) i))) }
[PROOFSTEP]
dsimp
[GOAL]
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑f ⁻¹' ⋃ (i : ι), ↑(U i) = ⋃ (i : ι), ↑((map f).obj (U i))
[PROOFSTEP]
rw [Set.preimage_iUnion]
[GOAL]
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ⋃ (i : ι), ↑f ⁻¹' ↑(U i) = ⋃ (i : ι), ↑((map f).obj (U i))
[PROOFSTEP]
rfl
[GOAL]
X Y Z : TopCat
⊢ map (𝟙 X) = 𝟭 (Opens ↑X)
[PROOFSTEP]
rfl
[GOAL]
X Y Z : TopCat
f g : X ⟶ Y
h : f = g
U : Opens ↑Y
⊢ (map f).obj U = (map g).obj U
[PROOFSTEP]
rw [congr_arg map h]
[GOAL]
X Y Z : TopCat
f g : X ⟶ Y
h : f = g
⊢ map f = map g
[PROOFSTEP]
subst h
[GOAL]
X Y Z : TopCat
f : X ⟶ Y
⊢ map f = map f
[PROOFSTEP]
rfl
[GOAL]
X Y Z : TopCat
f g : X ⟶ Y
h : f = g
U : Opens ↑Y
⊢ (map f).obj U = (map g).obj U
[PROOFSTEP]
rw [h]
[GOAL]
X Y Z : TopCat
f g : X ⟶ Y
h : f = g
U : Opens ↑Y
⊢ (map g).obj U = (map f).obj U
[PROOFSTEP]
rw [h]
[GOAL]
X✝ Y✝ Z X Y : TopCat
H : X ≅ Y
U : Opens ↑Y
⊢ (𝟭 (Opens ↑Y)).obj U = (map H.hom ⋙ map H.inv).obj U
[PROOFSTEP]
simp [map, Set.preimage_preimage]
[GOAL]
X✝ Y✝ Z X Y : TopCat
H : X ≅ Y
U : Opens ↑X
⊢ (map H.inv ⋙ map H.hom).obj U = (𝟭 (Opens ↑X)).obj U
[PROOFSTEP]
simp [map, Set.preimage_preimage]
[GOAL]
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
H : Mono f
X✝ Y✝ : Opens ↑X
i : (functor hf).obj X✝ ⟶ (functor hf).obj Y✝
x : ↑X
hx : x ∈ ↑X✝
⊢ x ∈ ↑Y✝
[PROOFSTEP]
obtain ⟨y, hy, eq⟩ := i.le ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
H : Mono f
X✝ Y✝ : Opens ↑X
i : (functor hf).obj X✝ ⟶ (functor hf).obj Y✝
x : ↑X
hx : x ∈ ↑X✝
y : (forget TopCat).obj X
hy : y ∈ ↑Y✝
eq : ↑f y = ↑f x
⊢ x ∈ ↑Y✝
[PROOFSTEP]
exact (TopCat.mono_iff_injective f).mp H eq ▸ hy
[GOAL]
X : TopCat
U : Opens ↑X
⊢ (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj ⊤ = U
[PROOFSTEP]
ext1
[GOAL]
case h
X : TopCat
U : Opens ↑X
⊢ ↑((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj ⊤) = ↑U
[PROOFSTEP]
exact Set.image_univ.trans Subtype.range_coe
[GOAL]
X : TopCat
U : Opens ↑X
⊢ (map (inclusion U)).obj U = ⊤
[PROOFSTEP]
ext1
[GOAL]
case h
X : TopCat
U : Opens ↑X
⊢ ↑((map (inclusion U)).obj U) = ↑⊤
[PROOFSTEP]
exact Subtype.coe_preimage_self _
[GOAL]
X : TopCat
U : Opens ↑X
⊢ (map (inclusion U) ⋙ IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj U = (𝟭 (Opens ↑X)).obj U
[PROOFSTEP]
simp
[GOAL]
X : TopCat
⊢ IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤)) = map (inclusionTopIso X).inv
[PROOFSTEP]
refine' CategoryTheory.Functor.ext _ _
[GOAL]
case refine'_1
X : TopCat
⊢ ∀ (X_1 : Opens ↑((toTopCat X).obj ⊤)),
    (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj X_1 = (map (inclusionTopIso X).inv).obj X_1
[PROOFSTEP]
intro U
[GOAL]
case refine'_1
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
⊢ (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj U = (map (inclusionTopIso X).inv).obj U
[PROOFSTEP]
ext x
[GOAL]
case refine'_1.h.h
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
x : ↑X
⊢ x ∈ ↑((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj U) ↔ x ∈ ↑((map (inclusionTopIso X).inv).obj U)
[PROOFSTEP]
exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨x, trivial⟩, h, rfl⟩⟩
[GOAL]
case refine'_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).map f =
      eqToHom (_ : (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj X_1 = (map (inclusionTopIso X).inv).obj X_1) ≫
        (map (inclusionTopIso X).inv).map f ≫
          eqToHom (_ : (map (inclusionTopIso X).inv).obj Y = (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj Y)
[PROOFSTEP]
intros U V f
[GOAL]
case refine'_2
X : TopCat
U V : Opens ↑((toTopCat X).obj ⊤)
f : U ⟶ V
⊢ (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).map f =
    eqToHom (_ : (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj U = (map (inclusionTopIso X).inv).obj U) ≫
      (map (inclusionTopIso X).inv).map f ≫
        eqToHom (_ : (map (inclusionTopIso X).inv).obj V = (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj V)
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
U : Opens ↑Y
⊢ (IsOpenMap.functor hf).obj ((map f).obj U) = (IsOpenMap.functor hf).obj ⊤ ⊓ U
[PROOFSTEP]
ext
[GOAL]
case h.h
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U)) ↔ x✝ ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U)
[PROOFSTEP]
constructor
[GOAL]
case h.h.mp
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U)) → x✝ ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U)
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case h.h.mp.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
U : Opens ↑Y
x : (forget TopCat).obj X
hx : x ∈ ↑((map f).obj U)
⊢ ↑f x ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U)
[PROOFSTEP]
exact ⟨⟨x, trivial, rfl⟩, hx⟩
[GOAL]
case h.h.mpr
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U) → x✝ ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U))
[PROOFSTEP]
rintro ⟨⟨x, -, rfl⟩, hx⟩
[GOAL]
case h.h.mpr.intro.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
U : Opens ↑Y
x : (forget TopCat).obj X
hx : ↑f x ∈ ↑U
⊢ ↑f x ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U))
[PROOFSTEP]
exact ⟨x, hx, rfl⟩
[GOAL]
X : TopCat
U : Opens ↑X
⊢ Set.range ((forget TopCat).map (inclusion U)) = ↑U
[PROOFSTEP]
ext x
[GOAL]
case h
X : TopCat
U : Opens ↑X
x : (forget TopCat).obj X
⊢ x ∈ Set.range ((forget TopCat).map (inclusion U)) ↔ x ∈ ↑U
[PROOFSTEP]
constructor
[GOAL]
case h.mp
X : TopCat
U : Opens ↑X
x : (forget TopCat).obj X
⊢ x ∈ Set.range ((forget TopCat).map (inclusion U)) → x ∈ ↑U
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case h.mp.intro
X : TopCat
U : Opens ↑X
x : (forget TopCat).obj ((toTopCat X).obj U)
⊢ (forget TopCat).map (inclusion U) x ∈ ↑U
[PROOFSTEP]
exact x.2
[GOAL]
case h.mpr
X : TopCat
U : Opens ↑X
x : (forget TopCat).obj X
⊢ x ∈ ↑U → x ∈ Set.range ((forget TopCat).map (inclusion U))
[PROOFSTEP]
intro h
[GOAL]
case h.mpr
X : TopCat
U : Opens ↑X
x : (forget TopCat).obj X
h : x ∈ ↑U
⊢ x ∈ Set.range ((forget TopCat).map (inclusion U))
[PROOFSTEP]
exact ⟨⟨x, h⟩, rfl⟩
[GOAL]
X : TopCat
U V : Opens ↑X
⊢ (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj ((map (inclusion U)).obj V) = V ⊓ U
[PROOFSTEP]
ext1
[GOAL]
case h
X : TopCat
U V : Opens ↑X
⊢ ↑((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj ((map (inclusion U)).obj V)) = ↑(V ⊓ U)
[PROOFSTEP]
refine' Set.image_preimage_eq_inter_range.trans _
[GOAL]
case h
X : TopCat
U V : Opens ↑X
⊢ (V.1 ∩ Set.range fun x => ↑(inclusion U) x) = ↑(V ⊓ U)
[PROOFSTEP]
erw [set_range_forget_map_inclusion U]
[GOAL]
case h
X : TopCat
U V : Opens ↑X
⊢ V.1 ∩ ↑U = ↑(V ⊓ U)
[PROOFSTEP]
rfl
[GOAL]
X : TopCat
U : Opens ↑X
V : Opens { x // x ∈ U }
⊢ (map (inclusion U) ⋙ IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj
      ((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V) =
    (𝟭 (Opens ↑X)).obj ((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V)
[PROOFSTEP]
dsimp
[GOAL]
X : TopCat
U : Opens ↑X
V : Opens { x // x ∈ U }
⊢ (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj
      ((map (inclusion U)).obj ((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V)) =
    (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V
[PROOFSTEP]
rw [map_functor_eq V]
[GOAL]
X : TopCat
U : Opens ↑X
V : Opens { x // x ∈ U }
⊢ NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑(inclusion U))).counit
      ((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V) =
    eqToHom
      (_ :
        (map (inclusion U) ⋙ IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj
            ((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V) =
          (𝟭 (Opens ↑X)).obj ((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V))
[PROOFSTEP]
apply Subsingleton.elim