fintype instances for sigma types

instance instFintypeSigma {α : Type u_4} (β : α → Type u_5) [Fintype α] [(a : α) → Fintype (β a)] : Fintype (Sigma β)

@[simp]

theorem Finset.univ_sigma_univ {α : Type u_4} {β : α → Type u_5} [Fintype α] [(a : α) → Fintype (β a)] : (Finset.sigma Finset.univ fun a => Finset.univ) = Finset.univ

instance PSigma.fintype {α : Type u_4} {β : α → Type u_5} [Fintype α] [(a : α) → Fintype (β a)] : Fintype ((a : α) ×' β a)