no goals
K : Type u
inst✝³ : Field K
L : Type u_2
inst✝² : Field L
f : K →+* L
a : L
S : Type u_1
inst✝¹ : CommSemiring S
inst✝ : Algebra S K[X]
p : S
⊢ eval f a (↑(algebraMap S (RatFunc K)) p) = Polynomial.eval₂ f a (↑(algebraMap S K[X]) p)
simp [eval, IsScalarTower.algebraMap_apply S K[X] (RatFunc K)]