This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221).

The signature of a theorem changed:
```lean
theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) :
    (p ^ m).coeff (n * m) = p.coeff n ^ m  -- <-- the order of the product was `n * m`
    (p ^ m).coeff (m * n) = p.coeff n ^ m  -- <-- and it became `m * n`
```
Modified files:
```
Data/Polynomial/Basic.lean
Data/Polynomial/Degree/Lemmas.lean
Data/Polynomial/Degree/Definitions.lean
Data/Polynomial/Coeff.lean  -- for a "`simp` can prove this" golf
```

This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221).

The signature of a theorem changed:
```lean
theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) :
    (p ^ m).coeff (n * m) = p.coeff n ^ m  -- <-- the order of the product was `n * m`
    (p ^ m).coeff (m * n) = p.coeff n ^ m  -- <-- and it became `m * n`
```
Modified files:
```
Data/Polynomial/Basic.lean
Data/Polynomial/Degree/Lemmas.lean
Data/Polynomial/Degree/Definitions.lean
Data/Polynomial/Coeff.lean  -- for a "`simp` can prove this" golf
```

This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221).

The signature of a theorem changed:
```lean
theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) :
    (p ^ m).coeff (n * m) = p.coeff n ^ m  -- <-- the order of the product was `n * m`
    (p ^ m).coeff (m * n) = p.coeff n ^ m  -- <-- and it became `m * n`
```
Modified files:
```
Data/Polynomial/Basic.lean
Data/Polynomial/Degree/Lemmas.lean
Data/Polynomial/Degree/Definitions.lean
Data/Polynomial/Coeff.lean  -- for a "`simp` can prove this" golf
```

This PR ports the whole `compute_degree` tactic from mathlib3.

The tactic makes progress on goals of the form
*  `natDegree f ≤ d`,
*  `degree f ≤ d`,
*  `natDegree f = d`,
*  `degree f = d`,
*  `coeff f n = r`.

The variant `compute_degree!` applies `norm_num` and `assumption` to all left-over goals.

For instance, here is a valid computation of the degree of the 105-th cyclotomic polynomial:
```lean
example : natDegree
    (1 + X + X ^ 2 - X ^ 5 - X ^ 6 - 2 * X ^ 7 - X ^ 8 - X ^ 9 + X ^ 12 + X ^ 13 + X ^ 14 +
        X ^ 15 + X ^ 16 + X ^ 17 - X ^ 20 - X ^ 22 - X ^ 24 - X ^ 26 - X ^ 28 + X ^ 31 + X ^ 32 +
        X ^ 33 + X ^ 34 + X ^ 35 + X ^ 36 - X ^ 39 - X ^ 40 - 2 * X ^ 41 - X ^ 42 - X ^ 43 +
        X ^ 46 + X ^ 47 + X ^ 48 : ℤ[X]) = 48 := by
  compute_degree!
```
(Lean takes approximately 3s on my computer to prove the computation above.)

Affected files:
```
Mathlib/Lean/Expr/Basic.lean
Mathlib/Tactic/ComputeDegree.lean
test/ComputeDegree.lean
```

This PR is a companion to #6221.  It uses the tactic `compute_degree` to golf two proofs and restore a proof closer to its mathlib3 version.

This PR is a companion to #6221.  It uses the tactic `compute_degree` to golf two proofs and restore a proof closer to its mathlib3 version.

This PR is a companion to #6221.  It uses the tactic `compute_degree` to golf two proofs and restore a proof closer to its mathlib3 version.