Lemmas on Finset.sum and Finset.prod involving Finset.sym2 or Finset.sym.

theorem Finset.sum_sym2_filter_not_isDiag {ι : Type u_1} {α : Type u_2} [LinearOrder ι] [AddCommMonoid α] (s : Finset ι) (p : Sym2 ι → α) : ∑ i ∈ filter (fun (i : Sym2 ι) => ¬i.IsDiag) s.sym2, p i = ∑ i ∈ filter (fun (i : ι × ι) => i.1 < i.2) s.offDiag, p s(i.1, i.2)

theorem Finset.sum_count_of_mem_sym {α : Type u_1} [DecidableEq α] {m : ℕ} {k : Sym α m} {s : Finset α} (hk : k ∈ s.sym m) : ∑ i ∈ s, Multiset.count i ↑k = m