R : Type u_2
inst✝ : CommSemiring R
σ : Type u_1
f : σ → R
s : Finset σ
n : ℕ
⊢ sum (map ((fun x => prod x) ∘ (fun x => map f x) ∘ Finset.val) (Finset.powersetLen n s).val) =
    ∑ t in Finset.powersetLen n s, Finset.prod t f
R : Type u_2
inst✝ : CommSemiring R
σ : Type u_1
f : σ → R
s : Finset σ
n : ℕ
⊢ esymm (map f s.val) n = ∑ t in Finset.powersetLen n s, Finset.prod t f
simp only [esymm, powersetLen_map, ← Finset.map_val_val_powersetLen, map_map]
no goals
R : Type u_2
inst✝ : CommSemiring R
σ : Type u_1
f : σ → R
s : Finset σ
n : ℕ
⊢ sum (map ((fun x => prod x) ∘ (fun x => map f x) ∘ Finset.val) (Finset.powersetLen n s).val) =
    ∑ t in Finset.powersetLen n s, Finset.prod t f
rfl