case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
x : E
⊢ x ∈ restrictScalars F ⊥ ↔ x ∈ K
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ restrictScalars F ⊥ = K
ext x
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
x : E
⊢ x ∈ Set.range ↑(algebraMap { x // x ∈ K } E) ↔ x ∈ K
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
x : E
⊢ x ∈ restrictScalars F ⊥ ↔ x ∈ K
rw [mem_restrictScalars, mem_bot]
no goals
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
x : E
⊢ x ∈ Set.range ↑(algebraMap { x // x ∈ K } E) ↔ x ∈ K
exact Set.ext_iff.mp Subtype.range_coe x