diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean
index e86db46382fbd5..69260dc47ccc14 100644
--- a/Mathlib/NumberTheory/Padics/PadicNumbers.lean
+++ b/Mathlib/NumberTheory/Padics/PadicNumbers.lean
@@ -647,7 +647,7 @@ theorem exi_rat_seq_conv_cauchy : IsCauSeq (padicNorm p) (limSeq f) := fun ε h
   intro j hj
   suffices
     padicNormE (limSeq f j - f (max N N2) + (f (max N N2) - limSeq f (max N N2)) : ℚ_[p]) < ε by
-    ring_nf at this ⊢
+    ring_nf at this
     rw [← padicNormE.eq_padic_norm']
     exact mod_cast this
   apply lt_of_le_of_lt
diff --git a/Mathlib/Tactic/Group.lean b/Mathlib/Tactic/Group.lean
index ead2194e492093..f601ef20d59ea6 100644
--- a/Mathlib/Tactic/Group.lean
+++ b/Mathlib/Tactic/Group.lean
@@ -64,7 +64,7 @@ syntax (name := aux_group₂) "aux_group₂" (location)? : tactic
 
 macro_rules
 | `(tactic| aux_group₂ $[at $location]?) =>
-  `(tactic| ring_nf $[at $location]?)
+  `(tactic| ring_nf -failIfUnchanged $[at $location]?)
 
 /-- Tactic for normalizing expressions in multiplicative groups, without assuming
 commutativity, using only the group axioms without any information about which group
diff --git a/Mathlib/Tactic/Ring/RingNF.lean b/Mathlib/Tactic/Ring/RingNF.lean
index 3142f28a4ce931..7cc0164657a9ff 100644
--- a/Mathlib/Tactic/Ring/RingNF.lean
+++ b/Mathlib/Tactic/Ring/RingNF.lean
@@ -64,6 +64,8 @@ structure Config where
   zetaDelta := false
   /-- if true, atoms inside ring expressions will be reduced recursively -/
   recursive := true
+  /-- if true, then fail if no progess is made -/
+  failIfUnchanged := true
   /-- The normalization style. -/
   mode := RingMode.SOP
   deriving Inhabited, BEq, Repr
@@ -177,7 +179,10 @@ def ringNFTarget (s : IO.Ref AtomM.State) (cfg : Config) : TacticM Unit := withM
     goal.assign (← mkOfEqTrue (← r.getProof))
     replaceMainGoal []
   else
-    replaceMainGoal [← applySimpResultToTarget goal tgt r]
+    let newGoal ← applySimpResultToTarget goal tgt r
+    if cfg.failIfUnchanged && goal == newGoal then
+      throwError "ring_nf made no progress"
+    replaceMainGoal [newGoal]
 
 /-- Use `ring_nf` to rewrite hypothesis `h`. -/
 def ringNFLocalDecl (s : IO.Ref AtomM.State) (cfg : Config) (fvarId : FVarId) :
@@ -187,7 +192,10 @@ def ringNFLocalDecl (s : IO.Ref AtomM.State) (cfg : Config) (fvarId : FVarId) :
   let myres ← M.run s cfg <| rewrite tgt
   match ← applySimpResultToLocalDecl goal fvarId myres false with
   | none => replaceMainGoal []
-  | some (_, newGoal) => replaceMainGoal [newGoal]
+  | some (_, newGoal) =>
+    if cfg.failIfUnchanged && goal == newGoal then
+      throwError "ring_nf made no progress"
+    replaceMainGoal [newGoal]
 
 /--
 Simplification tactic for expressions in the language of commutative (semi)rings,
diff --git a/MathlibTest/ring.lean b/MathlibTest/ring.lean
index 69438c6b035db7..0525035fc672e9 100644
--- a/MathlibTest/ring.lean
+++ b/MathlibTest/ring.lean
@@ -210,17 +210,21 @@ end
 set_option linter.unusedTactic false in
 example (x : ℝ) (f : ℝ → ℝ) : True := by
   let y := x
+  /-
+  Two of these fail, and two of these succeed in rewriting the instance, so it's not a good idea
+  to use `fail_if_success` since the instances could change without warning.
+  -/
   have : x = y := by
-    ring_nf
+    ring_nf -failIfUnchanged
     ring_nf!
   have : x - y = 0 := by
-    ring_nf
+    ring_nf -failIfUnchanged
     ring_nf!
   have : f x = f y := by
-    ring_nf
+    ring_nf -failIfUnchanged
     ring_nf!
   have : f x - f y = 0 := by
-    ring_nf
+    ring_nf -failIfUnchanged
     ring_nf!
   trivial