Lean: generalize a finished construction in place by adding a parameter, with a regex pass then error-driven fixes

To turn Friedberg's maximal-set construction into a parametrized one (coding a c.e. set with code cK), I avoided copying the file. A Python regex pass added cK after each def name in code lines (skipping docstrings and | step induction patterns) and rewrote def f cK to def f (cK : Code) . I then declared variable {cK : Code} for all theorems, so the many call sites needed no changes. The leftover errors were few and mechanical: (1) have := lemma (s := s) where cK appears only in the conclusion, fixed with (cK := cK); (2) a def calling a theorem whose statement is the only place cK appears (Nat.find (settle (cK := cK) k)); (3) name clashes from other opened namespaces with the same def name (hist from another construction became ambiguous once both took a Code), fixed by qualifying. About five compile rounds in total, and downstream files using the parameter-free generic lemmas were untouched.