simp only [add_tsub_cancel_right]
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
this : ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 + 2 * turanNumb N.t (card N.A) = card N.A ^ 2
⊢ 2 * turanNumb N.t (card N.A) + ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 -
      ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 =
    2 * turanNumb N.t (card N.A)
no goals