case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : IntermediateField F E
t : Finset E
ht : Algebra.adjoin F ↑t = S.toSubalgebra
⊢ FG S
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : IntermediateField F E
h : Subalgebra.FG S.toSubalgebra
⊢ FG S
cases' h with t ht
no goals
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : IntermediateField F E
t : Finset E
ht : Algebra.adjoin F ↑t = S.toSubalgebra
⊢ FG S
exact ⟨t, (eq_adjoin_of_eq_algebra_adjoin _ _ _ ht.symm).symm⟩