no goals
σ : Type u_1
τ : Type ?u.111976
R : Type u_2
S : Type ?u.111982
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : MvPolynomial σ R
⊢ ↑(expand 1) f = f
simp only [expand, pow_one, eval₂Hom_eq_bind₂, bind₂_C_left, RingHom.toMonoidHom_eq_coe,
  RingHom.coe_monoidHom_id, AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.id_apply]