F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : Subfield E
HF : Set.range ↑(algebraMap F E) ⊆ ↑K
HS : S ⊆ ↑K
⊢ Set.range ↑(algebraMap F E) ∪ S ⊆ ↑K
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : Subfield E
HF : Set.range ↑(algebraMap F E) ⊆ ↑K
HS : S ⊆ ↑K
⊢ toSubfield (adjoin F S) ≤ K
apply Subfield.closure_le.mpr
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : Subfield E
HF : Set.range ↑(algebraMap F E) ⊆ ↑K
HS : S ⊆ ↑K
⊢ Set.range ↑(algebraMap F E) ⊆ ↑K ∧ S ⊆ ↑K
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : Subfield E
HF : Set.range ↑(algebraMap F E) ⊆ ↑K
HS : S ⊆ ↑K
⊢ Set.range ↑(algebraMap F E) ∪ S ⊆ ↑K
rw [Set.union_subset_iff]
no goals
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : Subfield E
HF : Set.range ↑(algebraMap F E) ⊆ ↑K
HS : S ⊆ ↑K
⊢ Set.range ↑(algebraMap F E) ⊆ ↑K ∧ S ⊆ ↑K
exact ⟨HF, HS⟩