rw [biUnion_parts M]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ card M.A = ∑ i in range (M.t + 1), card (MultiPart.P M i)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ card (Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i) = ∑ i in range (M.t + 1), card (MultiPart.P M i)