rw [parts_union h, sum_union (parts_disjoint h)]
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ i in range (t + 1), f (P i) = card (smallParts h) * f (minP t P) + card (largeParts h) * f (minP t P + 1)
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in smallParts h, f (P x) + ∑ x in largeParts h, f (P x) =
    card (smallParts h) * f (minP t P) + card (largeParts h) * f (minP t P + 1)