split_ifs
α : 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)
⊢ card
      (M.A \
        if k ≠ i ∧ k ≠ j then MultiPart.P M k
        else if k = i then erase (MultiPart.P M i) v else insert v (MultiPart.P M j)) =
    if k ≠ i ∧ k ≠ j then card (M.A \ MultiPart.P M k)
    else if k = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1
case pos
α : 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
⊢ card (M.A \ MultiPart.P M k) = card (M.A \ MultiPart.P M k)

case pos
α : 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✝ : k = i
⊢ card (M.A \ erase (MultiPart.P M i) v) = card (M.A \ MultiPart.P M i) + 1

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✝ : ¬k = i
⊢ card (M.A \ insert v (MultiPart.P M j)) = card (M.A \ MultiPart.P M j) - 1