performance regression in ring

[alexjbest]

I don't have time to debug now but I just bisected what looks like a pretty bad performance regression in ring, coming from 085e7ab it seems.

According to the following

import Mathlib.Tactic.Ring

set_option profiler true
set_option maxHeartbeats 700000 in
lemma a [CommRing R] (a1 a2 a3 a4 a6 : R) (P : R × R) :
  -(a1 ^ 4 * a2 * a3 ^ 2 - a1 ^ 5 * a3 * a4 + a1 ^ 6 * a6 + 8 * a1 ^ 2 * a2 ^ 2 * a3 ^ 2
  - a1 ^ 3 * a3 ^ 3 - 8 * a1 ^ 3 * a2 * a3 * a4 - a1 ^ 4 * a4 ^ 2 + 12 * a1 ^ 4 * a2 * a6
  + 16 * a2 ^ 3 * a3 ^ 2 - 36 * a1 * a2 * a3 ^ 3 - 16 * a1 * a2 ^ 2 * a3 * a4
  + 30 * a1 ^ 2 * a3 ^ 2 * a4 - 8 * a1 ^ 2 * a2 * a4 ^ 2 + 48 * a1 ^ 2 * a2 ^ 2 * a6
  - 36 * a1 ^ 3 * a3 * a6 + 27 * a3 ^ 4 - 72 * a2 * a3 ^ 2 * a4 - 16 * a2 ^ 2 * a4 ^ 2
  + 96 * a1 * a3 * a4 ^ 2 + 64 * a2 ^ 3 * a6 - 144 * a1 * a2 * a3 * a6 - 72 * a1 ^ 2 * a4 * a6
  + 64 * a4 ^ 3 + 216 * a3 ^ 2 * a6 - 288 * a2 * a4 * a6 + 432 * a6 ^ 2) =
  -((48 * P.fst * P.snd * a2 ^ 2 + 24 * a1 * a2 * a6 + 216 * P.snd * a6 + P.snd * a1 ^ 6 +
  11 * P.snd * a1 ^ 4 * a2 + P.fst * a1 ^ 4 * a3 + 38 * P.fst * a1 ^ 2 * a2 * a3
  + 8 * a1 ^ 2 * a2 ^ 2 * a3 + a1 ^ 4 * a2 * a3 + 40 * P.snd * a1 ^ 2 * a2 ^ 2
  + 32 * P.snd * a2 ^ 3 + 24 * P.fst * P.snd * a1 * a3 + 30 * P.fst ^ 2 * a2 * a3
  + 3 * P.fst * a1 ^ 3 * a4 + 60 * P.fst ^ 2 * a1 * a4 + 30 * P.fst ^ 2 * a1 ^ 2 * a3
  + 31 * a1 ^ 2 * a3 * a4 + 144 * P.snd ^ 2 * a3 + 198 * P.snd * a3 ^ 2 + 27 * a3 ^ 3
  + 60 * a1 * a4 ^ 2 + 36 * P.fst * a1 * a6 + 76 * P.fst * a2 ^ 2 * a3
  + 16 * a2 ^ 3 * a3 + 84 * P.fst * a1 * a2 * a4 - (36 * a3 * a6 + P.fst ^ 2 * a1 ^ 5
  + P.fst * a1 ^ 5 * a2 + P.fst * P.snd * a1 ^ 4
  + 9 * P.fst ^ 2 * a1 ^ 3 * a2 + 10 * P.fst * a1 ^ 3 * a2 ^ 2 + a1 ^ 5 * a4
  + 6 * P.snd ^ 2 * a1 ^ 3 + 8 * P.fst * P.snd * a1 ^ 2 * a2 + 24 * P.fst ^ 2 * a1 * a2 ^ 2
  + 32 * P.fst * a1 * a2 ^ 3 + 35 * P.snd * a1 ^ 3 * a3 + a1 ^ 3 * a3 ^ 2 + 9 * a1 ^ 3 * a2 * a4
  + 48 * P.snd ^ 2 * a1 * a2 + 134 * P.snd * a1 * a2 * a3 + 27 * P.fst * a1 * a3 ^ 2
  + 36 * a1 * a2 * a3 ^ 2 + 58 * P.snd * a1 ^ 2 * a4 + 24 * a1 * a2 ^ 2 * a4
  + 144 * P.fst * P.snd * a4 + 120 * P.snd * a2 * a4 + 168 * P.fst * a3 * a4
  + 34 * a2 * a3 * a4)) * (2 * P.snd + a1 * P.fst + a3) + (a1 ^ 2 * a3 ^ 2 + 12 * a1 ^ 2 * a6
  + 16 * a2 ^ 2 * a4 + 32 * P.fst * a2 ^ 3 + a1 ^ 4 * a4 + 144 * P.fst * a6 + 48 * a2 * a6
  + P.fst * a1 ^ 4 * a2 + 84 * P.fst * a3 ^ 2 + 56 * P.snd * a1 * a4 + 8 * a1 ^ 2 * a2 * a4
  + 28 * P.snd * a1 ^ 2 * a3 + 52 * P.snd * a2 * a3 + 96 * P.fst * P.snd * a3
  + 8 * P.fst * a1 ^ 2 * a2 ^ 2 + 38 * a2 * a3 ^ 2 + 32 * P.fst ^ 2 * a2 ^ 2
  - (2 * P.fst * a1 ^ 3 * a3 + 112 * P.fst * a2 * a4 + a1 ^ 3 * a2 * a3 + 36 * a1 * a3 * a4
  + 96 * P.fst ^ 2 * a4 + 32 * P.fst * P.snd * a1 * a2 + 32 * P.snd * a1 * a2 ^ 2 + 64 * a4 ^ 2
  + 4 * P.fst * P.snd * a1 ^ 3 + 10 * P.snd * a1 ^ 3 * a2 + P.snd * a1 ^ 5 + 8 * a1 * a2 ^ 2 * a3
  + 46 * P.fst * a1 * a2 * a3)) * (a1 * P.snd - (3 * P.fst ^ 2 + 2 * a2 * P.fst + a4))
  + (60 * a1 ^ 2 * a4 + 288 * P.fst * a4 + 240 * a2 * a4 + 12 * P.snd * a1 ^ 3
  + 36 * a1 ^ 3 * a3 + 96 * P.snd * a1 * a2 + 168 * a1 * a2 * a3 - (432 * a6 + a1 ^ 6
  + 288 * P.snd * a3 + 252 * a3 ^ 2 + 12 * a1 ^ 4 * a2 + 48 * a1 ^ 2 * a2 ^ 2 + 96 * P.fst * a2 ^ 2
  + 64 * a2 ^ 3)) * (P.snd ^ 2 + a1 * P.fst * P.snd + a3 * P.snd - (P.fst ^ 3 + a2 * P.fst ^ 2
  + a4 * P.fst + a6)))
:= by ring

the runtime of ring jumps from 2-3s to 18-40s on my machine, from d419b09 to 085e7ab.

@digama0 any ideas, both the ring and norm_num internals were affected by this commit, but I can't see a smoking gun.