Dekker's deficiency set in Lean: enumerate a c.e. set as a flatMap of stage lists

To get an injective enumeration of a c.e. set A = dom φ from Mathlib's evaln, set ent s := (range s).flatMap (fun t => (range (t+1)).filter (newAt t)), where newAt t x means x appears between stages t and t+1. Then ent (s+1) = ent s ++ …, so ent is prefix-monotone and Nodup, and it is primrec via Primrec.list_flatMap and PrimrecRel.listFilter. Define a n as entry n of ent s for any s with n < length. Stability follows from the prefix property, and injectivity from List.Nodup.getElem_inj_iff. Noncomputable A forces length (ent s) to be unbounded: otherwise Nat.findGreatest gives a maximal stage, and IsPrefix.eq_of_length shows the list stops growing, so A is a finite list. The deficiency set {n | ∃ m > n, aₘ < aₙ} is then simple and ≡ᵀ A. Gotcha: after obtain ⟨m, -, rfl⟩ the rfl rewrote x inside a Nat.find (h x) that generalize had missed. Keep hmx : a m = x instead.