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)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
x : X
simp :
  ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ <
    ε
⊢ nnnorm.{u_2} (E := 𝕜) ((f - f * comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜) < ε

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

Premises used: Pi.mul_apply, ContinuousMap.coe_sub, ContinuousMap.coe_mul, Pi.sub_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)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
x : X
pos :
  ∀ (hx : x ∈ t),
    ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
            ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ <
      ε
neg :
  ∀ (hx : x ∉ t),
    ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
            ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ <
      ε
⊢ ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ <
    ε

Tactic:
by_cases hx : x ∈ t
-- 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)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
x : X
hx : x ∈ t
⊢ ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ <
    ε

Tactic:
simpa only [hgt hx, comp_apply, Pi.one_apply, ContinuousMap.coe_coe, algebraMapCLM_apply,
        map_one, mul_one, sub_self, nnnorm_zero] using hε

Premises used: sub_self, Pi.one_apply, ContinuousMap.comp_apply, nnnorm_zero, algebraMapCLM_apply, map_one, ContinuousMap.coe_coe, mul_one
-- 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)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
x : X
hx : x ∉ t
⊢ ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ <
    ε

Tactic:
lt_of_le_of_lt ?_ (half_lt_self hε)

Premises used: half_lt_self, lt_of_le_of_lt
-- 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)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
x : X
hx : x ∉ t
neg :
  ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ ≤
    ε / 2
⊢ ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ <
    ε

Tactic:
refine lt_of_le_of_lt ?_ (half_lt_self hε)

Premises used: half_lt_self, lt_of_le_of_lt
-- 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)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
x : X
hx : x ∉ t
⊢ nnnorm.{u_2} (E := 𝕜)
      ((HSub.hSub (α := C(X, 𝕜)) 1 (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) : (a : X) → 𝕜) x : 𝕜) =
    ‖HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((algebraMap ℝ≥0 𝕜 : (a : ℝ≥0) → 𝕜) ((g : (a : X) → ℝ≥0) x : ℝ≥0) : 𝕜)‖₊

Tactic:
simp only [coe_sub, coe_one, coe_comp, ContinuousMap.coe_coe, Pi.sub_apply,
              Pi.one_apply, Function.comp_apply, algebraMapCLM_apply]

Premises used: Pi.one_apply, ContinuousMap.coe_comp, ContinuousMap.coe_sub, algebraMapCLM_apply, ContinuousMap.coe_coe, Function.comp_apply, ContinuousMap.coe_one, Pi.sub_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)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
x : X
hx : x ∉ t
⊢ ‖HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((algebraMap ℝ≥0 𝕜 : (a : ℝ≥0) → 𝕜) ((g : (a : X) → ℝ≥0) x : ℝ≥0) : 𝕜)‖₊ =
    nnnorm (E := 𝕜)
      ((algebraMap ℝ≥0 𝕜 : (a : ℝ≥0) → 𝕜) (HSub.hSub (α := ℝ≥0) (β := ℝ≥0) (1 : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)) : 𝕜)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, NNReal.smul_def, NNReal.coe_sub (hg x),
              NNReal.coe_one, sub_smul, one_smul]

Premises used: sub_smul, one_smul, Algebra.algebraMap_eq_smul_one, NNReal.smul_def, NNReal.coe_one, NNReal.coe_sub
-- 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)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
x : X
hx : x ∉ t
⊢ nnnorm.{u_2} (E := 𝕜)
      ((HSub.hSub (α := C(X, 𝕜)) 1 (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) : (a : X) → 𝕜) x : 𝕜) ≤
    1

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
-- 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)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
x : X
hx : x ∉ t
this :
  nnnorm.{u_2} (E := 𝕜)
      ((HSub.hSub (α := C(X, 𝕜)) 1 (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) : (a : X) → 𝕜) x : 𝕜) ≤
    1
⊢ ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ =
    ‖HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        ((HSub.hSub (α := C(X, 𝕜)) 1 (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) : (a : X) → 𝕜) x : 𝕜)‖₊

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

Premises used: mul_sub, Pi.one_apply, ContinuousMap.coe_sub, mul_one, ContinuousMap.coe_one, Pi.sub_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)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
x : X
hx : x ∉ t
this :
  nnnorm.{u_2} (E := 𝕜)
      ((HSub.hSub (α := C(X, 𝕜)) 1 (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) : (a : X) → 𝕜) x : 𝕜) ≤
    1
⊢ ‖HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        ((HSub.hSub (α := C(X, 𝕜)) 1 (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) : (a : X) → 𝕜) x : 𝕜)‖₊ ≤
    ε / 2 *
      nnnorm.{u_2} (E := 𝕜)
        ((HSub.hSub (α := C(X, 𝕜)) 1 (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) : (a : X) → 𝕜) x : 𝕜)

Tactic:
((nnnorm_mul_le _ _).trans
            (mul_le_mul_left (not_le.mp <| show ¬ε / 2 ≤ ‖f x‖₊ from hx).le _))

Premises used: not_le, nnnorm_mul_le, LT.lt.le, mul_le_mul_left, Iff.mp, LE.le.trans
-- 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)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
x : X
hx : x ∉ t
this :
  nnnorm.{u_2} (E := 𝕜)
      ((HSub.hSub (α := C(X, 𝕜)) 1 (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) : (a : X) → 𝕜) x : 𝕜) ≤
    1
⊢ ε / 2 *
      nnnorm.{u_2} (E := 𝕜)
        ((HSub.hSub (α := C(X, 𝕜)) 1 (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) : (a : X) → 𝕜) x : 𝕜) ≤
    ε / 2

Tactic:
simpa only [mul_one] using mul_le_mul_right this _

Premises used: mul_le_mul_right, mul_one
-- 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)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
x : X
hx : x ∉ t
this :
  nnnorm.{u_2} (E := 𝕜)
      ((HSub.hSub (α := C(X, 𝕜)) 1 (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) : (a : X) → 𝕜) x : 𝕜) ≤
    1
x₁ :
  ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ =
    ‖HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        ((HSub.hSub (α := C(X, 𝕜)) 1 (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) : (a : X) → 𝕜) x : 𝕜)‖₊
x₂ :
  ε / 2 *
      nnnorm.{u_2} (E := 𝕜)
        ((HSub.hSub (α := C(X, 𝕜)) 1 (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) : (a : X) → 𝕜) x : 𝕜) ≤
    ε / 2
⊢ ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ ≤
    ε / 2

Tactic:
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_left (not_le.mp <| show ¬ε / 2 ≤ ‖f x‖₊ from hx).le _))
        _ ≤ ε / 2 := by simpa only [mul_one] using mul_le_mul_right this _

Premises used: not_le, nnnorm_mul_le, algebraMapCLM, HSub.hSub, ContinuousMap.comp, LT.lt.le, NNReal, toContinuousMap, mul_le_mul_left, Iff.mp, LE.le.trans, OfNat.ofNat, DFunLike.coe
-- 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)ᶜ
g :
  ∃ (g : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I ∧
      (∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)) ∧
        Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
⊢ ∃ b ∈ (↑I : Set C(X, 𝕜)), nndist f b < ε

Tactic:
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, 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_left (not_le.mp <| show ¬ε / 2 ≤ ‖f x‖₊ from hx).le _))
        _ ≤ ε / 2 := by simpa only [mul_one] using mul_le_mul_right this _
-- 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)ᶜ
⊢ ∃ (g' : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
ht.isCompact.induction_on ?_ ?_ ?_ ?_

Premises used: IsClosed.isCompact, IsCompact.induction_on
-- 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)ᶜ
refine_1 :
  ∃ (g' : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ (x : X), Membership.mem (γ := Set X) ∅ x → LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
refine_2 :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t →
      (∃ (g' : C(X, ℝ≥0)),
          comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
            ∀ x ∈ t, 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)
refine_3 :
  ∀ ⦃s t : Set X⦄,
    (∃ (g' : C(X, ℝ≥0)),
        comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
          ∀ 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 ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)) →
        ∃ (g' : C(X, ℝ≥0)),
          comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
            ∀ x ∈ s ∪ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
refine_4 :
  ∀ x ∈ t,
    ∃ 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)
⊢ ∃ (g' : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
refine ht.isCompact.induction_on ?_ ?_ ?_ ?_
-- 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)ᶜ
⊢ ∃ (g' : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ (x : X), Membership.mem (γ := Set X) ∅ x → LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)

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

Premises used: False.elim, And.intro, Exists.intro, OfNat.ofNat
-- 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)ᶜ
refine_1 : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) 0 ∈ I
⊢ ∃ (g' : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ (x : X), Membership.mem (γ := Set X) ∅ x → LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
refine ⟨0, ?_, fun x hx => False.elim 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)ᶜ
⊢ 0 ∈ I

Tactic:
I.zero_mem

Premises used: Ideal.zero_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)ᶜ
h : Eq (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) 0) 0
⊢ comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) 0 ∈ I

Tactic:
convert! I.zero_mem

Premises used: Ideal.zero_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)ᶜ
h :
  ∀ (a : X),
    Eq.{u_2 + 1} (α := 𝕜) ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) 0 : (a : X) → 𝕜) a : 𝕜) ((0 : (a : X) → 𝕜) a : 𝕜)
⊢ Eq (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) 0) 0

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)ᶜ
a : X
⊢ Eq.{u_2 + 1} (α := 𝕜) ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) 0 : (a : X) → 𝕜) a : 𝕜) ((0 : (a : X) → 𝕜) a : 𝕜)

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

Premises used: map_zero, ContinuousMap.comp_apply, ContinuousMap.zero_apply, ContinuousMap.coe_coe