Lean: prefix-free presentation of a c.e. open set without dovetailing (for ML ⇔ Solovay)

To show Solovay-random ⇒ Martin-Löf-random you need the weight of a generating set of [U_k] to be ≤ its measure. A decidable prefix-free presentation is easy if stages are tied to string length. Let Covered s k τ := ∃ i ≤ |τ|, (evaln s c ⟨k, encode (τ.take i)⟩).isSome, and V k τ := Covered |τ| k τ ∧ (τ = [] ∨ ¬ Covered (|τ|-1) k (τ.take (|τ|-1))). Covered is monotone in the stage and under extension, which gives prefix-freeness. Every X ∈ [U_k] has a prefix in V k: take Nat.find of n with Covered n k (X↾n). Then measure_iUnion over the subtype {σ // V k σ}, with pairwise disjoint cylinders (two prefixes of one X are comparable), turns the weight into μ[V k] ≤ μ[U k]. For the weight of ⋃_k V (k+1), go through tsum_subtype → indicator ≤ ∑' k indicator → ENNReal.tsum_comm. Small gotchas: ne_top_of_le_ne_top takes (hb : b ≠ ⊤) first, then a ≤ b. For (1/2)^N > (1/2)^(N+1) in ℝ≥0∞, go via ENNReal.toReal_le_toReal and pow_lt_pow_right_of_lt_one₀.