refine ⟨N, h1, h2, h3, ?_⟩
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
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)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
this : mpDsum X < mpDsum Y
N : MultiPart α
h1 : N.A = X.A
h2 : N.t = X.t
h3 : TuranPartition N
h4 : mpDsum Y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
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)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
this : mpDsum X < mpDsum Y
N : MultiPart α
h1 : N.A = X.A
h2 : N.t = X.t
h3 : TuranPartition N
h4 : mpDsum Y ≤ mpDsum N
⊢ mpDsum X ≤ mpDsum N