linarith
α : 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)
h3 : ∑ w in M.A, degree (mp M) w < ∑ w in M.A, degree (mp (move M hvi hj)) w
h1 :
  ∑ v in M.A, degree (mp M) v + ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    ∑ v_1 in M.A, degree (mp (move M hvi hj)) v_1 + ∑ i_1 in range (M.t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2
h2 :
  ∑ v_1 in M.A, degree (mp (move M hvi hj)) v_1 + ∑ i_1 in range (M.t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 =
    card M.A ^ 2
⊢ ∑ i_1 in range (M.t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 <
    ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2
no goals