obtain hf := bal_sum_f hb.1
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
hf :
  ∀ (f : ℕ → ℕ),
    ∑ i in range (t + 1), f (P i) =
      card (smallParts (_ : Balanced t P)) * f (minP t P) + card (largeParts (_ : Balanced t P)) * f (minP t P + 1)
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)