rw [move_Pcard_sdiff hvi hj]
α : 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ (if k ≠ i ∧ k ≠ j then card (MultiPart.P M k)
      else if k = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1) *
      card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) k) =
    card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)

α : 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ k ∈ range (M.t + 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ ((if k ≠ i ∧ k ≠ j then card (MultiPart.P M k)
      else if k = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1) *
      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) =
    card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)

α : 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ k ∈ range (M.t + 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ k ∈ range (M.t + 1)