rw [← mul_add]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) * card (MultiPart.P M x) =
    card (MultiPart.P M x) * card M.A
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * (card (M.A \ MultiPart.P M x) + card (MultiPart.P M x)) = card (MultiPart.P M x) * card M.A