no goals
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
S : Set E
K L : IntermediateField F E
⊢ Module.rank F { x // x ∈ K } = 1 ↔ K = ⊥
rw [← toSubalgebra_eq_iff, ← rank_eq_rank_subalgebra, Subalgebra.rank_eq_one_iff,
  bot_toSubalgebra]