rw [← sum_degrees_eq_twice_card_edges]
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
⊢ 2 * card (edgeFinset (mp M)) < 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 : mpDsum M ≤ mpDsum N
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)