unfold mpDsum at *
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
lt : mpDsum M < mpDsum N
le2 : mpDsum N ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : ∑ v in M.A, degree (mp M) v ≤ ∑ v in N.A, degree (mp N) v
lt : ∑ v in M.A, degree (mp M) v < ∑ v in N.A, degree (mp N) v
le2 : ∑ v in N.A, degree (mp N) v ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)