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 ∈ s.sym2 with ¬i.IsDiag, p i = ∑ i ∈ s.offDiag with i.1 < i.2, 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