R : Type u_2
inst✝ : CommSemiring R
σ : Type u_1
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ Finset.card s
⊢ ∑ t in Finset.powersetLen (↑card s.val - k) s, Finset.prod t r =
    ∑ t in Finset.powersetLen (Finset.card s - k) s, ∏ i in t, r i
R : Type u_2
inst✝ : CommSemiring R
σ : Type u_1
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ Finset.card s
⊢ coeff (∏ i in s, (X + ↑C (r i))) k = ∑ t in Finset.powersetLen (Finset.card s - k) s, ∏ i in t, r i
rw [Finset.prod, prod_X_add_C_coeff' _ r h, Finset.esymm_map_val]
no goals
R : Type u_2
inst✝ : CommSemiring R
σ : Type u_1
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ Finset.card s
⊢ ∑ t in Finset.powersetLen (↑card s.val - k) s, Finset.prod t r =
    ∑ t in Finset.powersetLen (Finset.card s - k) s, ∏ i in t, r i
rfl