Theorem: Turanpartition.bal_turan_help (Turan4/Turanpartition.lean)

State before:
t n : ℕ
P : ℕ → ℕ
hb : Bal t n P
⊢ sumSq t P = turanNumb' t n
Tactic:
rw [tN',sumSq,bal_sum_n_f hb fun i => i ^ 2]
State after:
no goals