Evaluating polynomials at germs of functions

A polynomial with coefficients in S evaluated at the germ of a function f : α → T, where the coefficients act on germs through a ring homomorphism S →+* (α → T) followed by the coercion to germs, is the germ of the pointwise evaluations (Filter.Germ.eval₂_coeRingHom_comp_coe).

theorem Filter.Germ.eval₂_coeRingHom_comp_coe {α : Type u_1} {S : Type u_2} {T : Type u_3} [Semiring S] [Semiring T] (l : Filter α) (u : S →+* α → T) (P : Polynomial S) (f : α → T) : Polynomial.eval₂ ((coeRingHom l).comp u) (↑f) P = ↑fun (y : α) => Polynomial.eval (f y) (Polynomial.map ((Pi.evalRingHom (fun (x : α) => T) y).comp u) P)

Evaluating a polynomial with coefficients in S at the germ of f : α → T, where the coefficients act on germs through u : S →+* (α → T) followed by the coercion to germs, gives the germ of the pointwise evaluations: at y, the coefficients are evaluated by u · y.