no goals
σ : Type u_3
R : Type u_1
τ : Type ?u.97879
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
f : R →+* S
⊢ ↑(map f) (esymm σ R n) = esymm σ S n
simp_rw [esymm, map_sum, map_prod, map_X]