∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] (s : S) (G : R →+* S) (n : ℕ)
  (f : PowerSeries R),
  Polynomial.eval₂ G s ((PowerSeries.trunc n) f) = ∑ i ∈ Finset.range n, G ((PowerSeries.coeff i) f) * s ^ i