Finiteness of sum types

instance Finite.instSum {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] : Finite (α ⊕ β)

theorem Finite.sum_left {α : Type u_1} (β : Type u_3) [Finite (α ⊕ β)] : Finite α

theorem Finite.sum_right {β : Type u_2} (α : Type u_3) [Finite (α ⊕ β)] : Finite β