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

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.