obtain ⟨N, hA, ht, iN, sN⟩ := moved M
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ mpDsum M ≤ 2 * turanNumb M.t (card M.A)
case intro.intro.intro.intro
α : 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 M ≤ 2 * turanNumb M.t (card M.A)