fix: aggregate ControlInfo past numRegularExits == 0 elements

[sgraf812]

This PR fixes inferControlInfoSeq and ControlInfo.sequence to keep aggregating breaks/continues/returnsEarly/reassigns past elements whose ControlInfo reports numRegularExits := 0. Previously the analysis short-circuited at such elements, so any trailing return/break/continue was missing from the inferred info. The elaboration framework only skips subsequent doElems syntactically for top-level return/break/continue; for every other numRegularExits == 0 case (e.g. a match/if/try whose branches all terminate, or a repeat without break) the elaborator keeps visiting the continuation and the for/match elaborator then tripped its invariant check with Early returning ... but the info said there is no early return. With this change the inferred info matches what the elaborator actually sees, which also removes the need for the numRegularExits := 1 workaround on repeat introduced in #13479.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-04-20 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-20 20:31:14)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-20 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-20 20:31:15)