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 β

instance Finite.instPSum {α : Sort u_3} {β : Sort u_4} [Finite α] [Finite β] : Finite (α ⊕' β)

theorem Finite.psum_left {α : Sort u_3} {β : Sort u_4} [Finite (α ⊕' β)] : Finite α

theorem Finite.psum_right {α : Sort u_3} {β : Sort u_4} [Finite (α ⊕' β)] : Finite β