F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ (i : ι), f i
this : (F⟮x⟯ ≤ ⨆ (i : ι), f i) → ∃ s, F⟮x⟯ ≤ ⨆ (i : ι) (_ : i ∈ s), f i
⊢ ∃ s, x ∈ ⨆ (i : ι) (_ : i ∈ s), f i
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ (i : ι), f i
⊢ ∃ s, x ∈ ⨆ (i : ι) (_ : i ∈ s), f i
have := (adjoin_simple_isCompactElement x : IsCompactElement F⟮x⟯).exists_finset_of_le_iSup
  (IntermediateField F E) f
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ (i : ι), f i
this : (x ∈ ⨆ (i : ι), f i) → ∃ s, x ∈ ⨆ (i : ι) (_ : i ∈ s), f i
⊢ ∃ s, x ∈ ⨆ (i : ι) (_ : i ∈ s), f i
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ (i : ι), f i
this : (F⟮x⟯ ≤ ⨆ (i : ι), f i) → ∃ s, F⟮x⟯ ≤ ⨆ (i : ι) (_ : i ∈ s), f i
⊢ ∃ s, x ∈ ⨆ (i : ι) (_ : i ∈ s), f i
simp only [adjoin_simple_le_iff] at this
no goals
F : Type u_2
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
ι : Type u_1
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ (i : ι), f i
this : (x ∈ ⨆ (i : ι), f i) → ∃ s, x ∈ ⨆ (i : ι) (_ : i ∈ s), f i
⊢ ∃ s, x ∈ ⨆ (i : ι) (_ : i ∈ s), f i
exact this hx