no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.994751
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
j : Fin n
⊢ ↑(finSuccEquiv R n) (X (Fin.succ j)) = ↑Polynomial.C (X j)
simp