have := mp_deg_sum_move ⟨hi, hv⟩ ⟨hj, ne⟩ hc
case neg.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)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ 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
α : 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)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
this :
  ∑ w in X.A, degree (mp X) w <
    ∑ w in (move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)).A,
      degree (mp (move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i))) w
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N