case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
S : Set E
K L : IntermediateField F E
inst✝ : FiniteDimensional F E
h : ∀ (x : E), finrank F { x_1 // x_1 ∈ F⟮x⟯ } ≤ 1
⊢ ∀ (x : E), finrank F { x_1 // x_1 ∈ F⟮x⟯ } = 1
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
S : Set E
K L : IntermediateField F E
inst✝ : FiniteDimensional F E
h : ∀ (x : E), finrank F { x_1 // x_1 ∈ F⟮x⟯ } ≤ 1
⊢ ⊥ = ⊤
apply bot_eq_top_of_finrank_adjoin_eq_one
no goals
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
S : Set E
K L : IntermediateField F E
inst✝ : FiniteDimensional F E
h : ∀ (x : E), finrank F { x_1 // x_1 ∈ F⟮x⟯ } ≤ 1
⊢ ∀ (x : E), finrank F { x_1 // x_1 ∈ F⟮x⟯ } = 1
exact fun x => by linarith [h x, show 0 < finrank F F⟮x⟯ from finrank_pos]
no goals
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
S : Set E
K L : IntermediateField F E
inst✝ : FiniteDimensional F E
h : ∀ (x : E), finrank F { x_1 // x_1 ∈ F⟮x⟯ } ≤ 1
x : E
⊢ finrank F { x_1 // x_1 ∈ F⟮x⟯ } = 1
linarith [h x, show 0 < finrank F F⟮x⟯ from finrank_pos]