feat(field_theory/adjoin): F⟮α⟯ ≤ K ↔ α ∈ K (#15420)

I was surprised that we didn't have this lemma already.

src/field_theory/adjoin.lean

@@ -389,6 +389,11 @@ begin
   rw [ϕ.injective key, subalgebra.coe_zero]
 end
 
+variables {F} {α}
+
+@[simp] lemma adjoin_simple_le_iff {K : intermediate_field F E} : F⟮α⟯ ≤ K ↔ α ∈ K :=
+adjoin_le_iff.trans set.singleton_subset_iff
+
 end adjoin_simple
 end adjoin_def
 

src/field_theory/primitive_element.lean

@@ -113,9 +113,7 @@ begin
       { rw ← add_sub_cancel α (c • β),
         exact F⟮γ⟯.sub_mem (mem_adjoin_simple_self F γ) (F⟮γ⟯.to_subalgebra.smul_mem β_in_Fγ c) },
       exact λ x hx, by cases hx; cases hx; cases hx; assumption },
-    { rw [adjoin_le_iff, set.le_eq_subset],
-      change {γ} ⊆ _,
-      rw set.singleton_subset_iff,
+    { rw [adjoin_simple_le_iff],
       have α_in_Fαβ : α ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (set.mem_insert α {β}),
       have β_in_Fαβ : β ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (set.mem_insert_of_mem α rfl),
       exact F⟮α,β⟯.add_mem α_in_Fαβ (F⟮α, β⟯.smul_mem β_in_Fαβ) } },