mathlib3

4e1eeebe - feat(tactic/linear_combination): allow combinations of arbitrary proofs (#14229)

feat(tactic/linear_combination): allow combinations of arbitrary proofs (#14229) This changes the syntax of `linear_combination` so that the combination is expressed using arithmetic operation. Credit to @digama0 for the parser. See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2313979.20arbitrary.20proof.20terms.20in.20.60linear_combination.60) for more details. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>