no goals
σ : Type u_1
R : Type u_2
τ : Type ?u.69783
S : Type ?u.69786
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
⊢ esymm σ R = Multiset.esymm (Multiset.map X univ.val)
refine' funext fun n => (Finset.esymm_map_val X _ n).symm