case intro.intro
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_3
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type ?u.1479689
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s => SeparatesPoints s) s
x y : α
n : x ≠ y
f : α → A
m : f ∈ (fun f => ↑f) '' ↑s
w : f x ≠ f y
⊢ ∃ f, f ∈ (fun f => ↑f) '' ↑s' ∧ f x ≠ f y
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_3
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type ?u.1479689
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s => SeparatesPoints s) s
x y : α
n : x ≠ y
⊢ ∃ f, f ∈ (fun f => ↑f) '' ↑s' ∧ f x ≠ f y
obtain ⟨f, m, w⟩ := h n
case intro.intro.intro.intro
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_3
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type ?u.1479689
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s => SeparatesPoints s) s
x y : α
n : x ≠ y
f : C(α, A)
m : f ∈ ↑s
w : (fun f => ↑f) f x ≠ (fun f => ↑f) f y
⊢ ∃ f, f ∈ (fun f => ↑f) '' ↑s' ∧ f x ≠ f y
case intro.intro
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_3
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type ?u.1479689
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s => SeparatesPoints s) s
x y : α
n : x ≠ y
f : α → A
m : f ∈ (fun f => ↑f) '' ↑s
w : f x ≠ f y
⊢ ∃ f, f ∈ (fun f => ↑f) '' ↑s' ∧ f x ≠ f y
rcases m with ⟨f, ⟨m, rfl⟩⟩
no goals
case intro.intro.intro.intro
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_3
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
A₂ : Type ?u.1479689
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : TopologicalSemiring A₂
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s => SeparatesPoints s) s
x y : α
n : x ≠ y
f : C(α, A)
m : f ∈ ↑s
w : (fun f => ↑f) f x ≠ (fun f => ↑f) f y
⊢ ∃ f, f ∈ (fun f => ↑f) '' ↑s' ∧ f x ≠ f y
exact ⟨_, ⟨f, ⟨r m, rfl⟩⟩, w⟩