mathlib

2f5afa10 - feat(tactic/compute_degree + test/compute_degree): introduce a tactic for proving `f.(nat_)degree ≤ d` (#14762)

feat(tactic/compute_degree + test/compute_degree): introduce a tactic for proving `f.(nat_)degree ≤ d` (#14762) This PR is a prequel to #14040. It introduces a simpler step than the actual computation of the degree. This step is used by the "main" tactic `compute_degree` defined in #14040. To help the reviewing process, I split this PR from the other one. For a very small sample of some golfing that could be done with this tactic, see [this diff](https://github.com/leanprover-community/mathlib/compare/adomani_compute_degree_le..adomani_compute_degree_le_golf), from #14776.