no goals
K : Type u_2
L : Type u_1
L' : Type ?u.252800
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : L
hx : x ∈ RingHom.fieldRange (algebraMap K L)
⊢ x ∈ Set.range ↑(algebraMap K L)
rwa [Set.mem_range, ← RingHom.mem_fieldRange]