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)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
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
      · 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_apply, map_pow,
        mul_apply, star_apply, star_def]
      simp only [RCLike.conj_mul]
      rfl
-- 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)ᶜ
this :
  ∃ (g' : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
obtain :
  ∀ (g' : C(X, ℝ≥0)) (hI' : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I)
    (hgt' : ∀ 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 : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)) ∧
          Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
⊢ ∃ (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

Tactic:
obtain ⟨g', hI', hgt'⟩ := 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)
hI' : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I
hgt' : ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
ht' : t = ∅
y : X
hy : y ∈ t
rwa rwa₁ rwa₂ rwa₃ : ∀ (hy : Membership.mem (γ := Set X) ∅ y), False
⊢ False

Tactic:
rwa [ht'] at hy
-- 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)
hI' : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I
hgt' : ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
obtain :
  ∀ (c : ℝ≥0) (hc : c > 0) (hgc' : t ⊆ {y : X | c ≤ (g' : (a : X) → ℝ≥0) y}),
    ∃ (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
⊢ ∃ (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

Tactic:
obtain ⟨c, hc, hgc'⟩ : ∃ c > 0, t ⊆ {y | 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_isMinOn ht' (map_continuous g').continuousOn
      ⟨g' x, hgt' x hx, hx'⟩

Premises used: Set.eq_empty_or_nonempty, Or.elim
-- 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)
hI' : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I
hgt' : ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
c : ℝ≥0
hc : c > 0
hgc' : t ⊆ {y : X | c ≤ (g' : (a : X) → ℝ≥0) y}
obtain :
  ∀ (g : C(X, ℝ≥0)) (hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g * g' : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0))
    (hgc : Set.EqOn (α := X) (β := ℝ≥0) (⇑(g * g') : (a : X) → ℝ≥0) 1 {x : X | c ≤ (g' : (a : X) → ℝ≥0) x}),
    ∃ (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
⊢ ∃ (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

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

Premises used: ContinuousMap.exists_mul_le_one_eqOn_ge
-- 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)
hI' : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I
hgt' : ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
c : ℝ≥0
hc : c > 0
hgc' : t ⊆ {y : X | c ≤ (g' : (a : X) → ℝ≥0) y}
g : C(X, ℝ≥0)
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g * g' : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgc : Set.EqOn (α := X) (β := ℝ≥0) (⇑(g * g') : (a : X) → ℝ≥0) 1 {x : X | c ≤ (g' : (a : X) → ℝ≥0) x}
⊢ ∃ (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

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

Premises used: HMul.hMul, And.intro, Exists.intro, Set.EqOn.mono
-- 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)
hI' : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I
hgt' : ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
c : ℝ≥0
hc : c > 0
hgc' : t ⊆ {y : X | c ≤ (g' : (a : X) → ℝ≥0) y}
g : C(X, ℝ≥0)
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g * g' : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgc : Set.EqOn (α := X) (β := ℝ≥0) (⇑(g * g') : (a : X) → ℝ≥0) 1 {x : X | c ≤ (g' : (a : X) → ℝ≥0) x}
refine : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g * g') ∈ I
⊢ ∃ (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

Tactic:
refine ⟨g * g', ?_, hg, hgc.mono hgc'⟩
-- 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)
hI' : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I
hgt' : ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
c : ℝ≥0
hc : c > 0
hgc' : t ⊆ {y : X | c ≤ (g' : (a : X) → ℝ≥0) y}
g : C(X, ℝ≥0)
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g * g' : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgc : Set.EqOn (α := X) (β := ℝ≥0) (⇑(g * g') : (a : X) → ℝ≥0) 1 {x : X | c ≤ (g' : (a : X) → ℝ≥0) x}
⊢ HMul.hMul (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g)
      (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g') ∈
    I

Tactic:
I.mul_mem_left ((algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) hI'

Premises used: algebraMapCLM, ContinuousMap.comp, NNReal, toContinuousMap, Ideal.mul_mem_left
-- 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)
hI' : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I
hgt' : ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
c : ℝ≥0
hc : c > 0
hgc' : t ⊆ {y : X | c ≤ (g' : (a : X) → ℝ≥0) y}
g : C(X, ℝ≥0)
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g * g' : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgc : Set.EqOn (α := X) (β := ℝ≥0) (⇑(g * g') : (a : X) → ℝ≥0) 1 {x : X | c ≤ (g' : (a : X) → ℝ≥0) x}
h :
  comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g * g') =
    HMul.hMul (α := 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.mul_mem_left ((algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) hI'

Premises used: algebraMapCLM, ContinuousMap.comp, NNReal, toContinuousMap, Ideal.mul_mem_left
-- 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)
hI' : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I
hgt' : ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
c : ℝ≥0
hc : c > 0
hgc' : t ⊆ {y : X | c ≤ (g' : (a : X) → ℝ≥0) y}
g : C(X, ℝ≥0)
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g * g' : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgc : Set.EqOn (α := X) (β := ℝ≥0) (⇑(g * g') : (a : X) → ℝ≥0) 1 {x : X | c ≤ (g' : (a : X) → ℝ≥0) x}
h :
  ∀ (a : X),
    Eq.{u_2 + 1} (α := 𝕜) ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g * g') : (a : X) → 𝕜) a : 𝕜)
      ((HMul.hMul (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g)
              (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g') :
            (a : X) → 𝕜)
          a :
        𝕜)
⊢ comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g * g') =
    HMul.hMul (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g)
      (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) 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)ᶜ
g' : C(X, ℝ≥0)
hI' : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I
hgt' : ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
c : ℝ≥0
hc : c > 0
hgc' : t ⊆ {y : X | c ≤ (g' : (a : X) → ℝ≥0) y}
g : C(X, ℝ≥0)
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g * g' : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgc : Set.EqOn (α := X) (β := ℝ≥0) (⇑(g * g') : (a : X) → ℝ≥0) 1 {x : X | c ≤ (g' : (a : X) → ℝ≥0) x}
a : X
⊢ Eq.{u_2 + 1} (α := 𝕜) ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g * g') : (a : X) → 𝕜) a : 𝕜)
    ((HMul.hMul (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g)
            (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g') :
          (a : X) → 𝕜)
        a :
      𝕜)

Tactic:
simp only [coe_algebraMapCLM, comp_apply, mul_apply, ContinuousMap.coe_coe, map_mul]

Premises used: coe_algebraMapCLM, ContinuousMap.comp_apply, map_mul, 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, 𝕜)
hI : IsClosed (↑I : Set C(X, 𝕜))
⊢ idealOfSet 𝕜 (setOfIdeal I) = I

Tactic:
(idealOfSet_ofIdeal_eq_closure I).trans (Ideal.ext <| Set.ext_iff.mp hI.closure_eq)

Premises used: IsClosed.closure_eq, Ideal.ext, Iff.mp, Set.ext_iff, ContinuousMap.idealOfSet_ofIdeal_eq_closure, Eq.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
s : Set X
⊢ setOfIdeal (idealOfSet 𝕜 s) = interior s

Tactic:
Set.Subset.antisymm
      ((setOfIdeal_open (idealOfSet 𝕜 s)).subset_interior_iff.mpr fun x hx =>
        let ⟨f, hf, hfx⟩ := mem_setOfIdeal.mp hx
        Set.notMem_compl_iff.mp (mt (@hf x) hfx))
      fun x hx => ?_

Premises used: Set.Subset.antisymm, Iff.mpr, Membership.mem, mt, IsOpen.subset_interior_iff, ContinuousMap.idealOfSet, _private.0.ContinuousMap.setOfIdeal_ofSet_eq_interior.match_1, Set.notMem_compl_iff, Iff.mp, ContinuousMap.mem_setOfIdeal, ContinuousMap.setOfIdeal_open
-- 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
s : Set X
𝕜₁ : ∀ (x : X) (hx : x ∈ interior s), x ∈ setOfIdeal (idealOfSet 𝕜 s)
⊢ setOfIdeal (idealOfSet 𝕜 s) = interior s

Tactic:
refine
    Set.Subset.antisymm
      ((setOfIdeal_open (idealOfSet 𝕜 s)).subset_interior_iff.mpr fun x hx =>
        let ⟨f, hf, hfx⟩ := mem_setOfIdeal.mp hx
        Set.notMem_compl_iff.mp (mt (@hf x) hfx))
      fun x hx => ?_

Premises used: Set.Subset.antisymm, Iff.mpr, Membership.mem, mt, IsOpen.subset_interior_iff, ContinuousMap.idealOfSet, _private.0.ContinuousMap.setOfIdeal_ofSet_eq_interior.match_1, Set.notMem_compl_iff, Iff.mp, ContinuousMap.mem_setOfIdeal, ContinuousMap.setOfIdeal_open
-- 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
s : Set X
x : X
hx : x ∈ interior s
⊢ x ∈ (closure sᶜ)ᶜ

Tactic:
rw [← compl_compl (interior s), ← closure_compl] at hx

Premises used: compl_compl, closure_compl, interior
-- 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
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
simp_rw :
  ∃ (f : C(X, 𝕜)),
    (∀ ⦃x : X⦄, x ∈ sᶜ → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)) ∧
      Ne.{u_2 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ x ∈ setOfIdeal (idealOfSet 𝕜 s)

Tactic:
simp_rw [mem_setOfIdeal, mem_idealOfSet]

Premises used: ContinuousMap.mem_idealOfSet, 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
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
obtain :
  ∀ (g : C(X, ℝ)) (hgs : Set.EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 (closure sᶜ))
    (hgx : Set.EqOn (α := X) (β := ℝ) (⇑g : (a : X) → ℝ) 1 {x}),
    ∃ (f : C(X, 𝕜)),
      (∀ ⦃x : X⦄, x ∈ sᶜ → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)) ∧
        Ne.{u_2 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ ∃ (f : C(X, 𝕜)),
    (∀ ⦃x : X⦄, x ∈ sᶜ → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)) ∧
      Ne.{u_2 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
obtain ⟨g, hgs, hgx : Set.EqOn g 1 {x}, -⟩ :=
    exists_continuous_zero_one_of_isClosed isClosed_closure isClosed_singleton
      (Set.disjoint_singleton_right.mpr hx)

Premises used: Iff.mpr, Set.disjoint_singleton_right, exists_continuous_zero_one_of_isClosed, isClosed_closure, isClosed_singleton
-- 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
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
g : C(X, ℝ)
hgs : Set.EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 (closure sᶜ)
hgx : Set.EqOn (α := X) (β := ℝ) (⇑g : (a : X) → ℝ) 1 {x}
⊢ ∀ ⦃x : X⦄,
    x ∈ sᶜ →
      Eq.{u_2 + 1} (α := 𝕜)
        (({ toFun := fun (x : X) ↦ (↑((g : (a : X) → ℝ) x) : 𝕜), continuous_toFun := ⋯ } : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
simpa only [coe_mk, ofReal_eq_zero] using fun x hx => hgs (subset_closure hx)

Premises used: subset_closure, RCLike.ofReal_eq_zero, ContinuousMap.coe_mk
-- 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
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
g : C(X, ℝ)
hgs : Set.EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 (closure sᶜ)
hgx : Set.EqOn (α := X) (β := ℝ) (⇑g : (a : X) → ℝ) 1 {x}
⊢ Ne.{u_2 + 1} (α := 𝕜)
    (({ toFun := fun (x : X) ↦ (↑((g : (a : X) → ℝ) x) : 𝕜), continuous_toFun := ⋯ } : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
simpa only [coe_mk, hgx (Set.mem_singleton x), Pi.one_apply, RCLike.ofReal_one] using
        one_ne_zero

Premises used: Set.mem_singleton, Pi.one_apply, RCLike.ofReal_one, ContinuousMap.coe_mk, one_ne_zero
-- 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
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
g : C(X, ℝ)
hgs : Set.EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 (closure sᶜ)
hgx : Set.EqOn (α := X) (β := ℝ) (⇑g : (a : X) → ℝ) 1 {x}
⊢ ∃ (f : C(X, 𝕜)),
    (∀ ⦃x : X⦄, x ∈ sᶜ → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)) ∧
      Ne.{u_2 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
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, RCLike.ofReal_one] using
        one_ne_zero⟩
-- 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
s : Set X
hs : IsOpen s
⊢ setOfIdeal (idealOfSet 𝕜 s) = s

Tactic:
(setOfIdeal_ofSet_eq_interior 𝕜 s).trans hs.interior_eq

Premises used: ContinuousMap.setOfIdeal_ofSet_eq_interior, IsOpen.interior_eq, Eq.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
s : Opens X
rw : IsCoatom (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 (↑s : Set X)) ↔ IsCoatom s
⊢ Ideal.IsMaximal (α := C(X, 𝕜)) (idealOfSet 𝕜 (↑s : Set X)) ↔ IsCoatom s

Tactic:
rw [Ideal.isMaximal_def]

Premises used: Ideal.isMaximal_def
-- 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
s : Opens X
⊢ IsCoatom (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 (↑s : Set X)) ↔ IsCoatom s

Tactic:
(idealOpensGI X 𝕜).isCoatom_iff (fun I hI => ?_) s

Premises used: GaloisInsertion.isCoatom_iff, ContinuousMap.idealOpensGI
-- 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
s : Opens X
refine : ∀ (I : Ideal C(X, 𝕜)) (hI : IsCoatom I), idealOfSet 𝕜 (↑(opensOfIdeal I) : Set X) = I
⊢ IsCoatom (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 (↑s : Set X)) ↔ IsCoatom s

Tactic:
refine (idealOpensGI X 𝕜).isCoatom_iff (fun I hI => ?_) s

Premises used: GaloisInsertion.isCoatom_iff, ContinuousMap.idealOpensGI
-- 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
s : Opens X
I : Ideal C(X, 𝕜)
hI : IsCoatom I
⊢ I.IsMaximal

Tactic:
rw [← Ideal.isMaximal_def] at hI

Premises used: Ideal.isMaximal_def
-- 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
s : Opens X
I : Ideal C(X, 𝕜)
hI : I.IsMaximal
⊢ idealOfSet 𝕜 (↑(opensOfIdeal I) : Set X) = I

Tactic:
idealOfSet_ofIdeal_isClosed inferInstance

Premises used: setOf, inferInstance, ContinuousMap.setOfIdeal, ContinuousMap.idealOfSet_ofIdeal_isClosed, Not
-- 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
s : Opens X
I : Ideal C(X, 𝕜)
hI : I.IsMaximal
⊢ idealOfSet 𝕜 (↑(opensOfIdeal I) : Set X) = I

Tactic:
exact idealOfSet_ofIdeal_isClosed inferInstance

Premises used: inferInstance, ContinuousMap.idealOfSet_ofIdeal_isClosed
-- 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
x : X
⊢ Ideal.IsMaximal (α := C(X, 𝕜)) (idealOfSet 𝕜 {x}ᶜ)

Tactic:
(idealOfSet_isMaximal_iff 𝕜 _).mpr <| Opens.isCoatom_iff.mpr ⟨x, rfl⟩

Premises used: Iff.mpr, TopologicalSpace.Opens.isCoatom_iff, Set.Mem, setOf, Set.singleton, Exists.intro, Not, rfl, ContinuousMap.idealOfSet_isMaximal_iff
-- 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, 𝕜)
hI : I.IsMaximal
⊢ Ideal.IsMaximal (α := C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I))

Tactic:
have h : (idealOfSet 𝕜 (setOfIdeal I)).IsMaximal :=
    (idealOfSet_ofIdeal_isClosed (inferInstance : IsClosed (I : Set C(X, 𝕜)))).symm ▸ hI
-- 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, 𝕜)
hI : I.IsMaximal
h : Ideal.IsMaximal (α := C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I))
obtain : ∀ (x : X) (hx : opensOfIdeal I = Closeds.compl {x}), ∃ (x : X), setOfIdeal I = {x}ᶜ
⊢ ∃ (x : X), setOfIdeal I = {x}ᶜ

Tactic:
obtain ⟨x, hx⟩ := Opens.isCoatom_iff.1 ((idealOfSet_isMaximal_iff 𝕜 (opensOfIdeal I)).1 h)

Premises used: TopologicalSpace.Opens.isCoatom_iff, Iff.mp, ContinuousMap.opensOfIdeal, ContinuousMap.idealOfSet_isMaximal_iff