K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
S : Set (Subfield K)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : K
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
S : Set (Subfield K)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : K
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
haveI : Nonempty S := Sne.to_subtype
no goals
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
S : Set (Subfield K)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : K
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]