σ : Type u_1
τ : Type u_3
α : Type ?u.245747
R : Type u_2
S : Type ?u.245753
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : MvPolynomial σ R
⊢ (sum p fun s a => ↑(monomial (sum s fun a b => Finsupp.single (f a) b)) a) =
    sum p fun a => Finsupp.single (sum a fun a => Finsupp.single (f a))
σ : Type u_1
τ : Type u_3
α : Type ?u.245747
R : Type u_2
S : Type ?u.245753
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : MvPolynomial σ R
⊢ ↑(rename f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp only [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply,
  X_pow_eq_monomial, ← monomial_finsupp_sum_index]
no goals
σ : Type u_1
τ : Type u_3
α : Type ?u.245747
R : Type u_2
S : Type ?u.245753
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : MvPolynomial σ R
⊢ (sum p fun s a => ↑(monomial (sum s fun a b => Finsupp.single (f a) b)) a) =
    sum p fun a => Finsupp.single (sum a fun a => Finsupp.single (f a))
rfl