List lemmas

Small general-purpose List lemmas used across the library.

theorem List.sum_attach_map {α : Type u_1} {M : Type u_2} [AddMonoid M] (l : List α) (f : α → M) : (map (fun (i : { x : α // x ∈ l }) => f ↑i) l.attach).sum = (map f l).sum

Summing over l.attach equals summing over l; removes the attach plumbing that recursive definitions introduce for termination.