no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f✝ : R →+* S₁
g✝ : σ → S₁
f : R →+* S₁
g : σ → S₁
d : σ →₀ ℕ
r : R
⊢ ↑(eval₂Hom f g) (↑(monomial d) r) = ↑f r * Finsupp.prod d fun i k => g i ^ k
simp only [monomial_eq, RingHom.map_mul, eval₂Hom_C, Finsupp.prod, map_prod,
  RingHom.map_pow, eval₂Hom_X']