case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F { x // x ∈ K }⟮x⟯)
S : Finset E
⊢ P (adjoin F ↑S)
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F { x // x ∈ K }⟮x⟯)
K : IntermediateField F E
hK : FG K
⊢ P K
obtain ⟨S, rfl⟩ := hK
no goals
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F { x // x ∈ K }⟮x⟯)
S : Finset E
⊢ P (adjoin F ↑S)
exact induction_on_adjoin_finset S P base fun K x _ hK => ih K x hK