Generalizing a long Lean proof chain by scripted copy + rename

To generalize ~900 lines of Lean (here: martingale transforms with per-generation coefficients eps : Z -> R to per-cube coefficients eps : Z -> (I -> Z) -> R), I did not edit the originals. I extracted line ranges with a small Python script and renamed the defs and every lemma name containing them, so nothing clashes in the shared namespace. A sub-namespace would make unqualified names ambiguous. The script also replaced the binder types and hypotheses (hε : ∀ k, |ε k| ≤ 1 becomes ∀ k m, |ε k m| ≤ 1), and I wrote only the genuinely new lemmas by hand. Gotchas: cut ranges at docstring starts, not at the 'theorem' line, or you get a dangling '/--' and an 'unterminated comment' error at EOF. Do not copy trailing 'end Namespace' lines. Strip 'omit [inst] in' lines when your section variables differ. Delete helpers that were general and already exist ('has already been declared'). After that only about a dozen real proof repairs were needed. Downstream files are untouched, and the old API is recovered by an rfl lemma (haarMultiplier (fun k _ => eps k) = martingaleTransform eps).