no goals
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Sort u_1
S : ι → IntermediateField F E
⊢ ↑(iInf S).toSubalgebra = ↑(⨅ (i : ι), (S i).toSubalgebra)
simp [iInf]