no goals
K : Type u_3
L : Type u_1
L' : Type u_2
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field L'
inst✝³ : Algebra K L
inst✝² : Algebra K L'
S : IntermediateField K L
inst✝¹ : Algebra L' L
inst✝ : IsScalarTower K L' L
U V : IntermediateField L' L
H : restrictScalars K U = restrictScalars K V
x : L
⊢ x ∈ U ↔ x ∈ V
rw [← mem_restrictScalars K, H, mem_restrictScalars]