rw [card_sdiff (sub_part hj.1)]
case neg
α : 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)
h : ¬(i ≠ i ∧ i ≠ j)
h_3 : i = i
h_4 : ¬(j ≠ i ∧ j ≠ j)
h_5 : ¬j = i
⊢ card (MultiPart.P M i) * (card M.A - card (MultiPart.P M i)) + card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    (card (MultiPart.P M i) - 1) * (card M.A - card (MultiPart.P M i) + 1) +
      (card (MultiPart.P M j) + 1) * (card (M.A \ MultiPart.P M j) - 1)
case neg
α : 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)
h : ¬(i ≠ i ∧ i ≠ j)
h_3 : i = i
h_4 : ¬(j ≠ i ∧ j ≠ j)
h_5 : ¬j = i
⊢ card (MultiPart.P M i) * (card M.A - card (MultiPart.P M i)) +
      card (MultiPart.P M j) * (card M.A - card (MultiPart.P M j)) <
    (card (MultiPart.P M i) - 1) * (card M.A - card (MultiPart.P M i) + 1) +
      (card (MultiPart.P M j) + 1) * (card M.A - card (MultiPart.P M j) - 1)