Uniform weight bounds on a bounded exceptional set

theorem MagnitudeConjecture.reindexed_subtype_sum_le {α : Type u} {β : Type v} [Fintype α] [Fintype β] (e : α ≃ β) (P : β → Prop) [DecidablePred P] (w : α → ℕ) (B C : ℕ) (hcard : Nat.card { b : β // P b } ≤ C) (hw : ∀ (a : α), w a ≤ B) : ∑ a : { a : α // P (e a) }, w ↑a ≤ C * B

Relabelling a bounded exceptional set preserves a uniform bound on its total weight.