no goals
K : Type u
L : Type v
M : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field M
S : Type u_1
inst✝ : SetLike S K
h : SubfieldClass S K
s : S
a : ℚ
x : { x // x ∈ s }
⊢ a • ↑x ∈ s
simpa only [Rat.smul_def] using mul_mem (coe_rat_mem s a) x.prop