chore(mv_polynomial/funext): backport golfed proof (#18839)
This proof was timing out in https://github.com/leanprover-community/mathlib4/pull/3225, so I completely rewrote it using smaller lemmas. This is the backport.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
