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