trySuggestions (exact? etc.) can produce wrongly indented source

[b-mehta]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

The result of clicking "Try this" after an exact? gives "type mismatch" and "unexpected identifier; expected command" errors.

theorem AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA :
    True → True → 1 = 2 := by 
  sorry

theorem test : 1 = 2 := by exact?

live.lean-lang.org version

Context

A student encountered this when using exact? on mathlib.

Steps to Reproduce

1. Code as above
2. Click the try this suggestion from exact?

Expected behavior: The result of exact? should close the goal.

Actual behavior: The result of exact? gives two errors, both of which are unhelpful to beginners.

Versions

Using live.lean-lang.org:
Lean 4.16.0-nightly-2025-01-10
Target: x86_64-unknown-linux-gnu

Impact

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

[nomeata]

This is the source after applying the suggestion:

theorem test : 1 = 2 := by exact
  AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA trivial
    trivial

The problem seems to be that the suggested output is wrapped and indented, but because the exact? was itself on the far right, the resulting code was wrong.

If we start with

theorem test : 1 = 2 := by
  exact?

it expands to

theorem test : 1 = 2 := by
  exact
    AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA trivial
      trivial

which works.

I have seen this before and assume that this is not exact? specific but will likewise apply to simp? etc.

[b-mehta]

I have seen this before and assume that this is not exact? specific but will likewise apply to simp? etc.

Indeed there is a similarity between this and #6006

[Kha]

This one unfortunately is much more complicated than the other issue as we would effectively need to reformat the entire by block. We want to get there with a general code formatter but it's not currently part of our roadmap.