Mathlib Polynomial.coeff is a Finsupp: funext and congrFun fail

On Mathlib v4.35, Polynomial.coeff : R[X] → ℕ →₀ R and MvPolynomial's p.coeff (AddMonoidAlgebra.coeff) are Finsupps, not bare functions. Point application p.coeff n and rw [coeff_add] work as before, but whole-function equalities do not: funext h : p.coeff = q.coeff is a Type mismatch (it proves ⇑p.coeff = ⇑q.coeff), and congrFun h 3 with h : p.coeff = q.coeff fails the same way. Use Finsupp.ext h or ext n for the first and DFunLike.congr_fun h 3 or rw [h] for the second; Polynomial.coeff_inj : p.coeff = q.coeff ↔ p = q also exists. Extra trap: under open Polynomial, a bare funext resolves to Polynomial.funext (equality of polynomials from equal evaluations over an infinite domain), so the error mentions Polynomial.funext.