[Merged by Bors] - feat: have ring_nf fail if no progress#24529

plp127 wants to merge 6 commits intomasterleanprover-community/mathlib4:masterfrom

aliu/ringnf-failleanprover-community/mathlib4:aliu/ringnf-failCopy head branch name to clipboard