awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ (¬∀ f ∈ I, Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)) ↔
    ∃ f ∈ I, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
have push : (∃ f ∈ I, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)) ↔
  ∃ f ∈ I, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
Tactic: push Not
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : T2Space R
I : Ideal C(X, R)
⊢ IsOpen (setOfIdeal I)
have simp : IsClosed.{u_1} (X := X) (⋂ i ∈ I, {x : X | Eq.{u_2 + 1} (α := R) ((i : (a : X) → R) x : R) (0 : R)})
Tactic: simp only [setOfIdeal, Set.setOf_forall, isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
⊢ GaloisConnection (α := Ideal C(X, R)) setOfIdeal (idealOfSet R)
have refine_1 : ∀ (I : Ideal C(X, R)) (s : Set X) (h : setOfIdeal I ≤ s) (f : C(X, R)) (hf : f ∈ I),
  Membership.mem (γ := Submodule C(X, R) C(X, R)) (idealOfSet R s) f
Tactic: refine fun I s => ⟨fun h f hf => ?_, fun h x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
refine_1 :
  ∀ (I : Ideal C(X, R)) (s : Set X) (h : setOfIdeal I ≤ s) (f : C(X, R)) (hf : f ∈ I),
    Membership.mem (γ := Submodule C(X, R) C(X, R)) (idealOfSet R s) f
⊢ GaloisConnection (α := Ideal C(X, R)) setOfIdeal (idealOfSet R)
have refine_2 : ∀ (I : Ideal C(X, R)) (s : Set X) (h : I ≤ idealOfSet R s) (x : X) (hx : x ∈ setOfIdeal I), x ∈ s
Tactic: refine fun I s => ⟨fun h f hf => ?_, fun h x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ≤ s
f : C(X, R)
hf : f ∈ I
⊢ Membership.mem (γ := Submodule C(X, R) C(X, R)) (idealOfSet R s) f
have refine_1 : ∀ (h' : f ∉ idealOfSet R s), False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring 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
have refine_1 : ∀ (x : X) (hx : x ∈ sᶜ) (hfx : Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)), False
Tactic: rcases notMem_idealOfSet.mp h' with ⟨x, hx, hfx⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
⊢ x ∈ s
have refine_2 : ∀ (f : C(X, R)) (hf : f ∈ I) (hfx : Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)), x ∈ s
Tactic: obtain ⟨f, hf, hfx⟩ := mem_setOfIdeal.mp hx
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring 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 : Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
⊢ x ∈ s
have refine_2 : ∀ (hx' : x ∉ s), False
Tactic: by_contra hx'
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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, 𝕜)
⊢ Eq (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) I.closure
have refine : LE.le (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) I.closure
Tactic: refine le_antisymm ?_
      ((idealOfSet_closed 𝕜 <| setOfIdeal I).closure_subset_iff.mpr fun f hf x hx =>
        notMem_setOfIdeal.mp hx hf)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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, 𝕜)
⊢ LE.le (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) I.closure
have refine : ∀ (f : C(X, 𝕜)) (hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f) (ε : ℝ)
  (hε : ε > 0), ∃ b ∈ (↑I : Set C(X, 𝕜)), dist f b < ε
Tactic: refine (fun f hf => Metric.mem_closure_iff.mpr fun ε hε => ?_)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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
ε : ℝ
hε : ε > 0
⊢ ∃ b ∈ (↑I : Set C(X, 𝕜)), dist f b < ε
have lift : ∀ (ε : ℝ≥0) (hε : (↑ε : ℝ) > 0), ∃ b ∈ (↑I : Set C(X, 𝕜)), dist f b < (↑ε : ℝ)
Tactic: lift ε to ℝ≥0 using hε.lt.le
Cleared hypotheses: ε, hε
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (hypothesis)
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
⊢ ∃ b ∈ (↑I : Set C(X, 𝕜)), dist f b < (↑ε : ℝ)
have hε₁ : 0 < ε
Tactic: replace hε := show (0 : ℝ≥0) < ε from hε
Cleared hypotheses: hε
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (hypothesis)
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 : 𝕜)}
⊢ ∃ b ∈ (↑I : Set C(X, 𝕜)), nndist f b < ε
have ht : IsClosed t
Tactic: have ht : IsClosed t := isClosed_le continuous_const (map_continuous f).nnnorm
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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
⊢ Disjoint t (setOfIdeal I)ᶜ
have refine : ∀ (x : X) (hx : x ∈ (setOfIdeal I)ᶜ), x ∈ tᶜ
Tactic: refine Set.subset_compl_iff_disjoint_left.mp fun x hx => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (hypothesis)
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
⊢ ∃ b ∈ (↑I : Set C(X, 𝕜)), nndist f b < ε
have htI : Disjoint t (setOfIdeal I)ᶜ
Tactic: have htI : Disjoint t (setOfIdeal I)ᶜ := by
    refine Set.subset_compl_iff_disjoint_left.mp fun x hx => ?_
    simpa only [t, Set.mem_setOf, Set.mem_compl_iff, not_le] using
      (nnnorm_eq_zero.mpr (mem_idealOfSet.mp hf hx)).trans_lt (half_pos hε)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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 : 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 < ε
have obtain : ∀ (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), ∃ b ∈ (↑I : Set C(X, 𝕜)), nndist f b < ε
Tactic: obtain ⟨g, hgI, hg, hgt⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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
⊢ ∃ b ∈ (↑I : Set C(X, 𝕜)), nndist f b < ε
have refine : nndist f (f * comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) < ε
Tactic: refine ⟨f * (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g, I.mul_mem_left f hgI, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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
⊢ nndist f (f * comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) < ε
have rw : ‖f - f * comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g‖₊ < ε
Tactic: rw [nndist_eq_nnnorm]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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
⊢ ‖f - f * comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g‖₊ < ε
have refine : ∀ (x : X), nnnorm.{u_2} (E := 𝕜) ((f - f * comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜) < ε
Tactic: refine (nnnorm_lt_iff _ hε).2 fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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
⊢ nnnorm.{u_2} (E := 𝕜) ((f - f * comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜) < ε
have simp : ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ <
  ε
Tactic: simp only [coe_sub, coe_mul, Pi.sub_apply, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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
⊢ ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ <
    ε
have 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 : 𝕜))‖₊ <
    ε
Tactic: by_cases hx : x ∈ t
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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 : 𝕜))‖₊ <
      ε
⊢ ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ <
    ε
have 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 : 𝕜))‖₊ <
    ε
Tactic: by_cases hx : x ∈ t
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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 : 𝕜))‖₊ <
    ε
have neg : ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ ≤
  ε / 2
Tactic: refine lt_of_le_of_lt ?_ (half_lt_self hε)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (hypothesis)
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 : 𝕜))‖₊ ≤
    ε / 2
have this : 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
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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 : 𝕜))‖₊ ≤
    ε / 2
have 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 : 𝕜)‖₊
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 _
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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 : 𝕜)‖₊
⊢ ‖HSub.hSub (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)
          ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜))‖₊ ≤
    ε / 2
have x₂ : ε / 2 *
    nnnorm.{u_2} (E := 𝕜)
      ((HSub.hSub (α := C(X, 𝕜)) 1 (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 _
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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)ᶜ
⊢ ∃ b ∈ (↑I : Set C(X, 𝕜)), nndist f b < ε
have 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
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 _