exact ⟨X, rfl, rfl, h', le_rfl⟩
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
h' : TuranPartition X
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
no goals