mathlib

c414df7d - feat(tactic/linear_combination): allow arbitrary proof terms (#13979)

feat(tactic/linear_combination): allow arbitrary proof terms (#13979) This extends `linear_combination` to allow arbitrary proof terms of equalities instead of just local hypotheses. ```lean constants (qc : ℚ) (hqc : qc = 2*qc) example (a b : ℚ) (h : ∀ p q : ℚ, p = q) : 3*a + qc = 3*b + 2*qc := by linear_combination (h a b, 3) (hqc) ``` This changes the syntax of `linear_combination` in the case where no coefficient is provided and it defaults to 1. A space-separated list of pexprs won't parse, since there's an ambiguity in `h1 h2` between an application or two arguments. So this case now requres parentheses around the argument: `linear_combination (h1, 3) (h2)` Does anyone object to this syntax change? Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>