refine' Finset.sum_congr rfl _
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ x in range (M.t + 1), (card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2) =
    ∑ x in range (M.t + 1), card (MultiPart.P M x) * card M.A
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : ℕ),
    x ∈ range (M.t + 1) →
      card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2 =
        card (MultiPart.P M x) * card M.A