fix: restore trailing whitespace of nested tactic blocks in the info tree

This PR fixes the goal view showing the state after the enclosing tactic instead of the nested block's goal on the line after the last tactic of a nested `have ... := by` block or `·` bullet, e.g. after an empty `·` where the next tactic is about to be typed (#15053).

Tactic steps are elaborated without the trailing whitespace of their last token for incremental reuse (#11958), which is re-added to the resulting info trees afterwards. `InfoTree.addTrailing?` passed each node's own trailing whitespace to its children instead of the trailing being added, which cut off propagation at the `by` token node that `have ... := by tacs` expands to via `with_annotate_state`, so the last nested tactic never regained its whitespace. Term-level blocks ending a tactic step additionally hide behind an unsubstituted info hole at that point, so `evalSepTactics` now substitutes holes before re-adding.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UUFnG7QzKo9chq1i9qDkaR