rw [← sum_degrees_eq_twice_card_edges]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ 2 * card (edgeFinset (mp M)) ≤ 2 * turanNumb M.t (Fintype.card α)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)