rw [mp_deg_sum M, mp_deg_sum (move M hvi hj), move_t hvi hj]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∑ w in M.A, degree (mp M) w < ∑ w in (move M hvi hj).A, degree (mp (move M hvi hj)) w
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) <
    ∑ i_1 in range (M.t + 1),
      card (MultiPart.P (move M hvi hj) i_1) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) i_1)