intro hA ht iM iN
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
⊢ M.A = N.A → M.t = N.t → TuranPartition M → TuranPartition N → mpDsum M = mpDsum N
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ mpDsum M = mpDsum N