unfold mpDsum at this
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : mpDsum M ≤ 2 * turanNumb M.t (card M.A)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : ∑ v in M.A, degree (mp M) v ≤ 2 * turanNumb M.t (card M.A)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)