no goals
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1212003
T : Type ?u.1212006
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ f : σ → MvPolynomial τ R
d : σ →₀ ℕ
r : R
⊢ ↑(bind₁ f) (↑(monomial d) r) = ↑C r * ∏ i in d.support, f i ^ ↑d i
simp only [monomial_eq, AlgHom.map_mul, bind₁_C_right, Finsupp.prod, AlgHom.map_prod,
  AlgHom.map_pow, bind₁_X_right]