fix(tactic/ring_exp): X^(2^3) = X^8 not X^6 (#18645)

Apparently `ring_exp` didn't correctly handle the exponentiation of coefficients, returning the product instead of the power as a coefficient. It still returned the right `expr`, so the faulty value is only used when checking that two terms are the same and so we can add their coefficients. In other words, this bug could only be triggered when `ring_exp` ends up adding `X^(a^b)` with `X^(a*b)` where `a` and `b` are both numerals.

Thanks to @alainchmt for reporting the bug!

src/tactic/ring_exp.lean

@@ -1003,7 +1003,8 @@ meta def pow_coeff (p_p q_p : expr) (p q : coeff) : ring_exp_m (ex prod) := do
   ctx ← get_context,
   pq' ← mk_pow [p_p, q_p],
   (pq_p, pq_pf) ← lift $ norm_num.eval_pow pq',
-  pure $ ex.coeff ⟨pq_p, pq_p, pq_pf⟩ ⟨p.1 * q.1⟩
+  if q.value.denom ≠ 1 then lift $ fail!"Only integer powers are supported, not {q.value}."
+  else pure $ ex.coeff ⟨pq_p, pq_p, pq_pf⟩ ⟨p.1 ^ q.value.num⟩
 
 /--
 Exponentiate two expressions.

test/ring_exp.lean

@@ -79,6 +79,10 @@ by ring_exp_eq
 -- power does not have to be a syntactic match to `monoid.has_pow`
 example {α} [comm_ring α] (x : ℕ → α) : (x ^ 2 * x) = x ^ 3 := by ring_exp
 
+-- Powers in the exponent get evaluated correctly.
+example (X : ℤ) : (X^5 + 1) * (X^2^3 + X) = X^13 + X^8 + X^6 + X :=
+by ring_exp
+
 end exponentiation
 
 section power_of_sum