∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {I : Type u_2}
  (f : MvPolynomial I R →ₐ[R] S),
  Function.Surjective ⇑f → Function.Surjective ⇑(MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))