mathlib

1ea49d0f - feat(tactic/linear_combination): add tactic for combining equations (#11646)

feat(tactic/linear_combination): add tactic for combining equations (#11646) This new tactic attempts to prove a target equation by creating a linear combination of a list of equalities. The name of this tactic is currently `linear_combination`, but I am open to other possible names. An example of how to use this tactic is shown below: ``` example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) : x*y = -2*y + 1 := by linear_combination (h1, 1) (h2, -2) ``` Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>