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
x : ℚ
⊢ ↑x ∈ s
simpa only [Rat.cast_def] using div_mem (coe_int_mem s x.num) (coe_nat_mem s x.den)