K : Type u_2
L : Type u_1
L' : Type ?u.277529
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S F E : IntermediateField K L
⊢ (∀ (x : L), x ∈ F.toSubalgebra ↔ x ∈ E.toSubalgebra) ↔ ∀ (x : L), x ∈ ↑F ↔ x ∈ ↑E
K : Type u_2
L : Type u_1
L' : Type ?u.277529
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S F E : IntermediateField K L
⊢ F.toSubalgebra = E.toSubalgebra ↔ F = E
rw [SetLike.ext_iff, SetLike.ext'_iff, Set.ext_iff]
no goals
K : Type u_2
L : Type u_1
L' : Type ?u.277529
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S F E : IntermediateField K L
⊢ (∀ (x : L), x ∈ F.toSubalgebra ↔ x ∈ E.toSubalgebra) ↔ ∀ (x : L), x ∈ ↑F ↔ x ∈ ↑E
rfl