case h
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
h : ∀ (x : E), Module.rank F { x_1 // x_1 ∈ F⟮x⟯ } = 1
y : E
⊢ y ∈ ⊥ ↔ y ∈ ⊤
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
h : ∀ (x : E), Module.rank F { x_1 // x_1 ∈ F⟮x⟯ } = 1
⊢ ⊥ = ⊤
ext y
case h
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
h : ∀ (x : E), Module.rank F { x_1 // x_1 ∈ F⟮x⟯ } = 1
y : E
⊢ y ∈ ⊥
case h
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
h : ∀ (x : E), Module.rank F { x_1 // x_1 ∈ F⟮x⟯ } = 1
y : E
⊢ y ∈ ⊥ ↔ y ∈ ⊤
rw [iff_true_right IntermediateField.mem_top]
no goals
case h
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
h : ∀ (x : E), Module.rank F { x_1 // x_1 ∈ F⟮x⟯ } = 1
y : E
⊢ y ∈ ⊥
exact rank_adjoin_simple_eq_one_iff.mp (h y)