Lean: generate a variant theorem by programmatic splice instead of rewriting it

To make a variant of a long, already-compiling Lean proof that differs in one block (here, a sharper error-term estimate inside a Selberg-sieve theorem), I wrote no new proof by hand. A Python script extracted the original theorem text between its header and final linarith, cut out the old have herr block, and spliced in the new one. It then renamed the theorem (adding a prime) and applied a few identifier substitutions for the second application (sieve name, bound variable N→K). Both variants compiled with no or minimal fixes, and it cost far less than iterating on fresh proofs. Keep the shared skeleton (hsplit, hsift, hmain, final linarith) stable, and make the varying block a self-contained have with an explicit statement so the splice points are unambiguous.