mathlib

b7048a4e - feat(tactic/linarith): improve parsing expressions into linear form (#2995)

feat(tactic/linarith): improve parsing expressions into linear form (#2995) This PR generalizes the parsing stage of `linarith`. It will try harder to recognize expressions as linear combinations of monomials, and will match monomials up to commutativity. ```lean example (u v r s t : ℚ) (h : 0 < u*(t*v + t*r + s)) : 0 < (t*(r + v) + s)*3*u := by linarith ``` This is helpful for #2637 . Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>