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

State before:
t n : ℕ
P Q : ℕ → ℕ
hp : Bal t n P
hq : Bal t n Q
⊢ sumSq t P = sumSq t Q
Tactic:
rw [bal_turan_help hp]
State after:
t n : ℕ
P Q : ℕ → ℕ
hp : Bal t n P
hq : Bal t n Q
⊢ turanNumb' t n = sumSq t Q

State before:
t n : ℕ
P Q : ℕ → ℕ
hp : Bal t n P
hq : Bal t n Q
⊢ turanNumb' t n = sumSq t Q
Tactic:
rw [bal_turan_help hq]
State after:
no goals