no goals
σ : Type u_3
τ : Type ?u.204198
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
p : ℕ
φ : MvPolynomial σ R
⊢ ↑(map f) (↑(expand p) φ) = ↑(expand p) (↑(map f) φ)
simp [expand, map_bind₁]