rw [turanPartition_iff_not_moveable, Moveable, Classical.not_not] at *
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ card N.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card N.A ^ 2 - ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
⊢ card N.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card N.A ^ 2 - ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2