"Try this" suggestion includes trailing comments

[TwoFX]

Prerequisites

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

• [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [x] 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

If I have this code

theorem foo (h : 1 = 1) : 1 = 2 := sorry

theorem bar : 1 = 2 := by
  simpa? using foo (by simp)
  -- This is a comment
  -- This is another comment

Then the "Try this" suggestion in the infoview looks like this:

After accepting the suggestion, the code is turns into this:

theorem foo (h : 1 = 1) : 1 = 2 := sorry

theorem bar : 1 = 2 := by
  simpa only [Nat.reduceEqDiff] using
    foo
      (by simp)  -- This is a comment
          -- This is another comment
  -- This is a comment
  -- This is another comment

Now the comments are duplicated

Steps to Reproduce

1. Paste the above code into the Lean 4 web editor

Expected behavior: Comments are not included in the suggestion

Actual behavior: Comments are included, leading to duplication upon accepting the suggestion

Versions

4.10.0-nightly-2024-06-27

Impact

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

[TwoFX]

Jujian Zhang just ran into this while demoing Lean to a bunch of people in Durham :)