F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ Set.range ↑(algebraMap F E)
⊢ x ∈ ↑(adjoin F S)
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
⊢ Set.range ↑(algebraMap F E) ⊆ ↑(adjoin F S)
intro x hx
case intro
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
f : F
hf : ↑(algebraMap F E) f = x
⊢ x ∈ ↑(adjoin F S)
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ Set.range ↑(algebraMap F E)
⊢ x ∈ ↑(adjoin F S)
cases' hx with f hf
case intro
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
f : F
hf : ↑(algebraMap F E) f = x
⊢ ↑(algebraMap F E) f ∈ ↑(adjoin F S)
case intro
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
f : F
hf : ↑(algebraMap F E) f = x
⊢ x ∈ ↑(adjoin F S)
rw [← hf]
no goals
case intro
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
f : F
hf : ↑(algebraMap F E) f = x
⊢ ↑(algebraMap F E) f ∈ ↑(adjoin F S)
exact adjoin.algebraMap_mem F S f