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>

src/ring_theory/polynomial/symmetric.lean

@@ -90,7 +90,7 @@ lemma neg (hφ : is_symmetric φ) : is_symmetric (-φ) :=
 λ e, by rw [alg_hom.map_neg, hφ]
 
 lemma sub (hφ : is_symmetric φ) (hψ : is_symmetric ψ) : is_symmetric (φ - ψ) :=
-λ e, by rw [alg_hom.map_sub, hφ, hψ]
+by { rw sub_eq_add_neg, exact hφ.add hψ.neg }
 
 end comm_ring