diff --git a/doc/examples/bintree.lean b/doc/examples/bintree.lean
index ff62f88c42c5..bb4fb73d1d95 100644
--- a/doc/examples/bintree.lean
+++ b/doc/examples/bintree.lean
@@ -282,7 +282,7 @@ theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β)
   let ⟨t, h⟩ := b; simp
   induction t with simp
   | leaf =>
-    split <;> simp <;> split <;> simp
+    split <;> (try simp) <;> split <;> (try simp)
     have_eq k k'
     contradiction
   | node left key value right ihl ihr =>
diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean
index 667af7dfce77..24409e9e0d02 100644
--- a/src/Init/Data/Nat/Linear.lean
+++ b/src/Init/Data/Nat/Linear.lean
@@ -353,7 +353,7 @@ theorem Poly.denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r
   | zero => assumption
   | succ fuel ih =>
     simp
-    split <;> simp at h <;> try assumption
+    split <;> try simp at h <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
     by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv]
     · apply ih; simp [denote_eq] at h |-; assumption
@@ -387,7 +387,7 @@ theorem Poly.of_denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
   | zero => assumption
   | succ fuel ih =>
     simp at h
-    split at h <;> simp <;> try assumption
+    split at h <;> try simp <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
     by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv] at h
     · have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
@@ -413,10 +413,9 @@ theorem Poly.of_denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
             rw [← Nat.add_assoc, ih, Nat.add_assoc]
 
 theorem Poly.denote_eq_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_eq ctx (m₁, m₂)) : denote_eq ctx (cancel m₁ m₂) := by
-  simp; apply denote_eq_cancelAux; simp [h]
+  apply denote_eq_cancelAux; simp [h]
 
 theorem Poly.of_denote_eq_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_eq ctx (cancel m₁ m₂)) : denote_eq ctx (m₁, m₂) := by
-  simp at h
   have := Poly.of_denote_eq_cancelAux (h := h)
   simp at this
   assumption
@@ -432,7 +431,7 @@ theorem Poly.denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r
   | zero => assumption
   | succ fuel ih =>
     simp
-    split <;> simp at h <;> try assumption
+    split <;> try simp at h <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
     by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv]
     · apply ih; simp [denote_le] at h |-; assumption
@@ -466,7 +465,7 @@ theorem Poly.of_denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
   | zero => assumption
   | succ fuel ih =>
     simp at h
-    split at h <;> simp <;> try assumption
+    split at h <;> try simp <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
     by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv] at h
     · have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
@@ -494,10 +493,9 @@ theorem Poly.of_denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
             exact this
 
 theorem Poly.denote_le_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_le ctx (m₁, m₂)) : denote_le ctx (cancel m₁ m₂) := by
-  simp; apply denote_le_cancelAux; simp [h]
+  apply denote_le_cancelAux; simp [h]
 
 theorem Poly.of_denote_le_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_le ctx (cancel m₁ m₂)) : denote_le ctx (m₁, m₂) := by
-  simp at h
   have := Poly.of_denote_le_cancelAux (h := h)
   simp at this
   assumption
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index b8060dacd1af..bba131d4228d 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -1229,7 +1229,7 @@ structure Config where
   autoUnfold        : Bool := false
   /-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all`
   will fail if they do not make progress. -/
-  failIfUnchanged   : Bool := false
+  failIfUnchanged   : Bool := true
   deriving Inhabited, BEq, Repr
 
 end DSimp
@@ -1260,7 +1260,7 @@ structure Config where
   dsimp             : Bool := true
   /-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all`
   will fail if they do not make progress. -/
-  failIfUnchanged   : Bool := false
+  failIfUnchanged   : Bool := true
   deriving Inhabited, BEq, Repr
 
 -- Configuration object for `simp_all`
diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean
index 3876f4f72e3b..60b6c0167ec6 100644
--- a/src/Init/WFTactics.lean
+++ b/src/Init/WFTactics.lean
@@ -10,7 +10,7 @@ import Init.WF
 /-- Unfold definitions commonly used in well founded relation definitions.
 This is primarily intended for internal use in `decreasing_tactic`. -/
 macro "simp_wf" : tactic =>
-  `(tactic| simp [invImage, InvImage, Prod.lex, sizeOfWFRel,
+  `(tactic| try simp [invImage, InvImage, Prod.lex, sizeOfWFRel,
           measure, Nat.lt_wfRel, WellFoundedRelation.rel])
 
 /-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case"
diff --git a/tests/lean/973b.lean b/tests/lean/973b.lean
index ad1a17f1f4d1..c2887d94ce79 100644
--- a/tests/lean/973b.lean
+++ b/tests/lean/973b.lean
@@ -7,5 +7,5 @@ theorem ex {x : Nat} {p : Nat → Prop} (h₁ : p x) (h₂ : q x p = x) : f x =
 
 set_option trace.Meta.Tactic.simp.discharge true
 theorem foo : f (f x) = x := by
-  simp
+  simp (config := { failIfUnchanged := false })
   sorry
diff --git a/tests/lean/dsimpZetaIssue.lean b/tests/lean/dsimpZetaIssue.lean
index d7ab6a439e0e..3347c15152e2 100644
--- a/tests/lean/dsimpZetaIssue.lean
+++ b/tests/lean/dsimpZetaIssue.lean
@@ -1,5 +1,5 @@
 example : let x := 0; x + 5 = 5 := by
-  dsimp (config := { zeta := false })
+  dsimp (config := { zeta := false, failIfUnchanged := false })
   trace_state
   simp
 
@@ -12,7 +12,7 @@ example : let x := 0; x + y = y := by
   rw [Nat.zero_add]
 
 example : let x := 0; x + y = y := by
-  dsimp (config := { zeta := false })
+  dsimp (config := { zeta := false, failIfUnchanged := false })
   trace_state
   conv => zeta
   trace_state
diff --git a/tests/lean/eraseSimp.lean b/tests/lean/eraseSimp.lean
index f52d35f84f2d..211b764b7c3f 100644
--- a/tests/lean/eraseSimp.lean
+++ b/tests/lean/eraseSimp.lean
@@ -12,7 +12,7 @@ section
 attribute [-simp] Nat.zero_add
 
 theorem ex2 {a b : Nat} (h₁ : a = b) : 0 + a = b := by
-  simp -- did not apply `Nat.zero_add`
+  fail_if_success simp -- did not apply `Nat.zero_add`
   rw [Nat.zero_add]
   assumption
 
@@ -24,6 +24,6 @@ theorem ex3 {a b : Nat} (h₁ : a = b) : 0 + a = b := by
   assumption
 
 theorem ex4 {a b : Nat} (h₁ : a = b) : 0 + a = b := by
-  simp [-Nat.zero_add]
+  fail_if_success simp [-Nat.zero_add]
   rw [Nat.zero_add]
   assumption
diff --git a/tests/lean/ppProofs.lean b/tests/lean/ppProofs.lean
index 35ce06374f10..9a8462d32ea0 100644
--- a/tests/lean/ppProofs.lean
+++ b/tests/lean/ppProofs.lean
@@ -2,7 +2,7 @@ set_option pp.analyze.trustSubst true
 set_option pp.proofs false
 example (h : α = β) : h ▸ (a : α) = (b : β) := _
 example (h : α = β) : id h ▸ (a : α) = (b : β) := _
-example (h : α = β) : id h ▸ (a : α) = (b : β) := by simp
+example (h : α = β) : id h ▸ (a : α) = (b : β) := by simp (config := { failIfUnchanged := false })
 set_option pp.proofs.withType false
 example (h : α = β) : id h ▸ (a : α) = (b : β) := _
 set_option pp.proofs true
diff --git a/tests/lean/ppProofs.lean.expected.out b/tests/lean/ppProofs.lean.expected.out
index ee0f6646f4d2..82e9547bb1b9 100644
--- a/tests/lean/ppProofs.lean.expected.out
+++ b/tests/lean/ppProofs.lean.expected.out
@@ -12,7 +12,7 @@ b : β
 a : α
 h : α = β
 ⊢ (_ : α = β) ▸ a = b
-ppProofs.lean:5:50-5:57: error: unsolved goals
+ppProofs.lean:5:50-5:98: error: unsolved goals
 α β : Sort ?u
 b : β
 a : α
diff --git a/tests/lean/root.lean b/tests/lean/root.lean
index 4d5a905b7389..53aa28e1fd6b 100644
--- a/tests/lean/root.lean
+++ b/tests/lean/root.lean
@@ -87,12 +87,12 @@ example : isEven (x+1+1) = isEven x := by simp -- Ok
 
 end Ex
 
-example : isEven (x+1+1) = isEven x := by simp; done -- Error
+example : isEven (x+1+1) = isEven x := by simp (config := { failIfUnchanged := false }); done -- Error
 
 open Ex in
 example : isEven (x+1+1) = isEven x := by simp -- Ok
 
-example : isEven (x+1+1) = isEven x := by simp; done -- Error
+example : isEven (x+1+1) = isEven x := by simp (config := { failIfUnchanged := false }); done -- Error
 
 namespace Foo
 
diff --git a/tests/lean/root.lean.expected.out b/tests/lean/root.lean.expected.out
index b023b96864a3..4f298108b409 100644
--- a/tests/lean/root.lean.expected.out
+++ b/tests/lean/root.lean.expected.out
@@ -8,9 +8,9 @@ root.lean:41:7-41:8: error: unknown identifier 'h'
 root.lean:43:7-43:8: error: unknown identifier 'f'
 Bla.f (x : Nat) : Nat
 prv (x : Nat) : Nat
-root.lean:90:48-90:52: error: unsolved goals
+root.lean:90:89-90:93: error: unsolved goals
 x : Nat
 ⊢ isEven (x + 1 + 1) = isEven x
-root.lean:95:48-95:52: error: unsolved goals
+root.lean:95:89-95:93: error: unsolved goals
 x : Nat
 ⊢ isEven (x + 1 + 1) = isEven x
diff --git a/tests/lean/run/1711.lean b/tests/lean/run/1711.lean
index 0d76cf8ad118..c297ed229cf9 100644
--- a/tests/lean/run/1711.lean
+++ b/tests/lean/run/1711.lean
@@ -20,7 +20,6 @@ theorem MulOneClass.ext {M : Type u} : ∀ ⦃m₁ m₂ : MulOneClass M⦄, m₁
       cases mul₂ with | mk mul₂ =>
         simp
         intro h
-        simp [toMul, Mul.mul] at h -- h : mul₁ = mul₂
         cases h
         have := (one_mul₂ one₁).symm.trans (mul_one₁ one₂) -- TODO: make sure we can apply after congr
         subst this
diff --git a/tests/lean/run/341.lean b/tests/lean/run/341.lean
index 531f212bf334..b81d2d20797b 100644
--- a/tests/lean/run/341.lean
+++ b/tests/lean/run/341.lean
@@ -102,7 +102,6 @@ namespace SetModel
            , tm := fun {γ} =>
                      (by
                        simp at fTy xTy; subst fTy xTy; simp at Actx Bctx; subst Actx Bctx
-                       simp [interpTyStep, cast] at *
                        exact (ftm xtm)
                      )
                }
diff --git a/tests/lean/run/387.lean b/tests/lean/run/387.lean
index 24b6c66cdbd1..73b1950f0d11 100644
--- a/tests/lean/run/387.lean
+++ b/tests/lean/run/387.lean
@@ -8,7 +8,8 @@ example (a : Nat) : p a a := by simp [foo a]
 example : p 0 0 := by simp [foo 0]
 example : p 0 0 := by simp [foo 0 0]
 example : p 0 0 := by
-  simp [foo 1] -- will not simplify
+  fail_if_success
+    simp [foo 1] -- will not simplify
   simp [foo 0]
 example : p 0 0 ∧ p 1 1 := by
   simp [foo 1]
diff --git a/tests/lean/run/constProp.lean b/tests/lean/run/constProp.lean
index a0849afaf5ff..27b3f04dbfbc 100644
--- a/tests/lean/run/constProp.lean
+++ b/tests/lean/run/constProp.lean
@@ -235,7 +235,7 @@ notation:60 "(" σ ", " s ")"  " ⇓ " σ':60 => Bigstep σ s σ'
 
 /- This proof can be automated using forward reasoning. -/
 theorem Bigstem.det (h₁ : (σ, s) ⇓ σ₁) (h₂ : (σ, s) ⇓ σ₂) : σ₁ = σ₂ := by
-  induction h₁ generalizing σ₂ <;> cases h₂ <;> simp_all
+  induction h₁ generalizing σ₂ <;> cases h₂ <;> try simp_all
   -- The rest of this proof should be automatic with congruence closure and a bit of forward reasoning
   case seq ih₁ ih₂ _ h₁ h₂ =>
     simp [ih₁ h₁] at ih₂
@@ -451,7 +451,7 @@ theorem State.erase_le (σ : State) : σ.erase x ≼ σ := by
   | [] => simp; apply le_refl
   | (y, v) :: σ =>
     simp
-    split <;> simp [*]
+    split <;> try simp [*]
     next => apply erase_le_cons; apply le_refl
     next => apply cons_le_cons; apply erase_le
 
diff --git a/tests/lean/run/declareConfigElabBug.lean b/tests/lean/run/declareConfigElabBug.lean
index cd2ec0e5290c..af9e7eec8f1e 100644
--- a/tests/lean/run/declareConfigElabBug.lean
+++ b/tests/lean/run/declareConfigElabBug.lean
@@ -1,5 +1,5 @@
 set_option trace.Elab true
 theorem ex (h : a = b) : (fun x => x) a = b := by
-  simp (config := { beta := false })
+  simp (config := { beta := false, failIfUnchanged := false })
   trace_state
   simp (config := { beta := true }) [h]
diff --git a/tests/lean/run/discrTreeSimp.lean b/tests/lean/run/discrTreeSimp.lean
index 4448bebc6e09..1e2c1b377fc2 100644
--- a/tests/lean/run/discrTreeSimp.lean
+++ b/tests/lean/run/discrTreeSimp.lean
@@ -8,7 +8,7 @@ theorem map_map (f : α → β) (g : β → γ) (xs : List α) : (xs.map f |>.ma
   sorry
 
 theorem ex1 (f : Nat → Nat) (xs : List Nat) : (xs.map f |>.map f) = xs.map (f ∘ f) := by
-  simp
+  fail_if_success simp
   simp [map_map]
   done
 
diff --git a/tests/lean/run/eqnsAtSimp2.lean b/tests/lean/run/eqnsAtSimp2.lean
index 862b4de62ba7..8d7424a2af75 100644
--- a/tests/lean/run/eqnsAtSimp2.lean
+++ b/tests/lean/run/eqnsAtSimp2.lean
@@ -29,11 +29,11 @@ theorem f_succ (x : Nat) : f (x+1) = f x * 2 := by
   simp
 
 theorem f_succ₂ (x : Nat) : f (x+1) = f x * 2 := by
-  simp [-f]
+  fail_if_success simp [-f]
   simp
 
 attribute [-simp] f
 
 theorem f_succ₃ (x : Nat) : f (x+1) = f x * 2 := by
-  simp
+  fail_if_success simp
   simp [f]
diff --git a/tests/lean/run/exfalsoBug.lean b/tests/lean/run/exfalsoBug.lean
index 441139a92780..f8da44ecf73d 100644
--- a/tests/lean/run/exfalsoBug.lean
+++ b/tests/lean/run/exfalsoBug.lean
@@ -72,7 +72,7 @@ theorem f_eq (n : Nat) :
   split
   next r h =>
     revert h
-    split <;> simp [f']
+    split <;> try simp [f']
     next => intro h; subst h; simp
     next hne =>
       cases n <;> simp [f']
@@ -80,7 +80,7 @@ theorem f_eq (n : Nat) :
       next n _ =>
        have : Nat.succ n - 1 = n := rfl
        rw [this]
-       split <;> simp
+       split <;> try simp
        next r hrn h₁ =>
          split <;> simp
          next => intro he; subst he; simp [*]
diff --git a/tests/lean/run/openInScopeBug.lean b/tests/lean/run/openInScopeBug.lean
index b1498aab4ca5..901068fdef5a 100644
--- a/tests/lean/run/openInScopeBug.lean
+++ b/tests/lean/run/openInScopeBug.lean
@@ -9,17 +9,22 @@ namespace Foo
 end Foo
 
 theorem ex1 : f (g (g (g x))) = x := by
-  simp -- does not use ax1 and ax2
+  fail_if_success simp -- does not use ax1 and ax2
   simp [Foo.ax1, Foo.ax2]
 
 theorem ex2 : f (g (g (g x))) = x :=
-  have h₁ : f (g (g (g x))) = f (g x) := by simp; /- try again with `Foo` scoped lemmas -/ open Foo in simp
-  have h₂ : f (g x) = x               := by simp; open Foo in simp
+  have h₁ : f (g (g (g x))) = f (g x) := by
+    fail_if_success simp
+    /- try again with `Foo` scoped lemmas -/
+    open Foo in simp
+  have h₂ : f (g x) = x               := by
+    fail_if_success simp
+    open Foo in simp
   Eq.trans h₁ h₂
   -- open Foo in simp -- works
 
 theorem ex3 : f (g (g (g x))) = x := by
-  simp
+  fail_if_success simp
   simp [Foo.ax1, Foo.ax2]
 
 open Foo in
@@ -28,5 +33,7 @@ theorem ex4 : f (g (g (g x))) = x := by
 
 theorem ex5 : f (g (g (g x))) = x ∧ f (g x) = x := by
   apply And.intro
-  { simp; open Foo in simp }
-  { simp; open Foo in simp }
+  { fail_if_success simp
+    open Foo in simp }
+  { fail_if_success simp
+    open Foo in simp }
diff --git a/tests/lean/run/simp4.lean b/tests/lean/run/simp4.lean
index 60528b6c4d89..19277d45cfa9 100644
--- a/tests/lean/run/simp4.lean
+++ b/tests/lean/run/simp4.lean
@@ -49,7 +49,7 @@ theorem ex8 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by
   simp (config := { contextual := true })
 
 theorem ex9 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by
-  simp
+  fail_if_success simp
   intro h₁ h₂
   simp [h₁] at h₂
   simp [h₂]
diff --git a/tests/lean/run/simp6.lean b/tests/lean/run/simp6.lean
index a35d361c950c..64f36a558c05 100644
--- a/tests/lean/run/simp6.lean
+++ b/tests/lean/run/simp6.lean
@@ -21,7 +21,7 @@ theorem ex6 : (if "hello" = "world" then 1 else 2) = 2 :=
 #print ex6
 
 theorem ex7 : (if "hello" = "world" then 1 else 2) = 2 := by
-  simp (config := { decide := false })
+  fail_if_success simp (config := { decide := false })
   simp
 
 theorem ex8 : (10 + 2000 = 20) = False :=
diff --git a/tests/lean/run/simpDischargeLoop.lean b/tests/lean/run/simpDischargeLoop.lean
index c658e567fb14..5abdeabba0dc 100644
--- a/tests/lean/run/simpDischargeLoop.lean
+++ b/tests/lean/run/simpDischargeLoop.lean
@@ -40,6 +40,6 @@ theorem double.inj'' : double n = double m → n = m := by
       apply ih h
 
 theorem double.inj''' : double n = double m → n = m := by
-  simp (config := { maxDischargeDepth := 2 })
-  simp (config := { maxSteps := 2000000 })
+  fail_if_success simp (config := { maxDischargeDepth := 2 })
+  fail_if_success simp (config := { maxSteps := 2000000 })
   admit
diff --git a/tests/lean/run/simpStar.lean b/tests/lean/run/simpStar.lean
index 7ef9d42a1e18..abdc7b707b0a 100644
--- a/tests/lean/run/simpStar.lean
+++ b/tests/lean/run/simpStar.lean
@@ -2,7 +2,7 @@ opaque f (x y : Nat) : Nat
 opaque g (x : Nat) : Nat
 
 theorem ex1 (x : Nat) (h₁ : f x x = g x) (h₂ : g x = x) : f x (f x x) = x := by
-  simp
+  fail_if_success simp
   simp [*]
 
 theorem ex2 (x : Nat) (h₁ : f x x = g x) (h₂ : g x = x) : f x (f x x) = x := by
diff --git a/tests/lean/simpZetaFalse.lean b/tests/lean/simpZetaFalse.lean
index bc17452d54c9..e4a92a94bfdb 100644
--- a/tests/lean/simpZetaFalse.lean
+++ b/tests/lean/simpZetaFalse.lean
@@ -16,7 +16,7 @@ theorem ex2 (x z : Nat) (h : f (f x) = x) (h' : z = x) : (let y := f (f x); y) =
 #print ex2 -- uses let_val_congr
 
 theorem ex3 (x z : Nat) : (let α := Nat; (fun x : α => 0 + x)) = id := by
-  simp (config := { zeta := false })
+  simp (config := { zeta := false, failIfUnchanged := false })
   trace_state -- should not simplify let body since `fun α : Nat => fun x : α => 0 + x` is not type correct
   simp [id]
 
diff --git a/tests/lean/simp_dsimp.lean b/tests/lean/simp_dsimp.lean
index eb0f14616b5f..fec3a72d506e 100644
--- a/tests/lean/simp_dsimp.lean
+++ b/tests/lean/simp_dsimp.lean
@@ -7,6 +7,6 @@ example (x : Nat) (a : A (x + 0)) : f (x + 0) a = x := by
   sorry
 
 example (x : Nat) (a : A (x + 0)) : f (x + 0) a = x := by
-  simp (config := { dsimp := false })
+  simp (config := { dsimp := false, failIfUnchanged := false })
   trace_state -- ⊢ f (x + 0) a = x
   sorry
diff --git a/tests/pkg/user_attr/UserAttr/Tst.lean b/tests/pkg/user_attr/UserAttr/Tst.lean
index 621bd1ee3fa3..53b664d876ea 100644
--- a/tests/pkg/user_attr/UserAttr/Tst.lean
+++ b/tests/pkg/user_attr/UserAttr/Tst.lean
@@ -26,7 +26,7 @@ def getFooAttrInfo? (declName : Name) : CoreM (Option (Nat × Bool)) :=
 @[my_simp] theorem g_eq : g x = x + 1 := rfl
 
 example : f x + g x = 2*x + 3 := by
-  simp_arith -- does not appy f_eq and g_eq
+  fail_if_success simp_arith -- does not appy f_eq and g_eq
   simp_arith [f, g]
 
 example : f x + g x = 2*x + 3 := by