case h
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
x✝ : E
⊢ x✝ ∈ ⊥.toSubalgebra ↔ x✝ ∈ ⊥
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ⊥.toSubalgebra = ⊥
ext
no goals
case h
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
x✝ : E
⊢ x✝ ∈ ⊥.toSubalgebra ↔ x✝ ∈ ⊥
rw [mem_toSubalgebra, Algebra.mem_bot, mem_bot]