-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem continuousMapEval_bijective : Bijective (continuousMapEval X 𝕜)

Proof state:
case refine_2.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
φ : ↑(characterSpace 𝕜 C(X, 𝕜))
x : X
hx : idealOfSet 𝕜 {x}ᶜ = RingHom.ker φ
⊢ ∃ a, (continuousMapEval X 𝕜) a = φ

Tactic:
refine ⟨x, CharacterSpace.ext_ker <| Ideal.ext fun f => ?_⟩

Result:
case refine_2.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
φ : ↑(characterSpace 𝕜 C(X, 𝕜))
x : X
hx : idealOfSet 𝕜 {x}ᶜ = RingHom.ker φ
f : C(X, 𝕜)
⊢ f ∈ RingHom.ker ((continuousMapEval X 𝕜) x) ↔ f ∈ RingHom.ker φ

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
⊢ Bijective ⇑(continuousMapEval X 𝕜)

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

Result:
case refine_1
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
x y : X
hxy : (continuousMapEval X 𝕜) x = (continuousMapEval X 𝕜) y
⊢ x = y

case refine_2
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
φ : ↑(characterSpace 𝕜 C(X, 𝕜))
⊢ ∃ a, (continuousMapEval X 𝕜) a = φ

Proof state:
case refine_2.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
φ : ↑(characterSpace 𝕜 C(X, 𝕜))
x : X
hx : idealOfSet 𝕜 {x}ᶜ = RingHom.ker φ
f : C(X, 𝕜)
⊢ f ∈ RingHom.ker ((continuousMapEval X 𝕜) x) ↔ f ∈ RingHom.ker φ

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

Result:
no goals

Proof state:
case h
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
x y : X
hxy : x ≠ y
f : C(X, ℝ)
fx : Set.EqOn (⇑f) 0 {x}
fy : Set.EqOn (⇑f) 1 {y}
⊢ ((continuousMapEval X 𝕜) x) ({ toFun := fun x => ↑x, continuous_toFun := ⋯ }.comp f) ≠
    ((continuousMapEval X 𝕜) y) ({ toFun := fun x => ↑x, continuous_toFun := ⋯ }.comp 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)

Result:
no goals

Proof state:
case refine_1
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
x y : X
hxy : (continuousMapEval X 𝕜) x = (continuousMapEval X 𝕜) y
⊢ x = y

Tactic:
contrapose! hxy

Result:
case refine_1
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
x y : X
hxy : x ≠ y
⊢ (continuousMapEval X 𝕜) x ≠ (continuousMapEval X 𝕜) y

Proof state:
case refine_1.intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
x y : X
hxy : x ≠ y
f : C(X, ℝ)
fx : Set.EqOn (⇑f) 0 {x}
fy : Set.EqOn (⇑f) 1 {y}
⊢ ∃ a, ((continuousMapEval X 𝕜) x) a ≠ ((continuousMapEval X 𝕜) y) a

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

Result:
case h
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
x y : X
hxy : x ≠ y
f : C(X, ℝ)
fx : Set.EqOn (⇑f) 0 {x}
fy : Set.EqOn (⇑f) 1 {y}
⊢ ((continuousMapEval X 𝕜) x) ({ toFun := fun x => ↑x, continuous_toFun := ⋯ }.comp f) ≠
    ((continuousMapEval X 𝕜) y) ({ toFun := fun x => ↑x, continuous_toFun := ⋯ }.comp f)

Proof state:
case refine_2
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
φ : ↑(characterSpace 𝕜 C(X, 𝕜))
⊢ ∃ a, (continuousMapEval X 𝕜) a = φ

Tactic:
obtain ⟨x, hx⟩ := (ideal_isMaximal_iff (RingHom.ker φ)).mp inferInstance

Result:
case refine_2.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
φ : ↑(characterSpace 𝕜 C(X, 𝕜))
x : X
hx : idealOfSet 𝕜 {x}ᶜ = RingHom.ker φ
⊢ ∃ a, (continuousMapEval X 𝕜) a = φ

Proof state:
case refine_1
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
x y : X
hxy : x ≠ y
⊢ (continuousMapEval X 𝕜) x ≠ (continuousMapEval X 𝕜) y

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, -⟩

Result:
case refine_1.intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
x y : X
hxy : x ≠ y
f : C(X, ℝ)
fx : Set.EqOn (⇑f) 0 {x}
fy : Set.EqOn (⇑f) 1 {y}
⊢ (continuousMapEval X 𝕜) x ≠ (continuousMapEval X 𝕜) y

Proof state:
case refine_1.intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
x y : X
hxy : x ≠ y
f : C(X, ℝ)
fx : Set.EqOn (⇑f) 0 {x}
fy : Set.EqOn (⇑f) 1 {y}
⊢ (continuousMapEval X 𝕜) x ≠ (continuousMapEval X 𝕜) y

Tactic:
rw [DFunLike.ne_iff]

Result:
case refine_1.intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
x y : X
hxy : x ≠ y
f : C(X, ℝ)
fx : Set.EqOn (⇑f) 0 {x}
fy : Set.EqOn (⇑f) 1 {y}
⊢ ∃ a, ((continuousMapEval X 𝕜) x) a ≠ ((continuousMapEval X 𝕜) y) a