Theorem: Turanpartition.tn_turanNumb'_2 (Turan4/Turanpartition.lean)

State before:
t n : ℕ
⊢ 2 * turanNumb t n = n ^ 2 - turanNumb' t n
Tactic:
rw [← tn_turanNumb' t n]
State after:
t n : ℕ
⊢ 2 * turanNumb t n = turanNumb' t n + 2 * turanNumb t n - turanNumb' t n

State before:
t n : ℕ
⊢ 2 * turanNumb t n = turanNumb' t n + 2 * turanNumb t n - turanNumb' t n
Tactic:
exact (add_tsub_cancel_left _ _).symm
State after:
no goals