mathlib3

71786433 - feat(tactic/linear_combination): allow linear_combination to leave goal open (#15319)

feat(tactic/linear_combination): allow linear_combination to leave goal open (#15319) Previously, `linear_combination` was a finishing tactic: it would close the goal, or fail. This PR changes it to be more of a simplification tactic. The semantics are "subtract this linear combination from the goal and normalize." In the case where the linear combination *does* close the goal, this behavior is the same as before. This is a very convenient way to see what's missing from your linear combination. I imagine that people will often look at the remaining expression and modify the combination until the goal is closed. By request of @hrmacbeth the default normalizer is `ring SOP`. cc @digama0 Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>