no goals
σ : Type u_3
R : Type u_1
τ : Type ?u.70471
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Algebra R S
f : σ → S
n : ℕ
⊢ ↑(aeval f) (esymm σ R n) = Multiset.esymm (Multiset.map f univ.val) n
simp_rw [esymm, aeval_sum, aeval_prod, aeval_X, Finset.esymm_map_val]