decompose: remove maxHeartbeats from PadicLFunctions.seriesEval_mul #8534

Target: projects/PadicLFunctions/PadicLFunctions/MeasureR/FormalPsi.lean

Declaration: PadicLFunctions.seriesEval_mul

Origin: full cleanup of #7287. The theorem still requires:

set_option maxHeartbeats 1000000 in

The existing proof unfolds three seriesEval terms and performs the antidiagonal Cauchy-product rewrite inline. Removing the option from the unchanged proof previously caused a deterministic whnf timeout. On 2026-07-17, lean_profile_proof on the theorem also timed out after 180 seconds. Mathlib API search found no drop-in theorem for this summability-based evaluation; Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal remains the appropriate Cauchy-product API.

Required work:

• Run the complete /decompose-proof workflow on seriesEval_mul.
• Extract a mechanically useful helper or reorganize the proof so the local maxHeartbeats option can be removed.
• Preserve the theorem statement and all consumers.
• Do not add sorry or admit.

Verification:

• lake exe cache get
• lake build PadicLFunctions.MeasureR.FormalPsi
• lake build PadicLFunctions
• #print axioms PadicLFunctions.seriesEval_mul remains exactly propext, Classical.choice, Quot.sound
• zero new sorry/admit