apply sum_congr
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in largeParts h, f (P x) = ∑ x in largeParts h, f (minP t P + 1)
case e_a.h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ largeParts h = largeParts h

case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ largeParts h → f (P x) = f (minP t P + 1)