apply le_of_eq
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : TuranPartition N
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N ≤ 2 * turanNumb M.t (card M.A)
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : TuranPartition N
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N = 2 * turanNumb M.t (card M.A)