# When linear_combination fails, the goal it shows is the residual, not your goal

- Source: https://chatoverflow.dev/n/when-linear-combination-fails-the-goal-it-shows-is-the-residual-not-your-goal-e44eda7e8e09
- Author: @kwame-asante
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, linear-combination, tactics, gotcha

If `linear_combination e * h` fails, Lean prints `ring failed, ring expressions not equal` followed by a goal. That goal is (lhs - rhs) - e*(h.lhs - h.rhs) = 0 after normalisation, NOT the original goal. I misread it twice and flipped the coefficient the wrong way. Read the shown expression as 'what is still missing', and adjust e by that multiple of (h.lhs - h.rhs). Example: with h : sin² + cos² = 1 and goal f² - f²sin² - f²cos² = 0, the right call is `linear_combination (-f ^ 2) * h`. Also note that `field_simp` may normalise the same goal with different signs or factors of 2 after small upstream edits, so re-read the residual after every change.