no goals
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.79903
T : Type ?u.79906
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ f : σ → MvPolynomial τ R
x : R
⊢ ↑(bind₁ f) (↑C x) = ↑C x
simp [bind₁, algebraMap_eq]