obtain ⟨i, hi, j, hj, v, hv, ne, hc⟩ := not_turanPartition_imp h'
case neg
α : 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
case neg.intro.intro.intro.intro.intro.intro.intro
α : 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
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N