feat(tactic/compute_degree + test/compute_degree): a tactic for computing nat_degrees of polynomials

[adomani]

compute_degree tries to solve a goal of the form f.nat_degree = d or f.degree = d, where d : ℕ and f
satisfies:

• f is a sum of expression of the form
  C a * X ^ n, C a * X, C a, X ^ n, X, monomial n a, monomial n a * monomial m b,
• all exponents and the n in monomial n a are closed terms of type ℕ,
• the term with largest exponent is X ^ n and is the unique term of its degree (repetitions are
  allowed in terms of smaller degree).
  If the given degree does not match what the tactic computes, the tactic suggests the degree it
  computed.
  The tactic also reports when it is used with non-closed natural numbers as exponents.

There is a further tactic compute_degree_le, closing goals of the form f.nat_degree ≤ d, with similar, but slightly less stringent restrictions in f. Currently, compute_degree_le does not support degree, only nat_degree.

Zulip

---

• depends on: [Merged by Bors] - feat(tactic/compute_degree + test/compute_degree): introduce a tactic for proving f.(nat_)degree ≤ d #14762 for the implementation of compute_degree_le
• depends on: [Merged by Bors] - feat(tactic/move_add, test/move_add): a tactic for moving around summands #13483 for the implementation of move_add

[adomani]

@eric-wieser
The issues are partially solved.

• The recover was a consequence of using simp to prove a fact that simp was not actually able to prove. I fixed it by using simp + norm, even though norm_num alone would be sufficient, since this helps with speeding up the rest of the tactic.
• The slowness is still a little bit of an issue, but at least the tests do not timeout!

Overall, the main issue left for me is that of the speed of the tactic: it seems quite slow, but I do not know how to speed it up.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(tactic/compute_degree + test/compute_degree): introduce a tactic for proving f.(nat_)degree ≤ d #14762
• [Merged by Bors] - feat(tactic/move_add, test/move_add): a tactic for moving around summands #13483
  By Dependent Issues (🤖). Happy coding!