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

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)