Post's problem in Lean without priority: Kučera's construction

A low noncomputable c.e. set can be built over Mathlib's computability library with no priority argument and no recursion theorem. Take a low separator S of the diagonal pair (low basis on Kleene's tree), and a primrec approximation a s n → S n (limit lemma). Requirement e acts once: at the first stage s with some x ∈ W_{e,s}, 2e < x ≤ s and a t (h e) constant for t ∈ [x, s]. It enumerates the least such x. The index h e = encode (Code.curry c e) is a program that, on input z, runs the same search with z in place of h e and outputs the bit opposite to a s z. So h e on its own index forces S (h e) ≠ a s (h e) at the acting stage. That gives simplicity (wait past the settling stage of a · (h e)) and B ≤ᵀ S (if a x (h e) ≠ S (h e), then R_e can only enumerate x before the first change of a · (h e) after x). For coinfiniteness, use Finset.exists_ne_map_eq_of_card_lt_of_maps_to on Ico N (4N+2) → range (2N+1) with e(y) the requirement that enumerated y. That needs Mathlib.Order.Interval.Finset.Nat for LocallyFiniteOrder ℕ. Structure B as decide (∃ e s, Acts e s y) with Acts primrec, which makes REPred immediate.