Formatter emits trailing whitespace before multi-tactic `tacticSeq` arguments

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Pretty-printing a tactic with a multi-tactic indented tacticSeq argument leaves a trailing space on the row above the argument:

iterate 1␣          -- ← trailing space emitted by the formatter
  skip
  skip

At widths narrow enough to break the separator, it instead emits a whitespace-only blank line:

iterate 1
␣␣                  -- ← blank line containing two spaces
  skip
  skip

The defect is not iterate-specific: any ppSpace tacticSeq syntax triggers it (see the second block of the test case).

Context

Formatting of tactic sequences, e.g. via PrettyPrinter.ppCategory, produces output with trailing whitespace, which editors and linters flag and which git marks as whitespace errors. Related to the umbrella issue #369 (pretty printer is not yet at a point where we would reformat our code with it); related whitespace fixes #1945 and #3318 cover other formatters.

Steps to Reproduce

1. Save the following to mwe.lean:

import Lean
open Lean PrettyPrinter

#eval show CoreM Unit from do
  match Parser.runParserCategory (← getEnv) `tactic "iterate 1\n  skip\n  skip" "<mwe>" with
  | .error e => throwError e
  | .ok stx => IO.println <| repr <| (← ppCategory `tactic stx).pretty 100

syntax "myiter" num ppSpace tacticSeq : tactic

#eval show CoreM Unit from do
  match Parser.runParserCategory (← getEnv) `tactic "myiter 1\n  skip\n  skip" "<mwe>" with
  | .error e => throwError e
  | .ok stx => IO.println <| repr <| (← ppCategory `tactic stx).pretty 100

#eval show CoreM Unit from do
  match Parser.runParserCategory (← getEnv) `tactic "iterate 1\n  skip\n  skip" "<mwe>" with
  | .error e => throwError e
  | .ok stx => IO.println <| repr <| (← ppCategory `tactic stx).pretty 12

2. Run lean mwe.lean.

Expected behavior:

"iterate 1\n  skip\n  skip"
"myiter 1\n  skip\n  skip"
"iterate 1\n  skip\n  skip"

No trailing whitespace at any width.

Actual behavior:

"iterate 1 \n  skip\n  skip"
"myiter 1 \n  skip\n  skip"
"iterate 1\n  \n  skip\n  skip"

The first row ends with a space; at width 12 a whitespace-only blank line appears instead.

Versions

Lean (version 4.34.0-nightly-2026-08-05, arm64-apple-darwin24.6.0, commit f2bcf2e8660ab2d16cf3cb50c8e127de0439a337, Release)

Also reproduced on v4.31.0, v4.32.0, v4.33.0-rc2, and master 4c29de6f (2026-08-05).
macOS Darwin 25.5.0 arm64.

Additional Information

Cause: three parts interact.

1. sepByIndent.formatter (Lean/Parser/Extra.lean:211-224) prepends a forced align (pushAlign (force := true)) to a multi-item indented sequence: an unflattenable line break taken whenever the column reaches the sequence's indentation level.
2. The ppSpace before the argument (Init/TacticsExtra.lean:69) is a flattenable line in the enclosing group.
3. In the Std.Format fit check, everything up to that align fits on the row, so the line flattens to a space. The align then breaks immediately after it, stranding the space at end of row. If the line already broke to the align's column (narrow width), the align breaks again, leaving the whitespace-only blank line.

Controls that format correctly: a single-tactic argument (iterate 1 skip, no forced align) and a tacticSeq directly after a keyword with no ppSpace (all_goals).

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal reproduction in mwe.lean and inspect sepByIndent.formatter in Lean/Parser/Extra.lean alongside the ppSpace definition in Init/TacticsExtra.lean. Trace ppCategory formatting and the Std.Format fit behavior at widths 100 and 12; done means both outputs contain no trailing spaces or whitespace-only lines.