diff --git a/Mathlib/Tactic/Abel.lean b/Mathlib/Tactic/Abel.lean
index f6e85e66d22811..e3c8190bb2adbb 100644
--- a/Mathlib/Tactic/Abel.lean
+++ b/Mathlib/Tactic/Abel.lean
@@ -506,7 +506,7 @@ elab (name := abelNF) "abel_nf" tk:"!"? cfg:optConfig loc:(location)? : tactic =
   let loc := (loc.map expandLocation).getD (.targets #[] true)
   let s ← IO.mkRef {}
   let m := AtomM.recurse s cfg.toConfig (wellBehavedDischarge := true) evalExpr (cleanup cfg)
-  transformAtLocation (m ·) "abel_nf" loc (failIfUnchanged := true) false
+  transformAtLocation (m ·) "abel_nf" loc (ifUnchanged := .error) false
 
 @[tactic_alt abel]
 macro "abel_nf!" cfg:optConfig loc:(location)? : tactic =>
diff --git a/Mathlib/Tactic/ByCases.lean b/Mathlib/Tactic/ByCases.lean
index 61eca0086a221f..357b9c6c824252 100644
--- a/Mathlib/Tactic/ByCases.lean
+++ b/Mathlib/Tactic/ByCases.lean
@@ -32,7 +32,7 @@ syntax (name := byCases!) "by_cases! " optConfig (atomic(ident " : "))? term : t
 
 local elab "try_push_neg_at" cfg:optConfig h:ident : tactic => do
   Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[h] false)
-    (failIfUnchanged := false)
+    (ifUnchanged := .silent)
 
 macro_rules
   | `(tactic| by_cases! $cfg:optConfig $e) => `(tactic| by_cases! $cfg h : $e)
diff --git a/Mathlib/Tactic/ByContra.lean b/Mathlib/Tactic/ByContra.lean
index ba616c9834018a..e47cd3d1b821e0 100644
--- a/Mathlib/Tactic/ByContra.lean
+++ b/Mathlib/Tactic/ByContra.lean
@@ -50,11 +50,11 @@ syntax (name := byContra!)
 
 local elab "try_push_neg_at" cfg:optConfig h:ident : tactic => do
   Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[h] false)
-    (failIfUnchanged := false)
+    (ifUnchanged := .silent)
 
 local elab "try_push_neg" cfg:optConfig : tactic => do
   Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[] true)
-    (failIfUnchanged := false)
+    (ifUnchanged := .silent)
 
 macro_rules
 | `(tactic| by_contra! $cfg $[$pat?]? $[: $ty?]?) => do
diff --git a/Mathlib/Tactic/Contrapose.lean b/Mathlib/Tactic/Contrapose.lean
index 65468a0f540d49..76306f4b2e3341 100644
--- a/Mathlib/Tactic/Contrapose.lean
+++ b/Mathlib/Tactic/Contrapose.lean
@@ -127,7 +127,7 @@ syntax (name := contrapose!)
 
 local elab "try_push_neg" cfg:optConfig : tactic => do
   Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[] true)
-    (failIfUnchanged := false)
+    (ifUnchanged := .silent)
 
 macro_rules
   | `(tactic| contrapose! $cfg) => `(tactic| (contrapose; try_push_neg $cfg))
diff --git a/Mathlib/Tactic/Field.lean b/Mathlib/Tactic/Field.lean
index e92e7097738209..e9ffcf0d056eda 100644
--- a/Mathlib/Tactic/Field.lean
+++ b/Mathlib/Tactic/Field.lean
@@ -69,7 +69,7 @@ elab (name := field) "field" d:(ppSpace discharger)? args:(ppSpace simpArgs)? :
   let s0 ← saveState
   -- run `field_simp` (only at the top level, not recursively)
   liftMetaTactic1 (transformAtTarget ((AtomM.run .reducible ∘ reduceProp disch) ·) "field"
-    (failIfUnchanged := False) · default)
+    (ifUnchanged := .silent) · default)
   let s1 ← saveState
   try
     -- run `ring1`
diff --git a/Mathlib/Tactic/FieldSimp.lean b/Mathlib/Tactic/FieldSimp.lean
index ed6186f84f59e9..bd9d4b3e24780f 100644
--- a/Mathlib/Tactic/FieldSimp.lean
+++ b/Mathlib/Tactic/FieldSimp.lean
@@ -711,7 +711,7 @@ elab (name := fieldSimp) "field_simp" d:(discharger)? args:(simpArgs)? loc:(loca
   let m := AtomM.recurse s { contextual := true } (wellBehavedDischarge := false)
     (fun e ↦ reduceProp disch e <|> reduceExpr disch e) cleanup
   let loc := (loc.map expandLocation).getD (.targets #[] true)
-  transformAtLocation (m ·) "field_simp" (failIfUnchanged := true) (mayCloseGoalFromHyp := true) loc
+  transformAtLocation (m ·) "field_simp" (ifUnchanged := .error) (mayCloseGoalFromHyp := true) loc
 
 /--
 `field_simp` normalizes an expression in a (semi-)field by rewriting it to a common denominator,
diff --git a/Mathlib/Tactic/Group.lean b/Mathlib/Tactic/Group.lean
index 88ad6698e1c580..316942299541c9 100644
--- a/Mathlib/Tactic/Group.lean
+++ b/Mathlib/Tactic/Group.lean
@@ -69,7 +69,7 @@ syntax (name := aux_group₂) "aux_group₂" (location)? : tactic
 
 macro_rules
 | `(tactic| aux_group₂ $[at $location]?) =>
-  `(tactic| ring_nf -failIfUnchanged $[at $location]?)
+  `(tactic| ring_nf (ifUnchanged := .silent) $[at $location]?)
 
 /-- `group` normalizes expressions in multiplicative groups that occur in the goal. `group` does not
 assume commutativity, instead using only the group axioms without any information about which group
diff --git a/Mathlib/Tactic/NormNum/Core.lean b/Mathlib/Tactic/NormNum/Core.lean
index 231444b5dc56ed..525357207dadae 100644
--- a/Mathlib/Tactic/NormNum/Core.lean
+++ b/Mathlib/Tactic/NormNum/Core.lean
@@ -261,7 +261,7 @@ def elabNormNum (cfg args loc : Syntax) (simpOnly := false) (useSimp := true) :
   let ctx ← getSimpContext cfg args (!useSimp || simpOnly)
   let loc := expandOptLocation loc
   transformAtNondepPropLocation (fun e ctx ↦ deriveSimp ctx useSimp e) "norm_num" loc
-    (failIfUnchanged := false) (mayCloseGoalFromHyp := true) ctx
+    (ifUnchanged := .silent) (mayCloseGoalFromHyp := true) ctx
 
 end Meta.NormNum
 
diff --git a/Mathlib/Tactic/Push.lean b/Mathlib/Tactic/Push.lean
index e1f951681515f7..cb1ca8c7602ed2 100644
--- a/Mathlib/Tactic/Push.lean
+++ b/Mathlib/Tactic/Push.lean
@@ -197,7 +197,7 @@ def elabHead (stx : Term) : TermElabM Head := withRef stx do
   | _ =>
     match ← resolvePushId? stx with
     | some (.const c _) => return .const c
-    | _ => throwError "Could not resolve `push` argument {stx}. \
+    | _ => throwError "Could not resolve `push` argument `{stx}`. \
       Expected either a constant, e.g. `push Not`, \
       or notation with underscores, e.g. `push ¬ _`"
 
@@ -209,9 +209,9 @@ def elabDischarger (stx : TSyntax ``discharger) : TacticM Simp.Discharge :=
 
 /-- Run the `push` tactic. -/
 def push (cfg : Config) (disch? : Option Simp.Discharge) (head : Head) (loc : Location)
-    (failIfUnchanged : Bool := true) : TacticM Unit := do
+    (ifUnchanged : BehaviorIfUnchanged := .error) : TacticM Unit := do
   let cfg := { distrib := cfg.distrib || (← getBoolOption `push_neg.use_distrib) }
-  transformAtLocation (pushCore head cfg disch? ·) s!"push {head}" loc failIfUnchanged
+  transformAtLocation (pushCore head cfg disch? ·) s!"push {head}" loc ifUnchanged
 
 /--
 `push c` rewrites the goal by pushing the constant `c` deeper into an expression.
@@ -318,7 +318,7 @@ elab (name := pull) "pull" disch?:(discharger)? head:(ppSpace colGt term) loc:(l
   let disch? ← disch?.mapM elabDischarger
   let head ← elabHead head
   let loc := (loc.map expandLocation).getD (.targets #[] true)
-  transformAtLocation (pullCore head · disch?) "pull" loc (failIfUnchanged := true) false
+  transformAtLocation (pullCore head · disch?) "pull" loc (ifUnchanged := .error) false
 
 /-- A simproc variant of `push fun _ ↦ _`, to be used as `simp [↓pushFun]`. -/
 simproc_decl _root_.pushFun (fun _ ↦ ?_) := pushStep .lambda {}
diff --git a/Mathlib/Tactic/ReduceModChar.lean b/Mathlib/Tactic/ReduceModChar.lean
index 149831d69531b9..11702f4f5e7b11 100644
--- a/Mathlib/Tactic/ReduceModChar.lean
+++ b/Mathlib/Tactic/ReduceModChar.lean
@@ -296,11 +296,11 @@ elab_rules : tactic
 | `(tactic| reduce_mod_char $[$loc]?) => unsafe do
   let loc := expandOptLocation (Lean.mkOptionalNode loc)
   transformAtNondepPropLocation (derive (expensive := false) ·) "reduce_mod_char" loc
-    (failIfUnchanged := false)
+    (ifUnchanged := .silent)
 | `(tactic| reduce_mod_char! $[$loc]?) => unsafe do
   let loc := expandOptLocation (Lean.mkOptionalNode loc)
   transformAtNondepPropLocation (derive (expensive := true) ·) "reduce_mod_char"
-    loc (failIfUnchanged := false)
+    loc (ifUnchanged := .silent)
 
 end ReduceModChar
 
diff --git a/Mathlib/Tactic/Ring/RingNF.lean b/Mathlib/Tactic/Ring/RingNF.lean
index 1261738959a7aa..1329877570144e 100644
--- a/Mathlib/Tactic/Ring/RingNF.lean
+++ b/Mathlib/Tactic/Ring/RingNF.lean
@@ -38,8 +38,8 @@ inductive RingMode where
 
 /-- Configuration for `ring_nf`. -/
 structure Config extends AtomM.Recurse.Config where
-  /-- if true, then fail if no progress is made -/
-  failIfUnchanged := true
+  /-- how to behave if no progress is made: warn, error or keep silent -/
+  ifUnchanged := BehaviorIfUnchanged.error
   /-- The normalization style. -/
   mode := RingMode.SOP
   deriving Inhabited, BEq, Repr
@@ -138,7 +138,7 @@ elab (name := ringNF) "ring_nf" tk:"!"? cfg:optConfig loc:(location)? : tactic =
   let loc := (loc.map expandLocation).getD (.targets #[] true)
   let s ← IO.mkRef {}
   let m := AtomM.recurse s cfg.toConfig (wellBehavedDischarge := true) evalExpr (cleanup cfg)
-  transformAtLocation (m ·) "ring_nf" loc cfg.failIfUnchanged false
+  transformAtLocation (m ·) "ring_nf" loc cfg.ifUnchanged false
 
 @[tactic_alt ringNF] macro "ring_nf!" cfg:optConfig loc:(location)? : tactic =>
   `(tactic| ring_nf ! $cfg:optConfig $(loc)?)
diff --git a/Mathlib/Tactic/WLOG.lean b/Mathlib/Tactic/WLOG.lean
index ca8c1cd07a6a33..f689340b80ff2b 100644
--- a/Mathlib/Tactic/WLOG.lean
+++ b/Mathlib/Tactic/WLOG.lean
@@ -133,7 +133,7 @@ def wlogCore (h : TSyntax ``binderIdent) (P : Term) (xs : Option (TSyntaxArray `
     reductionGoal.withContext do
       let negHygName := mkIdent <| ← reductionFVarIds.2.getUserName
       Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[(negHygName)] false)
-          (failIfUnchanged := false)
+        (ifUnchanged := .error)
 
 /-- `wlog h : P` adds an assumption `h : P` to the main goal, and adds a side goal that
 requires showing that the case `h : ¬ P` can be reduced to the case where `P` holds
diff --git a/Mathlib/Util/AtLocation.lean b/Mathlib/Util/AtLocation.lean
index dce5c65dad9610..7ff633fd0ceca1 100644
--- a/Mathlib/Util/AtLocation.lean
+++ b/Mathlib/Util/AtLocation.lean
@@ -47,18 +47,34 @@ def Lean.Elab.Tactic.withNondepPropLocation (loc : Location) (atLocal : FVarId 
 namespace Mathlib.Tactic
 open Lean Meta Elab.Tactic
 
+
+/-- Different settings of communicating about a tactic which made no progress:
+do nothing (keep silent), print a warning or throw an error. -/
+inductive BehaviorIfUnchanged where
+  /-- Don't log anything -/
+  | silent
+  /-- Log a warning -/
+  | warning
+  /-- Throw an error -/
+  | error
+deriving BEq, Inhabited, Repr
+
 /-- Use the procedure `m` to rewrite the provided goal.
 
 Assumes `proc` is not surrounded by backticks. -/
 def transformAtTarget (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
-    (failIfUnchanged : Bool) (goal : MVarId) :
+    (ifUnchanged : BehaviorIfUnchanged) (goal : MVarId) :
     ReaderT Simp.Context MetaM (Option MVarId) := do
   let tgt ← instantiateMVars (← goal.getType)
   let r ← m tgt
   -- we use expression equality here (rather than defeq) to be consistent with, e.g.,
   -- `applySimpResultToTarget`
   let unchanged := tgt.cleanupAnnotations == r.expr.cleanupAnnotations
-  if failIfUnchanged && unchanged then throwError "`{proc}` made no progress on the goal"
+  if unchanged then
+    match ifUnchanged with
+    | .warning => logWarning m!"`{proc}` made no progress on the goal"
+    | .error => throwError "`{proc}` made no progress on the goal"
+    | .silent => pure ()
   if r.expr.isTrue then
     goal.assign (← mkOfEqTrue (← r.getProof))
     pure none
@@ -76,7 +92,7 @@ this ensures that if the procedure `m` involves rewriting by this `SimpTheoremsA
 
 Assumes `proc` is not surrounded by backticks. -/
 def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
-    (failIfUnchanged : Bool) (mayCloseGoal : Bool) (fvarId : FVarId) (goal : MVarId) :
+    (ifUnchanged : BehaviorIfUnchanged) (mayCloseGoal : Bool) (fvarId : FVarId) (goal : MVarId) :
     ReaderT Simp.Context MetaM (Option MVarId) := do
   let ldecl ← fvarId.getDecl
   if ldecl.isImplementationDetail then
@@ -87,22 +103,26 @@ def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (
   let r ← withReader eraseFVarId <| m tgt
   -- we use expression equality here (rather than defeq) to be consistent with, e.g.,
   -- `applySimpResultToLocalDeclCore`
-  if failIfUnchanged && tgt.cleanupAnnotations == r.expr.cleanupAnnotations then
-    throwError "`{proc}` made no progress at `{Expr.fvar fvarId}`"
+  if tgt.cleanupAnnotations == r.expr.cleanupAnnotations then
+    match ifUnchanged with
+    | .warning => logWarning m!"`{proc}` made no progress at `{Expr.fvar fvarId}`"
+    | .error => throwError "`{proc}` made no progress at `{Expr.fvar fvarId}`"
+    | .silent => pure ()
   return (← applySimpResultToLocalDecl goal fvarId r mayCloseGoal).map Prod.snd
 
 /-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal).
 
 Assumes `proc` is not surrounded by backticks. -/
 def transformAtLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
-    (loc : Location) (failIfUnchanged : Bool := true) (mayCloseGoalFromHyp : Bool := false)
+    (loc : Location) (ifUnchanged : BehaviorIfUnchanged := .error)
+    (mayCloseGoalFromHyp : Bool := false)
     -- streamline the most common use case, in which the procedure `m`'s implementation is not
     -- simp-based and its `Simp.Context` is ignored
     (ctx : Simp.Context := default) :
     TacticM Unit :=
   withLocation loc
-    (liftMetaTactic1 ∘ (transformAtLocalDecl m proc failIfUnchanged mayCloseGoalFromHyp · · ctx))
-    (liftMetaTactic1 (transformAtTarget m proc failIfUnchanged · ctx))
+    (liftMetaTactic1 ∘ (transformAtLocalDecl m proc ifUnchanged mayCloseGoalFromHyp · · ctx))
+    (liftMetaTactic1 (transformAtTarget m proc ifUnchanged · ctx))
     fun _ ↦ throwError "`{proc}` made no progress anywhere"
 
 /-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal).
@@ -111,15 +131,15 @@ In the wildcard case (`*`), filter out all dependent and/or non-`Prop` hypothese
 
 Assumes `proc` is not surrounded by backticks. -/
 def transformAtNondepPropLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result)
-    (proc : String) (loc : Location) (failIfUnchanged : Bool := true)
+    (proc : String) (loc : Location) (ifUnchanged : BehaviorIfUnchanged := .error)
     (mayCloseGoalFromHyp : Bool := false)
     -- streamline the most common use case, in which the procedure `m`'s implementation is not
     -- simp-based and its `Simp.Context` is ignored
     (ctx : Simp.Context := default) :
     TacticM Unit :=
   withNondepPropLocation loc
-    (liftMetaTactic1 ∘ (transformAtLocalDecl m proc failIfUnchanged mayCloseGoalFromHyp · · ctx))
-    (liftMetaTactic1 (transformAtTarget m proc failIfUnchanged · ctx))
+    (liftMetaTactic1 ∘ (transformAtLocalDecl m proc ifUnchanged mayCloseGoalFromHyp · · ctx))
+    (liftMetaTactic1 (transformAtTarget m proc ifUnchanged · ctx))
     fun _ ↦ throwError "`{proc}` made no progress anywhere"
 
 end Mathlib.Tactic
diff --git a/MathlibTest/ring.lean b/MathlibTest/ring.lean
index daaf10c6427ae1..b43dd83432af4b 100644
--- a/MathlibTest/ring.lean
+++ b/MathlibTest/ring.lean
@@ -258,16 +258,16 @@ example (x : ℝ) (f : ℝ → ℝ) : True := by
   to use `fail_if_success` since the instances could change without warning.
   -/
   have : x = y := by
-    ring_nf -failIfUnchanged
+    ring_nf (ifUnchanged := .silent)
     ring_nf!
   have : x - y = 0 := by
-    ring_nf -failIfUnchanged
+    ring_nf (ifUnchanged := .silent)
     ring_nf!
   have : f x = f y := by
-    ring_nf -failIfUnchanged
+    ring_nf (ifUnchanged := .silent)
     ring_nf!
   have : f x - f y = 0 := by
-    ring_nf -failIfUnchanged
+    ring_nf (ifUnchanged := .silent)
     ring_nf!
   trivial