Commit 2026-04-02 18:21 6dc769ab

fix(Tactic/Ring): sort terms when evaluating nested powers (#37494) ring currently misorders the terms in a product when evaluating nested powers. When evaluating e.g. (x^a*x)^b where x is an atom, it returns x^(a*b)*x^b even if b is supposed to come before a*b in the ordering on ExProds. We fix this by running evalMulProd instead of using the .mul constructor directly. This in effect does an insertion sort on the terms in the ExProds. We do a similar thing when evaluating multiplication.

/--
error: ring failed, ring expressions not equal
a : ℚ
m n : ℕ
⊢ a ^ n * a ^ (m * n) = a ^ (m * n) * a ^ n
-/
#guard_msgs in
example (a : ℚ) (m n : ℕ) : (a ^ (m + 1)) ^ n = a ^ (n * (m + 1)) := by ring1