intro hA ht him h1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
⊢ M.A = N.A → M.t = N.t → TuranPartition M → ¬TuranPartition N → mpDsum N < mpDsum M
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
⊢ mpDsum N < mpDsum M