no goals
σ : Type u_3
τ : Type ?u.1251650
R : Type u_1
S : Type u_2
T : Type ?u.1251659
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
r : R
⊢ ↑(bind₂ f) (↑(monomial d) r) = ↑f r * ↑(monomial d) 1
simp only [monomial_eq, RingHom.map_mul, bind₂_C_right, Finsupp.prod, map_prod,
  map_pow, bind₂_X_right, C_1, one_mul]