Membership in intermediate fields obtained by adjoining elements

Linear expressions a + b * x with coefficients in an intermediate field F belong to F ⊔ K⟮x⟯, without any algebraic relation on x.

theorem TauCeti.IntermediateField.mem_sup_adjoin_of_exists_add_mul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {x y : L} (hy : ∃ (a : L) (b : L), a ∈ F ∧ b ∈ F ∧ y = a + b * x) : y ∈ F ⊔ K⟮x⟯

If a and b lie in F, then a + b * x lies in F ⊔ K⟮x⟯.

theorem IntermediateField.adjoin_adjoinSimple_gen_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (α : L) : K⟮AdjoinSimple.gen K α⟯ = ⊤

The generator of K⟮α⟯ generates it: inside the field K⟮α⟯, adjoining the generator gives everything.