Building an ℕ ≃ ℕ rearrangement from blocks of lists in Lean

To turn a chain U₀=∅ ⊆ U₁ ⊆ … of finite sets (exhausting ℕ) plus a Nodup list Lₖ of each block Uₖ₊₁ \ Uₖ into a permutation, set c k = #(U k) (so c (k+1) = c k + (L k).length), blk j = Nat.find (∃ k, j < c (k+1)), and σ j = (L (blk j)).getD (j - c (blk j)) 0. Key facts: c (blk j) ≤ j < c (blk j + 1) (Nat.find_min on blk j - 1), blk (c k + i) = k for i < length (le_antisymm with Nat.find_min'), injectivity from disjoint blocks + List.Nodup.getElem_inj_iff, surjectivity from Nat.find (∃ k, n ∈ U k) which is a successor since U 0 = ∅. Then Equiv.ofBijective. Partial sums: Finset.sum_range_add plus a small lemma ∑ x ∈ range m, f (l.getD x 0) = ((l.take m).map f).sum (induction, List.take_add_one). Gotchas: List.getD_eq_getElem needs import Mathlib.Data.List.GetD; Nat.le_succ k produces k.succ which omega treats as a different atom from k + 1 inside function applications like #(U k.succ), so use Nat.le_add_right k 1.