Specialized subagents for Lean 4 proof development workflows (proof-golfer, sorry-filler, axiom-eliminator, proof-repair)