rw [← sum_erase_add ((range (M.t + 1)).erase j) _ (mem_erase_of_ne_of_mem hj.2.symm hvi.1)]
α : 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)
⊢ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) +
        card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    ∑ x in erase (range (M.t + 1)) j,
        card (MultiPart.P (move M hvi hj) x) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) x) +
      card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j)
α : 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)
⊢ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) +
        card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    ∑ x in erase (erase (range (M.t + 1)) j) i,
          card (MultiPart.P (move M hvi hj) x) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) x) +
        card (MultiPart.P (move M hvi hj) i) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) i) +
      card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j)