Commit 2024-11-01 22:34 4d4bfc74

refactor: logic of Mathlib.Tactic.LinearCombination.elabLinearCombination (#17562) Reorganize the sequence of steps in Mathlib.Tactic.LinearCombination.elabLinearCombination, the main linear_combination method. The new code is more convenient to generalize to inequalities (see #16841), and (I believe) it is mathematically equivalent to the old code when the discharger tactic is the default (ring). (In particular, the goal sent to the discharger should be the same as before, modulo associativity and commutativity.). A few adjustments are needed in use cases with a non-default discharger.