x generates the function field F(x)

Stream: Is there code for X?

[Michael Stoll]

I'm looking for a simple proof of the following:

import Mathlib

open scoped IntermediateField

example {F} [Field F] : F⟮RatFunc.X (K := F)⟯ = ⊤ := sorry

This looks like it should be in Mathlib, but apply? does not give anything useful, and
@loogle IntermediateField.adjoin, RatFunc.X

[loogle]

:shrug: nothing found

[Michael Stoll]

import Mathlib

open scoped IntermediateField

example {F} [Field F] : F⟮RatFunc.X (K := F)⟯ = ⊤ := by
    refine IntermediateField.ext fun a ↦ ⟨fun _ ↦ trivial, fun _ ↦ ?_⟩
    rw [IntermediateField.mem_adjoin_simple_iff]
    have (p : Polynomial F) : Polynomial.aeval X p = algebraMap (Polynomial F) (RatFunc F) p := by
      rw [← RatFunc.algebraMap_X, Polynomial.aeval_algebraMap_apply, Polynomial.aeval_X_left_apply]
    refine ⟨a.num, a.denom, ?_⟩
    simp only [this, num_div_denom]

Is there an easier way?