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, 𝕜)
hI : I.IsMaximal
h : Ideal.IsMaximal (α := C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I))
x : X
hx : opensOfIdeal I = Closeds.compl {x}
⊢ ∃ (x : X), setOfIdeal I = {x}ᶜ

Tactic:
⟨x, congr_arg (fun (s : Opens X) => (s : Set X)) hx⟩

Premises used: congr_arg, SetLike.coe, Exists.intro
-- 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))
x : X
hx : opensOfIdeal I = Closeds.compl {x}
⊢ ∃ (x : X), setOfIdeal I = {x}ᶜ

Tactic:
exact ⟨x, congr_arg (fun (s : Opens X) => (s : Set X)) hx⟩
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed (↑I : Set C(X, 𝕜))
⊢ I.IsMaximal ↔ ∃ (x : X), idealOfSet 𝕜 {x}ᶜ = I

Tactic:
⟨?_, fun h =>
      let ⟨x, hx⟩ := h
      hx ▸ idealOf_compl_singleton_isMaximal 𝕜 x⟩

Premises used: _private.0.ContinuousMap.ideal_isMaximal_iff.match_1, Eq.rec, Iff.intro, Ideal.IsMaximal, ContinuousMap.idealOf_compl_singleton_isMaximal
-- 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, 𝕜))
fun : I.IsMaximal → ∃ (x : X), idealOfSet 𝕜 {x}ᶜ = I
⊢ I.IsMaximal ↔ ∃ (x : X), idealOfSet 𝕜 {x}ᶜ = I

Tactic:
refine
    ⟨?_, fun h =>
      let ⟨x, hx⟩ := h
      hx ▸ idealOf_compl_singleton_isMaximal 𝕜 x⟩
-- 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, 𝕜))
hI' : I.IsMaximal
obtain : ∀ (x : X) (hx : setOfIdeal I = {x}ᶜ), ∃ (x : X), idealOfSet 𝕜 {x}ᶜ = I
⊢ ∃ (x : X), idealOfSet 𝕜 {x}ᶜ = I

Tactic:
obtain ⟨x, hx⟩ := setOfIdeal_eq_compl_singleton I

Premises used: ContinuousMap.setOfIdeal_eq_compl_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
I : Ideal C(X, 𝕜)
hI : IsClosed (↑I : Set C(X, 𝕜))
hI' : I.IsMaximal
x : X
hx : setOfIdeal I = {x}ᶜ
⊢ idealOfSet 𝕜 {x}ᶜ = I

Tactic:
simpa only [idealOfSet_ofIdeal_eq_closure, I.closure_eq_of_isClosed hI] using
        congr_arg (idealOfSet 𝕜) hx.symm

Premises used: Ideal.closure_eq_of_isClosed, congr_arg, ContinuousMap.idealOfSet, Eq.symm, ContinuousMap.idealOfSet_ofIdeal_eq_closure
-- 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, 𝕜))
hI' : I.IsMaximal
x : X
hx : setOfIdeal I = {x}ᶜ
⊢ ∃ (x : X), idealOfSet 𝕜 {x}ᶜ = I

Tactic:
exact
    ⟨x, by
      simpa only [idealOfSet_ofIdeal_eq_closure, I.closure_eq_of_isClosed hI] using
        congr_arg (idealOfSet 𝕜) hx.symm⟩
-- Module: Mathlib.Topology.ContinuousMap.Ideals
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
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' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ 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 := ⋯ }

Tactic:
rw [CharacterSpace.eq_set_map_one_map_mul]

Premises used: WeakDual.CharacterSpace.eq_set_map_one_map_mul
-- Module: Mathlib.Topology.ContinuousMap.Ideals
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, 𝕜)))
    {φ : 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' := ⋯, map_smul' := ⋯, cont := ⋯ }

Tactic:
⟨rfl, fun f g => rfl⟩

Premises used: Set.Mem, setOf, And.intro, rfl
-- Module: Mathlib.Topology.ContinuousMap.Ideals
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, 𝕜)))
    {φ : 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' := ⋯, map_smul' := ⋯, cont := ⋯ }

Tactic:
exact ⟨rfl, fun f g => rfl⟩
-- Module: Mathlib.Topology.ContinuousMap.Ideals
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 𝕜
⊢ Continuous (Y := (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))) fun (x : X) ↦
    Subtype.mk (p := fun (x : WeakDual 𝕜 C(X, 𝕜)) ↦
      Membership.mem (γ := Set (WeakDual 𝕜 C(X, 𝕜))) (characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) x)
      { toFun := fun (f : C(X, 𝕜)) ↦ (f : (a : X) → 𝕜) x, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ⋯

Tactic:
Continuous.subtype_mk (continuous_of_continuous_eval map_continuous) _

Premises used: WeakDual.continuous_of_continuous_eval, Continuous.subtype_mk
-- Module: Mathlib.Topology.ContinuousMap.Ideals
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 𝕜
⊢ Continuous (Y := (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))) fun (x : X) ↦
    Subtype.mk (p := fun (x : WeakDual 𝕜 C(X, 𝕜)) ↦
      Membership.mem (γ := Set (WeakDual 𝕜 C(X, 𝕜))) (characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) x)
      { toFun := fun (f : C(X, 𝕜)) ↦ (f : (a : X) → 𝕜) x, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ⋯

Tactic:
exact Continuous.subtype_mk (continuous_of_continuous_eval map_continuous) _

Premises used: WeakDual.continuous_of_continuous_eval, Continuous.subtype_mk
-- Module: Mathlib.Topology.ContinuousMap.Ideals
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
f : C(X, 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (((((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))) :
          (a : C(X, 𝕜)) → 𝕜)
        f :
      𝕜)
    ((f : (a : X) → 𝕜) x : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Ideals
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)))

Tactic:
⟨fun x y hxy => ?_, fun φ => ?_⟩

Premises used: And.intro, Function.Bijective
-- Module: Mathlib.Topology.ContinuousMap.Ideals
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
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 =
        φ
⊢ 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)))

Tactic:
refine ⟨fun x y hxy => ?_, fun φ => ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.Ideals
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)))
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)))
⊢ x = y

Tactic:
contrapose! hxy
-- Module: Mathlib.Topology.ContinuousMap.Ideals
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
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)))
⊢ 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, -⟩

Premises used: Iff.mpr, exists_continuous_zero_one_of_isClosed, Set.disjoint_singleton, isClosed_singleton
-- Module: Mathlib.Topology.ContinuousMap.Ideals
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
f : C(X, ℝ)
fx : Set.EqOn (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) 0 {x}
fy : Set.EqOn (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) 1 {y}
refine_1 :
  ∃ (a : C(X, 𝕜)),
    Ne.{u_2 + 1} (α := 𝕜)
      (((((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))) :
            (a : C(X, 𝕜)) → 𝕜)
          a :
        𝕜)
      (((((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))) :
            (a : C(X, 𝕜)) → 𝕜)
          a :
        𝕜)
⊢ 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:
rw [DFunLike.ne_iff]

Premises used: DFunLike.ne_iff
-- Module: Mathlib.Topology.ContinuousMap.Ideals
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
f : C(X, ℝ)
fx : Set.EqOn (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) 0 {x}
fy : Set.EqOn (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) 1 {y}
h :
  Ne.{u_2 + 1} (α := 𝕜)
    (((((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))) :
          (a : C(X, 𝕜)) → 𝕜)
        (ContinuousMap.comp { toFun := fun (x : ℝ) ↦ (↑x : 𝕜), continuous_toFun := ⋯ } f) :
      𝕜)
    (((((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))) :
          (a : C(X, 𝕜)) → 𝕜)
        (ContinuousMap.comp { toFun := fun (x : ℝ) ↦ (↑x : 𝕜), continuous_toFun := ⋯ } f) :
      𝕜)
⊢ ∃ (a : C(X, 𝕜)),
    Ne.{u_2 + 1} (α := 𝕜)
      (((((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))) :
            (a : C(X, 𝕜)) → 𝕜)
          a :
        𝕜)
      (((((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))) :
            (a : C(X, 𝕜)) → 𝕜)
          a :
        𝕜)

Tactic:
use (⟨fun (x : ℝ) => (x : 𝕜), RCLike.continuous_ofReal⟩ : C(ℝ, 𝕜)).comp f

Premises used: ContinuousMap.mk, ContinuousMap.comp, RCLike.ofReal, RCLike.continuous_ofReal
-- Module: Mathlib.Topology.ContinuousMap.Ideals
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
f : C(X, ℝ)
fx : Set.EqOn (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) 0 {x}
fy : Set.EqOn (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) 1 {y}
⊢ Ne.{u_2 + 1} (α := 𝕜)
    (((((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))) :
          (a : C(X, 𝕜)) → 𝕜)
        (ContinuousMap.comp { toFun := fun (x : ℝ) ↦ (↑x : 𝕜), continuous_toFun := ⋯ } f) :
      𝕜)
    (((((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))) :
          (a : C(X, 𝕜)) → 𝕜)
        (ContinuousMap.comp { toFun := fun (x : ℝ) ↦ (↑x : 𝕜), continuous_toFun := ⋯ } f) :
      𝕜)

Tactic:
simpa only [continuousMapEval_apply_apply, ContinuousMap.comp_apply, coe_mk, Ne,
      RCLike.ofReal_inj] using
      ((fx (Set.mem_singleton x)).symm ▸ (fy (Set.mem_singleton y)).symm ▸ zero_ne_one : f x ≠ f y)

Premises used: Set.mem_singleton, RCLike.ofReal_inj, Eq.rec, zero_ne_one, Ne, ContinuousMap.comp_apply, ContinuousMap.coe_mk, WeakDual.CharacterSpace.continuousMapEval_apply_apply, Eq.symm
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : RCLike 𝕜
φ : (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))
refine_2 :
  ∀ (x : X) (hx : Eq (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 {x}ᶜ) (RingHom.ker φ)),
    ∃ (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 =
        φ
⊢ ∃ (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:
obtain ⟨x, hx⟩ := (ideal_isMaximal_iff (RingHom.ker φ)).mp inferInstance

Premises used: inferInstance, ContinuousMap.ideal_isMaximal_iff, Iff.mp, RingHom.ker
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : RCLike 𝕜
φ : (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))
x : X
hx : Eq (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 {x}ᶜ) (RingHom.ker φ)
⊢ ∃ (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:
⟨x, CharacterSpace.ext_ker <| Ideal.ext fun f => ?_⟩

Premises used: WeakDual.CharacterSpace.ext_ker, Ideal.ext, Exists.intro
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : RCLike 𝕜
φ : (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))
x : X
hx : Eq (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 {x}ᶜ) (RingHom.ker φ)
refine_2 :
  ∀ (f : C(X, 𝕜)),
    Membership.mem (γ := Ideal C(X, 𝕜))
        (RingHom.ker (F := (↑(characterSpace 𝕜 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))))
        f ↔
      Membership.mem (γ := Ideal C(X, 𝕜)) (RingHom.ker φ) f
⊢ ∃ (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 ⟨x, CharacterSpace.ext_ker <| Ideal.ext fun f => ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : RCLike 𝕜
φ : (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))
x : X
hx : Eq (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 {x}ᶜ) (RingHom.ker φ)
f : C(X, 𝕜)
⊢ Membership.mem (γ := Ideal C(X, 𝕜))
      (RingHom.ker (F := (↑(characterSpace 𝕜 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))))
      f ↔
    Membership.mem (γ := Ideal C(X, 𝕜)) (RingHom.ker φ) f

Tactic:
simpa only [RingHom.mem_ker, continuousMapEval_apply_apply, mem_idealOfSet_compl_singleton,
      RingHom.mem_ker] using SetLike.ext_iff.mp hx f

Premises used: RingHom.mem_ker, SetLike.ext_iff, Iff.mp, WeakDual.CharacterSpace.continuousMapEval_apply_apply, ContinuousMap.mem_idealOfSet_compl_singleton
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
inst_3 : Fact (a ≤ b)
E : Type u_2
inst_4 : TopologicalSpace E
f : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
x : α
hx : x ∈ Icc a b
⊢ Eq.{u_2 + 1} (α := E)
    ((((IccExtendCM : (a : C((↑(Icc a b) : Type u_1), E)) → C(α, E)) f : C(α, E)) : (a : α) → E) x : E)
    ((f : (a : (↑(Icc a b) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) x hx) : E)

Tactic:
simp [IccExtendCM, projIccCM, projIcc, hx.1, hx.2]

Premises used: ContinuousMap.projIccCM, Set.projIcc, And.right, And.left, ContinuousMap.IccExtendCM