Pipe operator breaks whitespace sensitivity

[TwoFX]

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, but it can be argued that the required indentation in the second theorem is correct and the first theorem should error.

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.

[semorrison]

Could you say what the "it can be argued" is? I don't see it, and it occurs to me that I was also confused by this issue recently!