Finiteness of sigma types

theorem Finite.instSigma {α : Type u_1} {β : α → Type u_2} [Finite α] [∀ (a : α), Finite (β a)] : Finite ((a : α) × β a)

theorem Finite.instPSigma {ι : Sort u_2} {π : ι → Sort u_3} [Finite ι] [∀ (i : ι), Finite (π i)] : Finite ((i : ι) ×' π i)