σ : Type u_1
R : Type u_2
τ : Type ?u.193960
S : Type ?u.193963
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ (Finset.biUnion (powersetLen n univ) fun t => {∑ i in t, Finsupp.single i 1}) =
    image (fun t => ∑ i in t, Finsupp.single i 1) (powersetLen n univ)
σ : Type u_1
R : Type u_2
τ : Type ?u.193960
S : Type ?u.193963
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ support (esymm σ R n) = image (fun t => ∑ i in t, Finsupp.single i 1) (powersetLen n univ)
rw [support_esymm']
no goals
σ : Type u_1
R : Type u_2
τ : Type ?u.193960
S : Type ?u.193963
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ (Finset.biUnion (powersetLen n univ) fun t => {∑ i in t, Finsupp.single i 1}) =
    image (fun t => ∑ i in t, Finsupp.single i 1) (powersetLen n univ)
exact biUnion_singleton