awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
hs : s₁ ⊆ s₂
g : C(X, ℝ≥0)
hI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hgt : ∀ x ∈ s₂, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ ∃ (g' : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ x ∈ s₁, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
⟨g, hI, fun x hx => hgt x (hs hx)⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
hs : s₁ ⊆ s₂
g : C(X, ℝ≥0)
hI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hgt : ∀ x ∈ s₂, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ ∃ (g' : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ x ∈ s₁, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
exact ⟨g, hI, fun x hx => hgt x (hs hx)⟩
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ : (a : X) → ℝ≥0) x : ℝ≥0)
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ ∃ (g' : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ x ∈ s₁ ∪ s₂, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
⟨g₁ + g₂, ?_, fun x hx => ?_⟩

Premises used: HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ : (a : X) → ℝ≥0) x : ℝ≥0)
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
refine_3 : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g₁ + g₂) ∈ I
refine_3₁ : ∀ (x : X) (hx : x ∈ s₁ ∪ s₂), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ + g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ ∃ (g' : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ x ∈ s₁ ∪ s₂, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
refine ⟨g₁ + g₂, ?_, fun x hx => ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ : (a : X) → ℝ≥0) x : ℝ≥0)
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ HAdd.hAdd (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁)
      (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂) ∈
    I

Tactic:
I.add_mem hI₁ hI₂

Premises used: Ideal.add_mem
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ : (a : X) → ℝ≥0) x : ℝ≥0)
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
h :
  comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g₁ + g₂) =
    HAdd.hAdd (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁)
      (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂)
⊢ comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g₁ + g₂) ∈ I

Tactic:
convert! I.add_mem hI₁ hI₂

Premises used: Ideal.add_mem
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ : (a : X) → ℝ≥0) x : ℝ≥0)
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
h :
  ∀ (y : X),
    Eq.{u_2 + 1} (α := 𝕜) ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g₁ + g₂) : (a : X) → 𝕜) y : 𝕜)
      ((HAdd.hAdd (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁)
              (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂) :
            (a : X) → 𝕜)
          y :
        𝕜)
⊢ comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g₁ + g₂) =
    HAdd.hAdd (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁)
      (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂)

Tactic:
ext y
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ : (a : X) → ℝ≥0) x : ℝ≥0)
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
y : X
⊢ Eq.{u_2 + 1} (α := 𝕜) ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g₁ + g₂) : (a : X) → 𝕜) y : 𝕜)
    ((HAdd.hAdd (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁)
            (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂) :
          (a : X) → 𝕜)
        y :
      𝕜)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ : (a : X) → ℝ≥0) x : ℝ≥0)
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
x : X
hx : x ∈ s₁ ∪ s₂
refine_3 : ∀ (hx : x ∈ s₁), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ + g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
refine_3₁ : ∀ (hx : x ∈ s₂), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ + g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ + g₂ : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
rcases hx with (hx | hx)
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ : (a : X) → ℝ≥0) x : ℝ≥0)
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
x : X
hx : x ∈ s₁
⊢ LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ + g₂ : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
simpa only [zero_add] using add_lt_add_of_lt_of_le (hgt₁ x hx) zero_le'

Premises used: zero_add, add_lt_add_of_lt_of_le, zero_le'
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
s₁ s₂ : Set X
g₁ : C(X, ℝ≥0)
hI₁ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁ ∈ I
hgt₁ : ∀ x ∈ s₁, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ : (a : X) → ℝ≥0) x : ℝ≥0)
g₂ : C(X, ℝ≥0)
hI₂ : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂ ∈ I
hgt₂ : ∀ x ∈ s₂, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
x : X
hx : x ∈ s₂
⊢ LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ + g₂ : (a : X) → ℝ≥0) x : ℝ≥0)

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

Premises used: add_lt_add_of_le_of_lt, zero_add, zero_le'
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
hx : x ∈ t
⊢ x ∈ (setOfIdeal I)ᶜᶜ

Tactic:
replace hx := htI.subset_compl_right hx
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
hx : x ∈ (setOfIdeal I)ᶜᶜ
⊢ ∃ f ∈ I, Ne.{u_2 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
rw [compl_compl, mem_setOfIdeal] at hx

Premises used: compl_compl, ContinuousMap.mem_setOfIdeal
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
hx : ∃ f ∈ I, Ne.{u_2 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)
refine_4 :
  ∀ (g : C(X, 𝕜)) (hI : g ∈ I) (hgx : Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)),
    ∃ t_1 ∈ nhdsWithin x t,
      ∃ (g' : C(X, ℝ≥0)),
        comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
          ∀ x ∈ t_1, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ ∃ t_1 ∈ nhdsWithin x t,
    ∃ (g' : C(X, ℝ≥0)),
      comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
        ∀ x ∈ t_1, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
obtain ⟨g, hI, hgx⟩ := hx
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ ∀ᶠ (z : X) in nhds x, Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) z : 𝕜) (0 : 𝕜)

Tactic:
have := (map_continuous g).continuousAt.eventually_ne hgx
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)
this : ∀ᶠ (z : X) in nhds x, Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) z : 𝕜) (0 : 𝕜)
⊢ ∃ t_1 ∈ nhdsWithin x t,
    ∃ (g' : C(X, ℝ≥0)),
      comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
        ∀ x ∈ t_1, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
⟨{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⟩⟩

Premises used: Iff.mpr, norm_pos_iff, pow_pos, ContinuousMap.mk, NNNorm.nnnorm, setOf, Continuous.pow, Ne, Inter.inter, Set.Subset.rfl, HPow.hPow, And.left, And.intro, Exists.intro, Continuous.nnnorm, ContinuousMapClass.map_continuous, OfNat.ofNat, DFunLike.coe, mem_nhdsWithin_iff_exists_mem_nhds_inter
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)
this : ∀ᶠ (z : X) in nhds x, Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) z : 𝕜) (0 : 𝕜)
refine_4 :
  comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜))
      { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (nnnorm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜)) 2,
        continuous_toFun := ⋯ : C(X, ℝ≥0) } ∈
    I
⊢ ∃ t_1 ∈ nhdsWithin x t,
    ∃ (g' : C(X, ℝ≥0)),
      comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
        ∀ x ∈ t_1, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
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⟩⟩
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)
this : ∀ᶠ (z : X) in nhds x, Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) z : 𝕜) (0 : 𝕜)
⊢ star g * g ∈ I

Tactic:
I.mul_mem_left (star g) hI

Premises used: Ideal.mul_mem_left, Star.star
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)
this : ∀ᶠ (z : X) in nhds x, Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) z : 𝕜) (0 : 𝕜)
h :
  comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜))
      { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (nnnorm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜)) 2,
        continuous_toFun := ⋯ : C(X, ℝ≥0) } =
    star g * g
⊢ comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜))
      { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (nnnorm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜)) 2,
        continuous_toFun := ⋯ : C(X, ℝ≥0) } ∈
    I

Tactic:
convert! I.mul_mem_left (star g) hI

Premises used: Ideal.mul_mem_left, Star.star
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)
this : ∀ᶠ (z : X) in nhds x, Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) z : 𝕜) (0 : 𝕜)
h :
  ∀ (a : X),
    Eq.{u_2 + 1} (α := 𝕜)
      ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜))
              { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (nnnorm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜)) 2,
                continuous_toFun := ⋯ : C(X, ℝ≥0) } :
            (a : X) → 𝕜)
          a :
        𝕜)
      ((star g * g : (a : X) → 𝕜) a : 𝕜)
⊢ comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜))
      { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (nnnorm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜)) 2,
        continuous_toFun := ⋯ : C(X, ℝ≥0) } =
    star g * g

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)
this : ∀ᶠ (z : X) in nhds x, Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) z : 𝕜) (0 : 𝕜)
a : X
h :
  HPow.hPow (α := 𝕜) (β := ℕ) ((algebraMap ℝ≥0 𝕜 : (a : ℝ≥0) → 𝕜) (nnnorm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) a : 𝕜)) : 𝕜)
      2 =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((g : (a : X) → 𝕜) a : 𝕜) : 𝕜) ((g : (a : X) → 𝕜) a : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜)
    ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜))
            { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (nnnorm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜)) 2,
              continuous_toFun := ⋯ : C(X, ℝ≥0) } :
          (a : X) → 𝕜)
        a :
      𝕜)
    ((star g * g : (a : X) → 𝕜) a : 𝕜)

Tactic:
simp only [comp_apply, ContinuousMap.coe_coe, coe_mk, algebraMapCLM_apply, map_pow,
        mul_apply, star_apply, star_def]

Premises used: RCLike.star_def, ContinuousMap.comp_apply, map_pow, algebraMapCLM_apply, ContinuousMap.star_apply, ContinuousMap.coe_mk, ContinuousMap.coe_coe, ContinuousMap.mul_apply
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)
this : ∀ᶠ (z : X) in nhds x, Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) z : 𝕜) (0 : 𝕜)
a : X
h :
  HPow.hPow (α := 𝕜) (β := ℕ) ((algebraMap ℝ≥0 𝕜 : (a : ℝ≥0) → 𝕜) (nnnorm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) a : 𝕜)) : 𝕜)
      2 =
    HPow.hPow (α := 𝕜) (β := ℕ) (↑(norm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) a : 𝕜)) : 𝕜) 2
⊢ HPow.hPow (α := 𝕜) (β := ℕ) ((algebraMap ℝ≥0 𝕜 : (a : ℝ≥0) → 𝕜) (nnnorm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) a : 𝕜)) : 𝕜)
      2 =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((g : (a : X) → 𝕜) a : 𝕜) : 𝕜) ((g : (a : X) → 𝕜) a : 𝕜)

Tactic:
simp only [RCLike.conj_mul]

Premises used: RCLike.conj_mul
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
g : C(X, 𝕜)
hI : g ∈ I
hgx : Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)
this : ∀ᶠ (z : X) in nhds x, Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) z : 𝕜) (0 : 𝕜)
a : X
⊢ HPow.hPow (α := 𝕜) (β := ℕ) ((algebraMap ℝ≥0 𝕜 : (a : ℝ≥0) → 𝕜) (nnnorm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) a : 𝕜)) : 𝕜)
      2 =
    HPow.hPow (α := 𝕜) (β := ℕ) (↑(norm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) a : 𝕜)) : 𝕜) 2

Tactic:
rfl