mathlib3

c377e68e - refactor(ring_theory/polynomial/symmetric): simplify proof (#6135)

refactor(ring_theory/polynomial/symmetric): simplify proof (#6135) ... of `mv_polynomial.is_symmetric.sub` 2X smaller proof term Co-authors: `lean-gptf`, Stanislas Polu This was found by `formal-lean-wm-to-tt-m1-m2-v4-c4` when we evaluated it on theorems added to `mathlib` after we last extracted training data. Co-authored-by: Jesse Michael Han <39395247+jesse-michael-han@users.noreply.github.com>