no goals
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
⊢ x ∈ ↑(⨆ (i : ι), S i) ↔ x ∈ ⋃ (i : ι), ↑(S i)
simp [mem_iSup_of_directed hS]