rw [mp_deg_sum_sq, ← card_univ, ← hu]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ ∑ v in M.A, degree (mp M) v = 2 * turanNumb M.t (Fintype.card α)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ card M.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = 2 * turanNumb M.t (card M.A)