no goals
K : Type u_2
L : Type u_1
L' : Type ?u.75335
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
n : ℕ
⊢ ↑n ∈ S
simpa using coe_int_mem S n