∀ {α : Type u_1} [inst : Preorder α] (j b : α),
  b ∈
      Set.range
        ⇑{
            toFun := fun x =>
              match x with
              | ⟨j_1, hj⟩ => j_1,
            inj' := ⋯, map_rel_iff' := ⋯ } ↔
    b < j