refactor: golf MvPolynomial.support_finSuccEquiv_nonempty (#11401)

Refactors the proof of this lemma. Adds a simp lemma to do this, and also adds MvPolynomial analogue

Mathlib/Algebra/MvPolynomial/Basic.lean

@@ -833,6 +833,10 @@ theorem support_eq_empty {p : MvPolynomial σ R} : p.support = ∅ ↔ p = 0 :=
   Finsupp.support_eq_empty
 #align mv_polynomial.support_eq_empty MvPolynomial.support_eq_empty
 
+@[simp]
+lemma support_nonempty {p : MvPolynomial σ R} : p.support.Nonempty ↔ p ≠ 0 := by
+  rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]
+
 theorem exists_coeff_ne_zero {p : MvPolynomial σ R} (h : p ≠ 0) : ∃ d, coeff d p ≠ 0 :=
   ne_zero_iff.mp h
 #align mv_polynomial.exists_coeff_ne_zero MvPolynomial.exists_coeff_ne_zero

Mathlib/Algebra/MvPolynomial/Equiv.lean

@@ -478,16 +478,10 @@ theorem finSuccEquiv_support' {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} :
     simp [h.1]
 #align mv_polynomial.fin_succ_equiv_support' MvPolynomial.finSuccEquiv_support'
 
+-- TODO: generalize `finSuccEquiv R n` to an arbitrary ZeroHom
 theorem support_finSuccEquiv_nonempty {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) :
     (finSuccEquiv R n f).support.Nonempty := by
-  simp only [Finset.nonempty_iff_ne_empty, Ne, Polynomial.support_eq_empty]
-  refine fun c => h ?_
-  let ii := (finSuccEquiv R n).symm
-  calc
-    f = ii (finSuccEquiv R n f) := by
-      simpa only [← AlgEquiv.invFun_eq_symm] using ((finSuccEquiv R n).left_inv f).symm
-    _ = ii 0 := by rw [c]
-    _ = 0 := by simp
+  rwa [Polynomial.support_nonempty, AddEquivClass.map_ne_zero_iff]
 #align mv_polynomial.support_fin_succ_equiv_nonempty MvPolynomial.support_finSuccEquiv_nonempty
 
 theorem degree_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) :