mathlib3

a15e64af - refactor(data/polynomial/degree/definitions): rw -> exact, use term mode proof (#5946)

refactor(data/polynomial/degree/definitions): rw -> exact, use term mode proof (#5946) Co-authors: `lean-gptf`, Stanislas Polu Co-authored-by: Jesse Michael Han <39395247+jesse-michael-han@users.noreply.github.com>