no goals
σ : Type u_3
τ : Type ?u.1299781
R : Type u_1
S : Type u_2
T : Type ?u.1299790
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
⊢ ↑(bind₂ f) (↑(monomial d) 1) = ↑(monomial d) 1
rw [bind₂_monomial, f.map_one, one_mul]