case refine'_1
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), x ∈ S → P K → P (restrictScalars F { x // x ∈ K }⟮x⟯)
⊢ P (adjoin F ↑∅)

case refine'_2
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), x ∈ S → P K → P (restrictScalars F { x // x ∈ K }⟮x⟯)
a✝ : E
s✝ : Finset E
ha : a✝ ∈ S
x✝¹ : s✝ ⊆ S
x✝ : ¬a✝ ∈ s✝
h : P (adjoin F ↑s✝)
⊢ P (adjoin F ↑(insert a✝ s✝))
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), x ∈ S → P K → P (restrictScalars F { x // x ∈ K }⟮x⟯)
⊢ P (adjoin F ↑S)
refine' Finset.induction_on' S _ (fun ha _ _ h => _)
no goals
case refine'_1
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), x ∈ S → P K → P (restrictScalars F { x // x ∈ K }⟮x⟯)
⊢ P (adjoin F ↑∅)
simp [base]
case refine'_2
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), x ∈ S → P K → P (restrictScalars F { x // x ∈ K }⟮x⟯)
a✝ : E
s✝ : Finset E
ha : a✝ ∈ S
x✝¹ : s✝ ⊆ S
x✝ : ¬a✝ ∈ s✝
h : P (adjoin F ↑s✝)
⊢ P (restrictScalars F (adjoin { x // x ∈ adjoin F ↑s✝ } {a✝}))
case refine'_2
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), x ∈ S → P K → P (restrictScalars F { x // x ∈ K }⟮x⟯)
a✝ : E
s✝ : Finset E
ha : a✝ ∈ S
x✝¹ : s✝ ⊆ S
x✝ : ¬a✝ ∈ s✝
h : P (adjoin F ↑s✝)
⊢ P (adjoin F ↑(insert a✝ s✝))
rw [Finset.coe_insert, Set.insert_eq, Set.union_comm, ← adjoin_adjoin_left]
no goals
case refine'_2
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), x ∈ S → P K → P (restrictScalars F { x // x ∈ K }⟮x⟯)
a✝ : E
s✝ : Finset E
ha : a✝ ∈ S
x✝¹ : s✝ ⊆ S
x✝ : ¬a✝ ∈ s✝
h : P (adjoin F ↑s✝)
⊢ P (restrictScalars F (adjoin { x // x ∈ adjoin F ↑s✝ } {a✝}))
exact ih (adjoin F _) _ ha h