rw [Finset.card_eq_sum_ones, sum_mul, one_mul]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ ∑ i in MultiPart.P M x, degree (mp M) i = card (MultiPart.P M x) * card (M.A \ MultiPart.P M x)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ ∑ i in MultiPart.P M x, degree (mp M) i = ∑ x_1 in MultiPart.P M x, card (M.A \ MultiPart.P M x)