theorem Finset.card_pi' {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} (ht : ∀ i ∉ s, ∃ (x : α i), t i = {x}) : (s.pi' t ⋯).card = ∏ i ∈ s, (t i).card