apply card_insert_of_not_mem (uniq_part' hvi.1 hj.1 hj.2.symm hvi.2)
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : ¬k = i
⊢ card (insert v (MultiPart.P M j)) = card (MultiPart.P M j) + 1
no goals