F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
K : IntermediateField F E
⊢ F⟮α⟯ ≤ K ↔ α ∈ K
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
K : IntermediateField F E
⊢ Insert.insert ∅ α ⊆ ↑K ↔ α ∈ K
simp only [← adjoin_le_iff, ← le_eq_subset]
no goals
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
K : IntermediateField F E
⊢ F⟮α⟯ ≤ K ↔ α ∈ K
exact adjoin_le_iff.trans singleton_subset_iff