awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)),
    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
have 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)
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
-- 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 ∈ 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
have 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
Tactic: obtain ⟨g', hI', 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)
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
⊢ False
have rwa : ∀ (hy : Membership.mem (γ := Set X) ∅ y), False
Tactic: rwa [ht'] at hy
Cleared hypotheses: hy
-- 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)
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
have 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
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'⟩
-- 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)
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)),
    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
have 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
Tactic: obtain ⟨g, hg, hgc⟩ := exists_mul_le_one_eqOn_ge g' hc
-- 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)
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
have refine : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g * g') ∈ I
Tactic: refine ⟨g * g', ?_, hg, hgc.mono hgc'⟩
-- 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)
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}
⊢ comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g * g') ∈ I
have h : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g * g') =
  HMul.hMul (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g')
Tactic: convert! I.mul_mem_left ((algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp 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)ᶜ
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}
⊢ comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) (g * g') =
    HMul.hMul (α := C(X, 𝕜)) (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g)
      (comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g')
have 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 :
      𝕜)
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
s : Set X
⊢ setOfIdeal (idealOfSet 𝕜 s) = interior s
have 𝕜₁ : ∀ (x : X) (hx : x ∈ interior s), x ∈ setOfIdeal (idealOfSet 𝕜 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 => ?_
-- 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
s : Set X
x : X
hx : x ∈ interior s
⊢ x ∈ setOfIdeal (idealOfSet 𝕜 s)
have hx₁ : x ∈ (closure sᶜ)ᶜ
Tactic: rw [← compl_compl (interior s), ← closure_compl] 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
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
⊢ x ∈ setOfIdeal (idealOfSet 𝕜 s)
have 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 : 𝕜)
Tactic: simp_rw [mem_setOfIdeal, mem_idealOfSet]
-- 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
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
⊢ ∃ (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 : 𝕜)
have 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 : 𝕜)
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)
-- 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
s : Opens X
⊢ Ideal.IsMaximal (α := C(X, 𝕜)) (idealOfSet 𝕜 (↑s : Set X)) ↔ IsCoatom s
have rw : IsCoatom (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 (↑s : Set X)) ↔ IsCoatom s
Tactic: rw [Ideal.isMaximal_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
s : Opens X
⊢ IsCoatom (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 (↑s : Set X)) ↔ IsCoatom s
have refine : ∀ (I : Ideal C(X, 𝕜)) (hI : IsCoatom I), idealOfSet 𝕜 (↑(opensOfIdeal I) : Set X) = I
Tactic: refine (idealOpensGI X 𝕜).isCoatom_iff (fun I hI => ?_) s
-- 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
s : Opens X
I : Ideal C(X, 𝕜)
hI : IsCoatom I
⊢ idealOfSet 𝕜 (↑(opensOfIdeal I) : Set X) = I
have hI₁ : I.IsMaximal
Tactic: rw [← Ideal.isMaximal_def] at hI
Cleared hypotheses: hI
-- 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, 𝕜)
hI : I.IsMaximal
⊢ ∃ (x : X), setOfIdeal I = {x}ᶜ
have h : 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
-- 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, 𝕜)
hI : I.IsMaximal
h : Ideal.IsMaximal (α := C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I))
⊢ ∃ (x : X), setOfIdeal I = {x}ᶜ
have obtain : ∀ (x : X) (hx : opensOfIdeal I = Closeds.compl {x}), ∃ (x : X), setOfIdeal I = {x}ᶜ
Tactic: obtain ⟨x, hx⟩ := Opens.isCoatom_iff.1 ((idealOfSet_isMaximal_iff 𝕜 (opensOfIdeal I)).1 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, 𝕜)
hI : IsClosed (↑I : Set C(X, 𝕜))
⊢ I.IsMaximal ↔ ∃ (x : X), idealOfSet 𝕜 {x}ᶜ = I
have fun : I.IsMaximal → ∃ (x : X), idealOfSet 𝕜 {x}ᶜ = I
Tactic: refine
    ⟨?_, fun h =>
      let ⟨x, hx⟩ := h
      hx ▸ idealOf_compl_singleton_isMaximal 𝕜 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, 𝕜)
hI : IsClosed (↑I : Set C(X, 𝕜))
hI' : I.IsMaximal
⊢ ∃ (x : X), idealOfSet 𝕜 {x}ᶜ = I
have obtain : ∀ (x : X) (hx : setOfIdeal I = {x}ᶜ), ∃ (x : X), idealOfSet 𝕜 {x}ᶜ = I
Tactic: obtain ⟨x, hx⟩ := setOfIdeal_eq_compl_singleton I
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : CommRing 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : Nontrivial 𝕜
inst_5 : NoZeroDivisors 𝕜
x : X
⊢ Membership.mem (γ := Set (WeakDual 𝕜 C(X, 𝕜))) (characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜)))
    { toFun := fun (f : C(X, 𝕜)) ↦ (f : (a : X) → 𝕜) x, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
have rw : Membership.mem (γ := Set (WeakDual 𝕜 C(X, 𝕜)))
  {φ : WeakDual 𝕜 C(X, 𝕜) |
    Eq.{u_2 + 1} (α := 𝕜) ((φ : (a : C(X, 𝕜)) → 𝕜) 1 : 𝕜) (1 : 𝕜) ∧
      ∀ (x y : C(X, 𝕜)),
        (φ : (a : C(X, 𝕜)) → 𝕜) (x * y) =
          HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : C(X, 𝕜)) → 𝕜) x : 𝕜) ((φ : (a : C(X, 𝕜)) → 𝕜) y : 𝕜)}
  { toFun := fun (f : C(X, 𝕜)) ↦ (f : (a : X) → 𝕜) x, map_add' := sorry, map_smul' := sorry, cont := sorry }
Tactic: rw [CharacterSpace.eq_set_map_one_map_mul]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : RCLike 𝕜
⊢ Bijective (α := X) (β := (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
    (⇑(continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
      (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
have refine_1 : ∀ (x y : X)
  (hxy :
    Eq (α := (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
      (((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
            (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
          x :
        (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
      (((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
            (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
          y :
        (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))),
  x = y
Tactic: refine ⟨fun x y hxy => ?_, fun φ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : RCLike 𝕜
refine_1 :
  ∀ (x y : X)
    (hxy :
      Eq (α := (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
        (((continuousMapEval X 𝕜 :
                C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
              (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
            x :
          (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
        (((continuousMapEval X 𝕜 :
                C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
              (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
            y :
          (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))),
    x = y
⊢ Bijective (α := X) (β := (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
    (⇑(continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
      (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
have refine_2 : ∀ (φ : (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))),
  ∃ (a : X),
    ((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        a =
      φ
Tactic: refine ⟨fun x y hxy => ?_, fun φ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : RCLike 𝕜
x y : X
hxy :
  Eq (α := (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
    (((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        x :
      (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
    (((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        y :
      (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
⊢ x = y
have refine_1 : ∀ (hxy : x ≠ y),
  Ne (α := (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
    (((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        x :
      (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
    (((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        y :
      (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
Tactic: contrapose! hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : RCLike 𝕜
x y : X
hxy : x ≠ y
⊢ Ne (α := (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
    (((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        x :
      (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
    (((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        y :
      (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
have refine_1 : ∀ (f : C(X, ℝ)) (fx : Set.EqOn (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) 0 {x})
  (fy : Set.EqOn (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) 1 {y}),
  Ne (α := (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
    (((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        x :
      (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
    (((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        y :
      (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
Tactic: rcases exists_continuous_zero_one_of_isClosed (isClosed_singleton : _root_.IsClosed {x})
        (isClosed_singleton : _root_.IsClosed {y}) (Set.disjoint_singleton.mpr hxy) with
      ⟨f, fx, fy, -⟩