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

State before:
t n : ℕ
P : ℕ → ℕ
hp : Bal t n P
⊢ sumSq t P + 2 * turanNumb t n = n ^ 2
Tactic:
rw [bal_turan_help hp]
State after:
t n : ℕ
P : ℕ → ℕ
hp : Bal t n P
⊢ turanNumb' t n + 2 * turanNumb t n = n ^ 2

State before:
t n : ℕ
P : ℕ → ℕ
hp : Bal t n P
⊢ turanNumb' t n + 2 * turanNumb t n = n ^ 2
Tactic:
exact tn_turanNumb' t n
State after:
no goals