If this line is absent, there are timeouts. Should I leave it this way?

At minimum, needs to have a -- Porting note

I'm trying to look at this now, but waiting on oleans / cache get! problems.

Two possibilities that I'd be okay with:

1. Leave it in, with a porting note
2. Split out two separate lemmas funext_fin_zero and funext_fin_succ.

Okay, the answer here is that this proof should never have been in mathlib3 in the first place. There is a lemma that should have been factored out:

theorem eval_eval_finSuccEquiv (f : MvPolynomial (Fin (n + 1)) R) :
    (eval x) (Polynomial.eval q (finSuccEquiv R n f)) = eval (Fin.cons (eval x q) x) f := sorry

private theorem funext_fin {n : ℕ} {p : MvPolynomial (Fin n) R}
    (h : ∀ x : Fin n → R, eval x p = 0) : p = 0 := by
  induction' n with n ih
  · apply (MvPolynomial.isEmptyRingEquiv R (Fin 0)).injective
    rw [RingEquiv.map_zero]
    convert h finZeroElim
  · apply (finSuccEquiv R n).injective
    simp only [AlgEquiv.map_zero]
    refine Polynomial.funext fun q => ?_
    rw [Polynomial.eval_zero]
    apply ih fun x => ?_
    calc _ = _ := eval_eval_finSuccEquiv p
         _ = 0 := h _

eval_eval_finSuccEquiv needs to be proved, and moved to Mathlib.Data.MvPolynomial.Equiv, after eval_eq_eval_mv_eval'.

In @jcommelin's defence, when he wrote this proof in leanprover-community/mathlib3#4196 the API in Mathlib.Data.MvPolynomial.Equiv wasn't as developed.

@Parcly-Taxel, do you want to tackle this? (Up to you of course.)

@Parcly-Taxel, I went down the rabbit hole and proved the theorem. There are some TODOs about things that need to be moved, still.

@semorrison Should we make a mathlib3 PR that moves the theorems to their proper files and rewrites funext_fin accordingly?

I think that would be a great idea, if you're up for it

I've done this now.