no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.896628
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
⊢ ↑(finSuccEquiv R n) p =
    ↑(eval₂Hom (RingHom.comp Polynomial.C C) fun i => Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i) p
rw [← finSuccEquiv_eq, RingHom.coe_coe]