intro X h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : MultiPart α),
    (∀ (y : MultiPart α),
        InvImage WellFoundedRelation.rel sumSqC y x →
          ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N) →
      ∃ N, N.A = x.A ∧ N.t = x.t ∧ TuranPartition N ∧ mpDsum x ≤ mpDsum N
α : 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
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N