case pos
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : x = y
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y

case neg
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
by_cases n : x = y
case neg.intro.intro.intro.intro
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : (fun f => ↑f) f x ≠ (fun f => ↑f) f y
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
case neg
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
obtain ⟨_, ⟨f, hf, rfl⟩, hxy⟩ := h n
case neg.intro.intro.intro.intro
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
case neg.intro.intro.intro.intro
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : (fun f => ↑f) f x ≠ (fun f => ↑f) f y
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
replace hxy : f x - f y ≠ 0 := sub_ne_zero_of_ne hxy
case neg.intro.intro.intro.intro
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
case neg.intro.intro.intro.intro
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
let a := v x
case neg.intro.intro.intro.intro
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
case neg.intro.intro.intro.intro
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
let b := v y
case neg.intro.intro.intro.intro
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : { x // x ∈ s } :=
  ((b - a) * (↑f x - ↑f y)⁻¹) • (↑(algebraMap ((fun x => 𝕜) x) { x // x ∈ s }) (↑f x) - { val := f, property := hf }) +
    ↑(algebraMap 𝕜 { x // x ∈ s }) a
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
case neg.intro.intro.intro.intro
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
let f' : s :=
  ((b - a) * (f x - f y)⁻¹) • (algebraMap _ s (f x) - (⟨f, hf⟩ : s)) + algebraMap _ s a
case neg.intro.intro.intro.intro.refine'_1
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : { x // x ∈ s } :=
  ((b - a) * (↑f x - ↑f y)⁻¹) • (↑(algebraMap ((fun x => 𝕜) x) { x // x ∈ s }) (↑f x) - { val := f, property := hf }) +
    ↑(algebraMap 𝕜 { x // x ∈ s }) a
⊢ ↑↑f' x = v x

case neg.intro.intro.intro.intro.refine'_2
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : { x // x ∈ s } :=
  ((b - a) * (↑f x - ↑f y)⁻¹) • (↑(algebraMap ((fun x => 𝕜) x) { x // x ∈ s }) (↑f x) - { val := f, property := hf }) +
    ↑(algebraMap 𝕜 { x // x ∈ s }) a
⊢ ↑↑f' y = v y
case neg.intro.intro.intro.intro
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : { x // x ∈ s } :=
  ((b - a) * (↑f x - ↑f y)⁻¹) • (↑(algebraMap ((fun x => 𝕜) x) { x // x ∈ s }) (↑f x) - { val := f, property := hf }) +
    ↑(algebraMap 𝕜 { x // x ∈ s }) a
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
refine' ⟨f', f'.prop, _, _⟩
case pos
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x : α
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f x = v x
case pos
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : x = y
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f y = v y
subst n
no goals
case pos
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x : α
⊢ ∃ f, f ∈ ↑s ∧ ↑f x = v x ∧ ↑f x = v x
refine' ⟨_, (v x • (1 : s) : s).prop, mul_one _, mul_one _⟩
no goals
case neg.intro.intro.intro.intro.refine'_1
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : { x // x ∈ s } :=
  ((b - a) * (↑f x - ↑f y)⁻¹) • (↑(algebraMap ((fun x => 𝕜) x) { x // x ∈ s }) (↑f x) - { val := f, property := hf }) +
    ↑(algebraMap 𝕜 { x // x ∈ s }) a
⊢ ↑↑f' x = v x
simp
no goals
case neg.intro.intro.intro.intro.refine'_2
α : Type u_2
inst✝¹² : TopologicalSpace α
R : Type ?u.1508154
inst✝¹¹ : CommSemiring R
A : Type ?u.1508160
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : TopologicalSemiring A
A₂ : Type ?u.1508332
inst✝⁶ : TopologicalSpace A₂
inst✝⁵ : Semiring A₂
inst✝⁴ : Algebra R A₂
inst✝³ : TopologicalSemiring A₂
𝕜 : Type u_1
inst✝² : TopologicalSpace 𝕜
s✝ : Set C(α, 𝕜)
f✝ : ↑s✝
x✝ : α
inst✝¹ : Field 𝕜
inst✝ : TopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : SeparatesPoints s
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : ↑f x - ↑f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : { x // x ∈ s } :=
  ((b - a) * (↑f x - ↑f y)⁻¹) • (↑(algebraMap ((fun x => 𝕜) x) { x // x ∈ s }) (↑f x) - { val := f, property := hf }) +
    ↑(algebraMap 𝕜 { x // x ∈ s }) a
⊢ ↑↑f' y = v y
simp [inv_mul_cancel_right₀ hxy]