Weighted sums over a common part of every finite fiber

def MagnitudeConjecture.commonFiberEquiv {ι : Type u} {α : Type v} (F : ι → Finset α) (I : Finset α) (hI : ∀ (i : ι), I ⊆ F i) : { a : (i : ι) × ↥(F i) // ↑a.snd ∈ I } ≃ ι × ↥I

Restricting every fiber to the same contained set gives a product.

theorem MagnitudeConjecture.sum_common_fiber {ι : Type u} [Fintype ι] {α : Type v} [DecidableEq α] (F : ι → Finset α) (I : Finset α) (hI : ∀ (i : ι), I ⊆ F i) (w : ι → ℕ) : ∑ a : { a : (i : ι) × ↥(F i) // ↑a.snd ∈ I }, w (↑a).fst = I.card * ∑ i : ι, w i

A weight depending only on the label repeats once for each common shift.