Summing a product after transposing two indices

TauCeti.sum_mul_swap compares ∑ k ∈ s, f k * g (Equiv.swap x y k) with ∑ k ∈ s, f k * g k: away from x and y the two sums agree termwise, so they differ only in that the terms f x * g x and f y * g y are replaced by f x * g y and f y * g x. The comparison is stated by adding the two exchanged pairs to the two sides rather than by subtracting them, so that it holds in a monoid without subtraction -- in particular over ℕ, where such a weighted sum is a convenient numerical measure of an arrangement of labels.

theorem TauCeti.sum_mul_swap {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [AddCommMonoid M] [Mul M] (f g : ι → M) {s : Finset ι} {x y : ι} (hx : x ∈ s) (hy : y ∈ s) (hne : x ≠ y) : ∑ k ∈ s, f k * g ((Equiv.swap x y) k) + (f x * g x + f y * g y) = ∑ k ∈ s, f k * g k + (f x * g y + f y * g x)

Transposing two indices of a weighted sum exchanges the two weights. Every term other than those at x and y is unchanged, so adding f x * g x + f y * g y to the transposed sum gives the original sum with f x * g y + f y * g x added.