R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ (fun f => ↑f) (↑↑(toContinuousMapOnAlgHom X) Polynomial.X) x ≠
    (fun f => ↑f) (↑↑(toContinuousMapOnAlgHom X) Polynomial.X) y
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ∃ f, f ∈ (fun f => ↑f) '' ↑(polynomialFunctions X) ∧ f x ≠ f y
refine' ⟨_, ⟨⟨_, ⟨⟨Polynomial.X, ⟨Algebra.mem_top, rfl⟩⟩, rfl⟩⟩, _⟩⟩
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ¬eval (↑x) Polynomial.X = eval (↑y) Polynomial.X
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ (fun f => ↑f) (↑↑(toContinuousMapOnAlgHom X) Polynomial.X) x ≠
    (fun f => ↑f) (↑↑(toContinuousMapOnAlgHom X) Polynomial.X) y
dsimp
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ¬↑x = ↑y
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ¬eval (↑x) Polynomial.X = eval (↑y) Polynomial.X
simp only [Polynomial.eval_X]
no goals
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ¬↑x = ↑y
exact fun h' => h (Subtype.ext h')