Commit 2026-10-01 10:46 16efc2c7

chore: remove linear_combination' tactic (#28925) When linear_combination was refactored in #15899, the old code was kept as the linear_combination' tactic, for easier migration. The consensus of the zulip discussion ([#mathlib4 > Narrowing the scope of `linear_combination` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Narrowing.20the.20scope.20of.20.60linear_combination.60/near/470237816)) was to wait, and "revisit this once people have experienced the various tactics in practice". Two years later, the old tactic has very few no uses: it is unused in mathlib; searching on github yields 160 hits --- most of which are in various forks of mathlib. Thus, removing this tactic seems appropriate. Compared to linear_combination, the primed version linear_combination' also supports e.g. multiplication of hypotheses. This is not supported by linear_combination directly, but the congr elaborator can be used.