case h
K : Type u_1
L : Type u_2
L' : Type ?u.81019
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ S : IntermediateField K L
x✝ : L
⊢ x✝ ∈ Subalgebra.toIntermediateField' S.toSubalgebra (_ : IsField { x // x ∈ S }) ↔ x✝ ∈ S
K : Type u_1
L : Type u_2
L' : Type ?u.81019
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ S : IntermediateField K L
⊢ Subalgebra.toIntermediateField' S.toSubalgebra (_ : IsField { x // x ∈ S }) = S
ext
no goals
case h
K : Type u_1
L : Type u_2
L' : Type ?u.81019
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ S : IntermediateField K L
x✝ : L
⊢ x✝ ∈ Subalgebra.toIntermediateField' S.toSubalgebra (_ : IsField { x // x ∈ S }) ↔ x✝ ∈ S
rfl