awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
have 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)
Tactic: refine ht.isCompact.induction_on ?_ ?_ ?_ ?_
-- 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)ᶜ
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)
⊢ ∃ (g' : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
have 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)
Tactic: refine ht.isCompact.induction_on ?_ ?_ ?_ ?_
-- 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)ᶜ
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)
⊢ ∃ (g' : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
have 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)
Tactic: refine ht.isCompact.induction_on ?_ ?_ ?_ ?_
-- 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)ᶜ
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)
⊢ ∃ (g' : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g' ∈ I ∧
      ∀ x ∈ t, LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g' : (a : X) → ℝ≥0) x : ℝ≥0)
have 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)
Tactic: refine ht.isCompact.induction_on ?_ ?_ ?_ ?_
-- 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)),
    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)
have refine_1 : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) 0 ∈ I
Tactic: refine ⟨0, ?_, fun x hx => False.elim 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, 𝕜)
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)ᶜ
⊢ comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) 0 ∈ I
have h : Eq (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) 0) 0
Tactic: convert! I.zero_mem
-- 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)ᶜ
⊢ Eq (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) 0) 0
have h : ∀ (a : X),
  Eq.{u_2 + 1} (α := 𝕜) ((comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) 0 : (a : X) → 𝕜) a : 𝕜) ((0 : (a : X) → 𝕜) a : 𝕜)
Tactic: ext
-- 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)ᶜ
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)
have refine_3 : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g₁ + g₂) ∈ I
Tactic: refine ⟨g₁ + g₂, ?_, fun x 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, 𝕜)
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
⊢ ∃ (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)
have refine_3₁ : ∀ (x : X) (hx : x ∈ s₁ ∪ s₂), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ + g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
Tactic: refine ⟨g₁ + g₂, ?_, fun x 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, 𝕜)
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)
⊢ comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g₁ + g₂) ∈ I
have h : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g₁ + g₂) =
  HAdd.hAdd (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂)
Tactic: convert! I.add_mem hI₁ hI₂
-- 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)ᶜ
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)
⊢ comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g₁ + g₂) =
    HAdd.hAdd (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₁)
      (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g₂)
have 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 :
      𝕜)
Tactic: ext y
-- 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)ᶜ
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₂
⊢ LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ + g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
have refine_3 : ∀ (hx : x ∈ s₁), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ + g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
Tactic: rcases hx with (hx | hx)
Cleared hypotheses: 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, 𝕜)
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)
⊢ LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ + g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
have refine_3₁ : ∀ (hx : x ∈ s₂), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((g₁ + g₂ : (a : X) → ℝ≥0) x : ℝ≥0)
Tactic: rcases hx with (hx | hx)
Cleared hypotheses: 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
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
hx : 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)
have hx₁ : x ∈ (setOfIdeal I)ᶜᶜ
Tactic: replace hx := htI.subset_compl_right hx
Cleared hypotheses: 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
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
hx : x ∈ (setOfIdeal 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)
have hx₁ : ∃ f ∈ I, Ne.{u_2 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜) (0 : 𝕜)
Tactic: rw [compl_compl, mem_setOfIdeal] at hx
Cleared hypotheses: 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, 𝕜)
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 : 𝕜)
⊢ ∃ 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)
have 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)
Tactic: obtain ⟨g, hI, hgx⟩ := hx
Cleared hypotheses: 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
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
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)
have this : ∀ᶠ (z : X) in nhds x, Ne.{u_2 + 1} (α := 𝕜) ((g : (a : X) → 𝕜) z : 𝕜) (0 : 𝕜)
Tactic: have := (map_continuous g).continuousAt.eventually_ne hgx
-- 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)ᶜ
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)
have refine_4 : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜))
    { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (nnnorm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜)) 2,
      continuous_toFun := sorry : C(X, ℝ≥0) } ∈
  I
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⟩⟩
-- 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)ᶜ
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 : 𝕜)
⊢ 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
have h : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜))
    { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (nnnorm.{u_2} (E := 𝕜) ((g : (a : X) → 𝕜) x : 𝕜)) 2,
      continuous_toFun := sorry : C(X, ℝ≥0) } =
  star g * g
Tactic: convert! I.mul_mem_left (star g) hI
-- 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)ᶜ
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 : 𝕜)
⊢ 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
have 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 := sorry : C(X, ℝ≥0) } :
          (a : X) → 𝕜)
        a :
      𝕜)
    ((star g * g : (a : X) → 𝕜) a : 𝕜)
Tactic: ext
-- 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)ᶜ
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
⊢ 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 : 𝕜)
have 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 : 𝕜)
Tactic: simp only [comp_apply, ContinuousMap.coe_coe, coe_mk, algebraMapCLM_apply, map_pow,
        mul_apply, star_apply, star_def]
-- 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)ᶜ
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 =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((g : (a : X) → 𝕜) a : 𝕜) : 𝕜) ((g : (a : X) → 𝕜) a : 𝕜)
have 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
Tactic: simp only [RCLike.conj_mul]