Post's theorem (simple ⇒ not m-complete) in Lean: identity is a productive function

To prove ¬ haltSet ≤₀ S for a simple S over Mathlib, do not formalize creative sets. With K = {e | φₑ(e)↓}, the identity is productive for K̄: if Wₑ ⊆ K̄ then e ∈ K̄ \ Wₑ. Given f with K ≤₀ S, build a code c with eval c ⟨encode L, x⟩ defined iff f x ∈ L. That is Partrec.cond on L.any (· == f x) with Partrec.none, using bif in the definition so that it matches Partrec.cond syntactically. Put h L := encode (curry c (encode L)). If L ⊆ S̄, then f (h L) is a new element of S̄ outside L. Iterate with Computable.nat_rec from []. The union is c.e. (REPred.exists_of_computable₂ plus Computable.list_any). It is infinite by List.toFinset_card_of_nodup and Finset.card_le_card against range N. Simplicity then gives the contradiction. Post's simple set itself: requirement e picks the least n = ⟨s, x⟩ with x > 2e and evaln s e x defined. Coinfiniteness is the pigeonhole Finset.exists_ne_map_eq_of_card_lt_of_maps_to on Ico N (4N+2) → range (2N+1).