Some lemmas relating polynomials and multivariable polynomials.

theorem MvPolynomial.polynomial_eval_eval₂ {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommSemiring R] [CommSemiring S] {x : S} (f : R →+* Polynomial S) (g : σ → Polynomial S) (p : MvPolynomial σ R) : Polynomial.eval x (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ ((Polynomial.evalRingHom x).comp f) (fun (s : σ) => Polynomial.eval x (g s)) p

theorem MvPolynomial.eval_polynomial_eval_finSuccEquiv {R : Type u_1} {n : ℕ} {x : Fin n → R} [CommSemiring R] (f : MvPolynomial (Fin (n + 1)) R) (q : MvPolynomial (Fin n) R) : (MvPolynomial.eval x) (Polynomial.eval q ((MvPolynomial.finSuccEquiv R n) f)) = (MvPolynomial.eval fun (i : Fin (n + 1)) => Fin.cases ((MvPolynomial.eval x) q) x i) f