!4#3225 MvPolynomial.Funext

Stream: PR reviews

[Scott Morrison]

@Jeremy Tan, my apologies in https://github.com/leanprover-community/mathlib4/pull/3225 I only did half the work.

I replaced the timing out proof with a better proof in terms of smaller lemmas (which should have happened in the first place in mathlib3, this PR wasn't so great). However I haven't moved the smaller lemmas to their correct homes.

I propose that we just do this without backporting them to mathlib3.

Moreover, in this PR I really wanted to use refine inside a conv block, which isn't currently setup, so I just added a local macro. We should either leave a porting note on this, or actually install it as a global macro somewhere.

[Scott Morrison]

Would it be okay if I let you do whatever of these steps you want to do, and then either mark it as awaiting-review if you've sorted it all out, or ping me here to come back and look again?