Pipe operator breaks whitespace sensitivity

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

Consider this code:

theorem foo {g : True → False} : False := by
  exact
g <| trivial

theorem foo' {g : True → False} : False := by
  exact
g trivial

Lean accepts the first theorem but produces multiple errors on the second theorem. Given that tactic scripts should be indentation-sensitive, I think that both versions should produce an error.

Context

This is a minimization of a mathlib issue. In mathlib, the code looks like this:

lemma coeff_preΨ_ne_zero {n : ℤ} (h : (n : R) ≠ 0) :
    (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) ≠ 0 := by
  induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat, Int.even_coe_nat]
      using W.coeff_preΨ'_ne_zero <| by exact_mod_cast h
  | neg n ih => simpa only [preΨ_neg, coeff_neg, neg_ne_zero, Int.natAbs_neg, even_neg]
      using ih <| neg_ne_zero.mp <| by exact_mod_cast h

lemma natDegree_preΨ_pos {n : ℤ} (hn : 2 < n.natAbs) (h : (n : R) ≠ 0) :
    0 < (W.preΨ n).natDegree := by
  induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat] using W.natDegree_preΨ'_pos hn <| by exact_mod_cast h
  | neg n ih => simpa only [preΨ_neg, natDegree_neg]
        using ih (by rwa [← Int.natAbs_neg]) <| neg_ne_zero.mp <| by exact_mod_cast h

Reducing the indentation of the final line of the second theorem causes an error. This seems confusing because the analogous line of the first theorem works fine, and the indentation used in the first theorem is what style guides recommend.

Steps to Reproduce

1. Copy the MWE above into live.lean-lang.org

Versions

4.11.0-nightly-2024-07-23 on live.lean-lang.org

Impact

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

Start by reproducing the minimal examples in live.lean-lang.org using Lean 4.11.0-nightly-2024-07-23, then compare the two theorem scripts and the indentation changes described in the issue. Done means the whitespace-sensitive behavior is consistent with the intended tactic-script indentation rules and the reported examples have appropriate diagnostics.