Commit 2024-08-22 23:39 b48de69e

fix: error positioning in linear_combination (#16072) A tweak to linear_combination so that when the default normalization tactic fails, the "red underlines" appear on the linear_combination call itself, rather than just on the "by" at the start of the proof. For example, compare before/after on this example:

import Mathlib
example {a : ℤ} (h : a = 1) : a = 2 := by
  linear_combination h

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Propagating.20errors.20through.20Unhygienic.2Erun