no goals
σ : Type u_1
τ : Type u_3
R : Type u_2
S : Type ?u.281360
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : ℕ
φ : MvPolynomial σ R
⊢ ↑(rename f) (↑(expand p) φ) = ↑(expand p) (↑(rename f) φ)
simp [expand, bind₁_rename, rename_bind₁, Function.comp]