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
i : ι
⊢ f i ≤ ⨆ (i : (i : ι) × { x // x ∈ f i }), F⟮↑i.snd⟯
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 : ι) × { x // x ∈ f i }) (_ : i ∈ s), F⟮↑i.snd⟯
refine' exists_finset_of_mem_iSup (SetLike.le_def.mp (iSup_le (fun i => _)) hx)
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
i : ι
x : E
h : x ∈ f i
⊢ x ∈ ⨆ (i : (i : ι) × { x // x ∈ f i }), F⟮↑i.snd⟯
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
i : ι
⊢ f i ≤ ⨆ (i : (i : ι) × { x // x ∈ f i }), F⟮↑i.snd⟯
intro x h
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
i : ι
x : E
h : x ∈ f i
⊢ x ∈ ⨆ (i : (i : ι) × { x // x ∈ f i }), F⟮↑i.snd⟯
exact SetLike.le_def.mp (le_iSup_of_le ⟨i, x, h⟩ (by simp)) (mem_adjoin_simple_self F x)
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
i : ι
x : E
h : x ∈ f i
⊢ F⟮x⟯ ≤ F⟮↑{ fst := i, snd := { val := x, property := h } }.snd⟯
simp