rw [mp_deg_sum_sq, mp_deg_sum_sq, hA]
α : 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
⊢ ∑ v in M.A, degree (mp M) v = ∑ v in N.A, degree (mp N) v
α : 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