no goals
K : Type u_2
L : Type u_1
L' : Type ?u.313025
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : { x // x ∈ S }
⊢ IsIntegral K x ↔ IsIntegral K ↑x
rw [← isAlgebraic_iff_isIntegral, isAlgebraic_iff, isAlgebraic_iff_isIntegral]