rw [mp_deg_sum M]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ v in M.A, degree (mp M) v + ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = card M.A ^ 2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card M.A ^ 2