rw [move_Pcard hvi hj hvi.1, move_Pcard hvi hj hj.1, move_Pcard_sdiff hvi hj hvi.1,
  move_Pcard_sdiff hvi hj hj.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)
⊢ card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) + card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    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)
α : 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)
⊢ card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) + card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    ((if i ≠ i ∧ i ≠ j then card (MultiPart.P M i)
        else if i = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1) *
        if i ≠ i ∧ i ≠ j then card (M.A \ MultiPart.P M i)
        else if i = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1) +
      (if j ≠ i ∧ j ≠ j then card (MultiPart.P M j)
        else if j = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1) *
        if j ≠ i ∧ j ≠ j then card (M.A \ MultiPart.P M j)
        else if j = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1