∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (b₁ b₂ : β),
  Finset.Ioo (Sum.inr b₁) (Sum.inr b₂) = Finset.map Function.Embedding.inr (Finset.Ioo b₁ b₂)