theorem function_field_generators (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] [IsAlgClosed k] [Algebra.EssFiniteType k F] (n : ℕ) (hdim : Algebra.trdeg k F = ↑n) : ∃ (t : Fin n → F) (α : F), AlgebraicIndependent k t ∧ IsAlgebraic (↥(IntermediateField.adjoin k (Set.range t))) α ∧ IntermediateField.adjoin k (insert α (Set.range t)) = ⊤