case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
⊢ ∑ i in P.parts, card i = card (Finset.biUnion P.parts id)
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
⊢ ∑ i in P.parts, card i = card s
convert congr_arg Finset.card P.biUnion_parts
case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
⊢ ∑ i in P.parts, card i = ∑ u in P.parts, card (id u)
case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
⊢ ∑ i in P.parts, card i = card (Finset.biUnion P.parts id)
rw [card_biUnion P.supIndep.pairwiseDisjoint]
no goals
case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
⊢ ∑ i in P.parts, card i = ∑ u in P.parts, card (id u)
rfl