theorem MathlibNt.SieveTheory.sum_fibres_filter_image {α : Type u_1} {β : Type u_2} {M : Type u_3} [DecidableEq β] [AddCommMonoid M] (A : Finset α) (out : α → β) (P : β → Prop) [DecidablePred P] (w : α → M) : ∑ n ∈ Finset.image out A with P n, ∑ x ∈ A with out x = n, w x = ∑ x ∈ A with P (out x), w x

Push a labelled finite sum through an output predicate, retaining every fibre weight.