diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean
index 531747d6052f1..5cd662e30609b 100644
--- a/Mathlib/Algebra/BigOperators/Finprod.lean
+++ b/Mathlib/Algebra/BigOperators/Finprod.lean
@@ -1245,8 +1245,7 @@ theorem finprod_mem_finset_product' [DecidableEq α] [DecidableEq β] (s : Finse
     ∀ a,
       (∏ i : β in (s.filter fun ab => Prod.fst ab = a).image Prod.snd, f (a, i)) =
         (Finset.filter (fun ab => Prod.fst ab = a) s).prod f := by
-    refine' fun a => Finset.prod_bij (fun b _ => (a, b)) _ _ _ _ <;>-- `finish` closes these goals
-      try simp; done
+    refine' fun a => Finset.prod_bij (fun b _ => (a, b)) _ _ _ _ <;> simp
     suffices ∀ a' b, (a', b) ∈ s → a' = a → (a, b) ∈ s ∧ a' = a by simpa
     rintro a' b hp rfl
     exact ⟨hp, rfl⟩
diff --git a/Mathlib/Algebra/CubicDiscriminant.lean b/Mathlib/Algebra/CubicDiscriminant.lean
index da41f51aa055f..0dbda7aa066c5 100644
--- a/Mathlib/Algebra/CubicDiscriminant.lean
+++ b/Mathlib/Algebra/CubicDiscriminant.lean
@@ -291,7 +291,7 @@ def equiv : Cubic R ≃ { p : R[X] // p.degree ≤ 3 } where
     -- Porting note: Added `simp only [Nat.zero_eq, Nat.succ_eq_add_one] <;> ring_nf`
     -- There's probably a better way to do this.
     ext (_ | _ | _ | _ | n) <;> simp only [Nat.zero_eq, Nat.succ_eq_add_one] <;> ring_nf
-      <;> simp only [coeffs]
+      <;> try simp only [coeffs]
     have h3 : 3 < 4 + n := by linarith only
     rw [coeff_eq_zero h3,
       (degree_le_iff_coeff_zero (f : R[X]) 3).mp f.2 _ <| WithBot.coe_lt_coe.mpr (by exact h3)]
diff --git a/Mathlib/Algebra/Star/CHSH.lean b/Mathlib/Algebra/Star/CHSH.lean
index 1071c14637cd9..ffef52b581cc6 100644
--- a/Mathlib/Algebra/Star/CHSH.lean
+++ b/Mathlib/Algebra/Star/CHSH.lean
@@ -170,8 +170,8 @@ we prepare some easy lemmas about √2.
 theorem tsirelson_inequality_aux : √2 * √2 ^ 3 = √2 * (2 * √2⁻¹ + 4 * (√2⁻¹ * 2⁻¹)) := by
   ring_nf
   rw [mul_inv_cancel (ne_of_gt (Real.sqrt_pos.2 (show (2 : ℝ) > 0 by norm_num)))]
-  convert congr_arg (· ^ 2) (@Real.sq_sqrt 2 (by norm_num)) using 1 <;> simp only [← pow_mul] <;>
-    norm_num
+  convert congr_arg (· ^ 2) (@Real.sq_sqrt 2 (by norm_num)) using 1 <;>
+    (try simp only [← pow_mul]) <;> norm_num
 #align tsirelson_inequality.tsirelson_inequality_aux TsirelsonInequality.tsirelson_inequality_aux
 
 theorem sqrt_two_inv_mul_self : √2⁻¹ * √2⁻¹ = (2⁻¹ : ℝ) := by
diff --git a/Mathlib/AlgebraicTopology/SimplexCategory.lean b/Mathlib/AlgebraicTopology/SimplexCategory.lean
index b74ffdc5291d1..222f67885a46c 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory.lean
@@ -215,8 +215,6 @@ theorem δ_comp_δ {n} {i j : Fin (n + 2)} (H : i ≤ j) :
     δ i ≫ δ j.succ = δ j ≫ δ (Fin.castSucc i) := by
   ext k
   dsimp [δ, Fin.succAbove]
-  simp only [OrderEmbedding.toOrderHom_coe, OrderEmbedding.coe_ofStrictMono, Function.comp_apply,
-    SimplexCategory.Hom.toOrderHom_mk, OrderHom.comp_coe]
   rcases i with ⟨i, _⟩
   rcases j with ⟨j, _⟩
   rcases k with ⟨k, _⟩
@@ -279,7 +277,8 @@ theorem δ_comp_σ_self {n} {i : Fin (n + 1)} :
   dsimp [σ, δ, Fin.predAbove, Fin.succAbove]
   simp [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.dite_val]
   split_ifs
-  all_goals try simp <;> linarith
+  any_goals simp
+  all_goals linarith
 #align simplex_category.δ_comp_σ_self SimplexCategory.δ_comp_σ_self
 
 @[reassoc]
@@ -296,7 +295,6 @@ theorem δ_comp_σ_succ {n} {i : Fin (n + 1)} : δ i.succ ≫ σ i = 𝟙 ([n] :
   rcases i with ⟨i, _⟩
   rcases j with ⟨j, _⟩
   dsimp [δ, σ, Fin.succAbove, Fin.predAbove]
-  simp only [Fin.mk_lt_mk]
   split_ifs <;> simp <;> simp at * <;> linarith
 #align simplex_category.δ_comp_σ_succ SimplexCategory.δ_comp_σ_succ
 
diff --git a/Mathlib/Analysis/Convex/Between.lean b/Mathlib/Analysis/Convex/Between.lean
index 00e26e73b4711..6768fbf5083f9 100644
--- a/Mathlib/Analysis/Convex/Between.lean
+++ b/Mathlib/Analysis/Convex/Between.lean
@@ -70,8 +70,10 @@ theorem right_mem_affineSegment (x y : P) : y ∈ affineSegment R x y :=
 theorem affineSegment_same (x : P) : affineSegment R x x = {x} := by
   -- porting note: added as this doesn't do anything in `simp_rw` any more
   rw [affineSegment]
+  -- Note: when adding "simp made no progress" in lean4#2336,
+  -- had to change `lineMap_same` to `lineMap_same _`. Not sure why?
   -- porting note: added `_ _` and `Function.const`
-  simp_rw [lineMap_same, AffineMap.coe_const _ _, Function.const,
+  simp_rw [lineMap_same _, AffineMap.coe_const _ _, Function.const,
     (Set.nonempty_Icc.mpr zero_le_one).image_const]
 #align affine_segment_same affineSegment_same
 
diff --git a/Mathlib/Analysis/Convex/Side.lean b/Mathlib/Analysis/Convex/Side.lean
index 646076298811e..21e1c4e2c7a00 100644
--- a/Mathlib/Analysis/Convex/Side.lean
+++ b/Mathlib/Analysis/Convex/Side.lean
@@ -398,8 +398,11 @@ theorem _root_.Wbtw.wOppSide₁₃ {s : AffineSubspace R P} {x y z : P} (h : Wbt
   rcases ht0.lt_or_eq with (ht0' | rfl); swap
   · rw [lineMap_apply_zero]; simp
   refine' Or.inr (Or.inr ⟨1 - t, t, sub_pos.2 ht1', ht0', _⟩)
-  simp_rw [lineMap_apply, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, ← neg_vsub_eq_vsub_rev z x,
-    vsub_self, zero_sub, ← neg_one_smul R (z -ᵥ x), ← add_smul, smul_neg, ← neg_smul, smul_smul]
+  -- TODO: after lean4#2336 "simp made no progress feature"
+  -- had to add `_` to several lemmas here. Not sure why!
+  simp_rw [lineMap_apply _, vadd_vsub_assoc _, vsub_vadd_eq_vsub_sub _,
+    ← neg_vsub_eq_vsub_rev z x, vsub_self _, zero_sub, ← neg_one_smul R (z -ᵥ x),
+    ← add_smul, smul_neg, ← neg_smul, smul_smul]
   ring_nf
 #align wbtw.w_opp_side₁₃ Wbtw.wOppSide₁₃
 
diff --git a/Mathlib/Data/Finsupp/Defs.lean b/Mathlib/Data/Finsupp/Defs.lean
index a739d1f09c3d2..632f60169c01d 100644
--- a/Mathlib/Data/Finsupp/Defs.lean
+++ b/Mathlib/Data/Finsupp/Defs.lean
@@ -544,7 +544,7 @@ def update (f : α →₀ M) (a : α) (b : M) : α →₀ M where
     classical
     simp [Function.update, Ne.def]
     split_ifs with hb ha ha <;>
-    simp only [*, not_false_iff, iff_true, not_true, iff_false]
+      try simp only [*, not_false_iff, iff_true, not_true, iff_false]
     · rw [Finset.mem_erase]
       simp
     · rw [Finset.mem_erase]
diff --git a/Mathlib/Data/Multiset/Functor.lean b/Mathlib/Data/Multiset/Functor.lean
index faa9db9959e24..7b98d000e794c 100644
--- a/Mathlib/Data/Multiset/Functor.lean
+++ b/Mathlib/Data/Multiset/Functor.lean
@@ -27,7 +27,7 @@ theorem fmap_def {α' β'} {s : Multiset α'} (f : α' → β') : f <$> s = s.ma
   rfl
 #align multiset.fmap_def Multiset.fmap_def
 
-instance : LawfulFunctor Multiset := by refine' { .. } <;> intros <;> simp; rfl
+instance : LawfulFunctor Multiset := by refine' { .. } <;> intros <;> (try simp); rfl
 
 open LawfulTraversable CommApplicative
 
diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index 3f006f9f711b6..15b15ab136c4b 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -897,7 +897,7 @@ theorem bitwise'_to_nat {f : Num → Num → Num} {g : Bool → Bool → Bool} (
   -- Porting note: `change .. with ..` is now `simp only [show .. = .. from rfl]`.
   intros m n
   cases' m with m <;> cases' n with n <;>
-      simp only [show zero = 0 from rfl, show ((0 : Num) : ℕ) = 0 from rfl]
+      try simp only [show zero = 0 from rfl, show ((0 : Num) : ℕ) = 0 from rfl]
   · rw [f00, Nat.bitwise'_zero]; rfl
   · unfold Nat.bitwise'
     rw [f0n, Nat.binaryRec_zero]
diff --git a/Mathlib/Data/UnionFind.lean b/Mathlib/Data/UnionFind.lean
index b23da938ee5eb..2cc517db1e155 100644
--- a/Mathlib/Data/UnionFind.lean
+++ b/Mathlib/Data/UnionFind.lean
@@ -47,8 +47,8 @@ def setParentBump {n} (m : UFModel n) (x y : Fin n)
   rank i := if y.1 = i ∧ m.rank x = m.rank y then m.rank y + 1 else m.rank i
   rank_lt i := by
     simp; split <;>
-      (rename_i h₁; simp [h₁]; split <;> rename_i h₂ <;>
-        (intro h; simp [h] at h₂ <;> simp [h₁, h₂, h]))
+      (rename_i h₁; (try simp [h₁]); split <;> rename_i h₂ <;>
+        (intro h; try simp [h] at h₂ <;> simp [h₁, h₂, h]))
     · simp [← h₁]; split <;> rename_i h₃
       · rw [h₃]; apply Nat.lt_succ_self
       · exact lt_of_le_of_ne H h₃
diff --git a/Mathlib/Data/Vector/Basic.lean b/Mathlib/Data/Vector/Basic.lean
index c418f586b4867..16eb67b3a8e3d 100644
--- a/Mathlib/Data/Vector/Basic.lean
+++ b/Mathlib/Data/Vector/Basic.lean
@@ -636,7 +636,7 @@ theorem get_set_of_ne {v : Vector α n} {i j : Fin n} (h : i ≠ j) (a : α) :
 
 theorem get_set_eq_if {v : Vector α n} {i j : Fin n} (a : α) :
     (v.set i a).get j = if i = j then a else v.get j := by
-  split_ifs <;> try simp [*] <;> try rw [get_set_of_ne]; assumption
+  split_ifs <;> (try simp [*]); rwa [get_set_of_ne]
 #align vector.nth_update_nth_eq_if Vector.get_set_eq_if
 
 @[to_additive]
diff --git a/Mathlib/FieldTheory/RatFunc.lean b/Mathlib/FieldTheory/RatFunc.lean
index b68f1ffde803e..51d865ce742e3 100644
--- a/Mathlib/FieldTheory/RatFunc.lean
+++ b/Mathlib/FieldTheory/RatFunc.lean
@@ -517,7 +517,7 @@ section TacticInterlude
 -- porting note: reimplemented the `frac_tac` and `smul_tac` as close to the originals as I could
 /-- Solve equations for `RatFunc K` by working in `FractionRing K[X]`. -/
 macro "frac_tac" : tactic => `(tactic| repeat (rintro (⟨⟩ : RatFunc _)) <;>
-  simp only [← ofFractionRing_zero, ← ofFractionRing_add, ← ofFractionRing_sub,
+  try simp only [← ofFractionRing_zero, ← ofFractionRing_add, ← ofFractionRing_sub,
     ← ofFractionRing_neg, ← ofFractionRing_one, ← ofFractionRing_mul, ← ofFractionRing_div,
     ← ofFractionRing_inv,
     add_assoc, zero_add, add_zero, mul_assoc, mul_zero, mul_one, mul_add, inv_zero,
diff --git a/Mathlib/Init/Algebra/Order.lean b/Mathlib/Init/Algebra/Order.lean
index ec9b0580e0e15..d7f20d7f99f65 100644
--- a/Mathlib/Init/Algebra/Order.lean
+++ b/Mathlib/Init/Algebra/Order.lean
@@ -431,7 +431,7 @@ theorem compare_gt_iff_gt {a b : α} : (compare a b = .gt) ↔ a > b := by
 
 theorem compare_eq_iff_eq {a b : α} : (compare a b = .eq) ↔ a = b := by
   rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
-  split_ifs <;> simp only []
+  split_ifs <;> try simp only []
   case _ h   => exact false_iff_iff.2 <| ne_iff_lt_or_gt.2 <| .inl h
   case _ _ h => exact true_iff_iff.2 h
   case _ _ h => exact false_iff_iff.2 h
diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean
index 69112d6134c58..428db1ca88d4c 100644
--- a/Mathlib/Logic/Equiv/Basic.lean
+++ b/Mathlib/Logic/Equiv/Basic.lean
@@ -1583,7 +1583,7 @@ theorem swapCore_swapCore (r a b : α) : swapCore a b (swapCore a b r) = r := by
 theorem swapCore_comm (r a b : α) : swapCore a b r = swapCore b a r := by
   unfold swapCore
   -- Porting note: whatever solution works for `swapCore_swapCore` will work here too.
-  split_ifs with h₁ h₂ h₃ <;> simp
+  split_ifs with h₁ h₂ h₃ <;> try simp
   · cases h₁; cases h₂; rfl
 #align equiv.swap_core_comm Equiv.swapCore_comm
 
diff --git a/Mathlib/Logic/Equiv/LocalEquiv.lean b/Mathlib/Logic/Equiv/LocalEquiv.lean
index 7fe39f175f56b..e4fbfb9bbae98 100644
--- a/Mathlib/Logic/Equiv/LocalEquiv.lean
+++ b/Mathlib/Logic/Equiv/LocalEquiv.lean
@@ -95,11 +95,13 @@ elab (name := mfldSetTac) "mfld_set_tac" : tactic => withMainContext do
       apply Set.ext; intro my_y
       constructor <;>
         · intro h_my_y
-          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))))
+          try simp only [*, mfld_simps] at h_my_y
+          try simp only [*, mfld_simps])))
   | (``Subset, #[_ty, _inst, _e₁, _e₂]) =>
     evalTactic (← `(tactic| (
       intro my_y h_my_y
-      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))))
+      try simp only [*, mfld_simps] at h_my_y
+      try simp only [*, mfld_simps])))
   | _ => throwError "goal should be an equality or an inclusion"
 
 attribute [mfld_simps] and_true eq_self_iff_true Function.comp_apply
diff --git a/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean b/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean
index e091f67e9e9c1..e86b6d162ca8a 100644
--- a/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean
+++ b/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean
@@ -62,7 +62,7 @@ theorem liouvilleWith_one (x : ℝ) : LiouvilleWith 1 x := by
   rw [abs_sub_comm, abs_of_pos (sub_pos.2 this), rpow_one, sub_lt_iff_lt_add',
     add_div_eq_mul_add_div _ _ hn'.ne', div_lt_div_right hn']
   convert add_lt_add_right ((Int.floor_le (x * n)).trans_lt (lt_add_one _)) 1 using 1 <;>
-  push_cast <;> ring
+    (try push_cast) <;> ring
 #align liouville_with_one liouvilleWith_one
 
 namespace LiouvilleWith
diff --git a/Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean b/Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean
index b7202a9f9296b..f35dc6ad7bfeb 100644
--- a/Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean
+++ b/Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean
@@ -286,16 +286,19 @@ def bicategory_coherence (g : MVarId) : TermElabM Unit := g.withContext do
 Use `pure_coherence` instead, which is a frontend to this one. -/
 elab "bicategory_coherence" : tactic => do bicategory_coherence (← getMainGoal)
 
+open Lean.Parser.Tactic
+
 /--
 Simp lemmas for rewriting a 2-morphism into a normal form.
 -/
-syntax (name := whisker_simps) "whisker_simps" : tactic
+syntax (name := whisker_simps) "whisker_simps" (config)? : tactic
 
 @[inherit_doc whisker_simps]
 elab_rules : tactic
-| `(tactic| whisker_simps) => do
+| `(tactic| whisker_simps $[$cfg]?) => do
   evalTactic (← `(tactic|
-    simp only [Category.assoc, Bicategory.comp_whiskerLeft, Bicategory.id_whiskerLeft,
+    simp $[$cfg]? only [Category.assoc,
+      Bicategory.comp_whiskerLeft, Bicategory.id_whiskerLeft,
       Bicategory.whiskerRight_comp, Bicategory.whiskerRight_id,
       Bicategory.whiskerLeft_comp, Bicategory.whiskerLeft_id,
       Bicategory.comp_whiskerRight, Bicategory.id_whiskerRight, Bicategory.whisker_assoc]
diff --git a/Mathlib/Tactic/CategoryTheory/Coherence.lean b/Mathlib/Tactic/CategoryTheory/Coherence.lean
index 6c9c464be855f..26d0086eec967 100644
--- a/Mathlib/Tactic/CategoryTheory/Coherence.lean
+++ b/Mathlib/Tactic/CategoryTheory/Coherence.lean
@@ -287,9 +287,11 @@ elab (name := liftable_prefixes) "liftable_prefixes" : tactic => do
   withOptions (fun opts => synthInstance.maxSize.set opts
     (max 256 (synthInstance.maxSize.get opts))) do
   evalTactic (← `(tactic|
-    simp only [monoidalComp, Category.assoc, MonoidalCoherence.hom] <;>
+    (simp (config := {failIfUnchanged := false}) only
+      [monoidalComp, Category.assoc, MonoidalCoherence.hom]) <;>
     (apply (cancel_epi (𝟙 _)).1 <;> try infer_instance) <;>
-    simp only [assoc_liftHom, Mathlib.Tactic.BicategoryCoherence.assoc_liftHom₂]))
+    (simp (config := {failIfUnchanged := false}) only
+      [assoc_liftHom, Mathlib.Tactic.BicategoryCoherence.assoc_liftHom₂])))
 
 lemma insert_id_lhs {C : Type*} [Category C] {X Y : C} (f g : X ⟶ Y) (w : f ≫ 𝟙 _ = g) :
     f = g := by
@@ -364,8 +366,7 @@ syntax (name := coherence) "coherence" : tactic
 elab_rules : tactic
 | `(tactic| coherence) => do
   evalTactic (← `(tactic|
-    simp only [bicategoricalComp];
-    simp only [monoidalComp];
-    try whisker_simps
+    (simp (config := {failIfUnchanged := false}) only [bicategoricalComp, monoidalComp]);
+    whisker_simps (config := {failIfUnchanged := false})
     ))
   coherence_loop
diff --git a/Mathlib/Tactic/DeriveTraversable.lean b/Mathlib/Tactic/DeriveTraversable.lean
index c20cdc5e343a3..88f5712fd8693 100644
--- a/Mathlib/Tactic/DeriveTraversable.lean
+++ b/Mathlib/Tactic/DeriveTraversable.lean
@@ -463,7 +463,7 @@ def deriveLawfulTraversable (m : MVarId) : TermElabM Unit := do
     if b then
       let hs ← getPropHyps
       s ← hs.foldlM (fun s f => f.getDecl >>= fun d => s.add (.fvar f) #[] d.toExpr) s
-    return { simpTheorems := #[s] }
+    return { config := { failIfUnchanged := false }, simpTheorems := #[s] }
   let .app (.app (.const ``LawfulTraversable _) F) _ ← m.getType >>= instantiateMVars | failure
   let some n := F.getAppFn.constName? | failure
   let [mit, mct, mtmi, mn] ← m.applyConst ``LawfulTraversable.mk | failure
diff --git a/Mathlib/Tactic/Group.lean b/Mathlib/Tactic/Group.lean
index 39e6332d14a76..5c9c750e39b5d 100644
--- a/Mathlib/Tactic/Group.lean
+++ b/Mathlib/Tactic/Group.lean
@@ -56,7 +56,7 @@ syntax (name := aux_group₁) "aux_group₁" (location)? : tactic
 
 macro_rules
 | `(tactic| aux_group₁ $[at $location]?) =>
-  `(tactic| simp (config := {decide := false}) only
+  `(tactic| simp (config := {decide := false, failIfUnchanged := false}) only
     [commutatorElement_def, mul_one, one_mul,
       ←zpow_neg_one, ←zpow_ofNat, ←zpow_mul,
       Int.ofNat_add, Int.ofNat_mul,
diff --git a/Mathlib/Tactic/Lift.lean b/Mathlib/Tactic/Lift.lean
index 11a010bb384b6..5980adbac0eda 100644
--- a/Mathlib/Tactic/Lift.lean
+++ b/Mathlib/Tactic/Lift.lean
@@ -154,8 +154,9 @@ def Lift.main (e t : TSyntax `term) (hUsing : Option (TSyntax `term))
       if decl.userName != newEqName then
         let declIdent := mkIdent decl.userName
         -- The line below fails if $declIdent is there only once.
-        evalTactic (← `(tactic| simp only [← $newEqIdent] at $declIdent $declIdent))
-    evalTactic (← `(tactic| simp only [← $newEqIdent]))
+        evalTactic (← `(tactic| simp (config := {failIfUnchanged := false})
+          only [← $newEqIdent] at $declIdent $declIdent))
+    evalTactic (← `(tactic| simp (config := {failIfUnchanged := false}) only [← $newEqIdent]))
   -- Clear the temporary hypothesis used for the new variable name if applicable
   if isNewVar && !isNewEq then
     evalTactic (← `(tactic| clear $newEqIdent))
diff --git a/Mathlib/Tactic/NoncommRing.lean b/Mathlib/Tactic/NoncommRing.lean
index 4d75bc4bf3ecc..4495473685373 100644
--- a/Mathlib/Tactic/NoncommRing.lean
+++ b/Mathlib/Tactic/NoncommRing.lean
@@ -40,19 +40,21 @@ by noncomm_ring
 syntax (name := noncomm_ring) "noncomm_ring" : tactic
 macro_rules
   | `(tactic| noncomm_ring) => `(tactic| (
-      simp only [ -- Expand everything out.
-                  add_mul, mul_add, sub_eq_add_neg,
-                  -- Right associate all products.
-                  mul_assoc,
-                  -- Expand powers to numerals.
-                  pow_one, pow_zero, pow_succ,
-                  -- Replace multiplication by numerals with `zsmul`.
-                  one_mul, mul_one, zero_mul, mul_zero,
-                  nat_lit_mul_eq_nsmul, mul_nat_lit_eq_nsmul,
-                  -- Pull `zsmul n` out the front so `abel` can see them.
-                  mul_smul_comm, smul_mul_assoc,
-                  -- Pull out negations.
-                  neg_mul, mul_neg ] <;>
+      (first | simp only [
+          -- Expand everything out.
+          add_mul, mul_add, sub_eq_add_neg,
+          -- Right associate all products.
+          mul_assoc,
+          -- Expand powers to numerals.
+          pow_one, pow_zero, pow_succ,
+          -- Replace multiplication by numerals with `zsmul`.
+          one_mul, mul_one, zero_mul, mul_zero,
+          nat_lit_mul_eq_nsmul, mul_nat_lit_eq_nsmul,
+          -- Pull `zsmul n` out the front so `abel` can see them.
+          mul_smul_comm, smul_mul_assoc,
+          -- Pull out negations.
+          neg_mul, mul_neg] |
+        fail "`noncomm_ring` simp lemmas don't apply; try `abel` instead") <;>
       first | abel1 | abel_nf ))
 
 end Mathlib.Tactic.NoncommRing
diff --git a/Mathlib/Tactic/NormCast/Tactic.lean b/Mathlib/Tactic/NormCast/Tactic.lean
index 718bda23fc10a..8b425a6b62b7f 100644
--- a/Mathlib/Tactic/NormCast/Tactic.lean
+++ b/Mathlib/Tactic/NormCast/Tactic.lean
@@ -260,6 +260,7 @@ syntax (name := pushCast) "push_cast " (config)? (discharger)? (&" only")?
 @[tactic pushCast] def evalPushCast : Tactic := fun stx ↦ do
   let { ctx, dischargeWrapper, .. } ← withMainContext do
     mkSimpContext' (← pushCastExt.getTheorems) stx (eraseLocal := false)
+  let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
   dischargeWrapper.with fun discharge? ↦
     discard <| simpLocation ctx discharge? (expandOptLocation stx[5])
 
diff --git a/Mathlib/Tactic/SimpRw.lean b/Mathlib/Tactic/SimpRw.lean
index fc839024dca63..5e359dbdae83f 100644
--- a/Mathlib/Tactic/SimpRw.lean
+++ b/Mathlib/Tactic/SimpRw.lean
@@ -54,7 +54,7 @@ by simp_rw [h1, h2]
 ```
 -/
 elab s:"simp_rw " rws:rwRuleSeq g:(location)? : tactic => do
-  evalTactic (← `(tactic| simp%$s only $g ?))
+  evalTactic (← `(tactic| simp%$s (config := { failIfUnchanged := false }) only $g ?))
   withSimpRWRulesSeq s rws fun symm term => do
     evalTactic (← match term with
     | `(term| $e:term) =>
diff --git a/Mathlib/Tactic/SplitIfs.lean b/Mathlib/Tactic/SplitIfs.lean
index c719391b94917..931c54c6b1fcc 100644
--- a/Mathlib/Tactic/SplitIfs.lean
+++ b/Mathlib/Tactic/SplitIfs.lean
@@ -64,6 +64,7 @@ private def discharge? (e : Expr) : SimpM (Option Expr) := do
 -/
 private def reduceIfsAt (loc : Location) : TacticM Unit := do
   let ctx ← SplitIf.getSimpContext
+  let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
   let _ ← simpLocation ctx discharge? loc
   pure ()
 
diff --git a/Mathlib/Topology/MetricSpace/Infsep.lean b/Mathlib/Topology/MetricSpace/Infsep.lean
index 90f5032ac4ed9..11e07b5a2ed53 100644
--- a/Mathlib/Topology/MetricSpace/Infsep.lean
+++ b/Mathlib/Topology/MetricSpace/Infsep.lean
@@ -148,7 +148,8 @@ theorem einfsep_insert_le : (insert x s).einfsep ≤ ⨅ (y ∈ s) (_ : x ≠ y)
 
 theorem le_einfsep_pair : edist x y ⊓ edist y x ≤ ({x, y} : Set α).einfsep := by
   simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff, mem_singleton_iff]
-  rintro a (rfl | rfl) b (rfl | rfl) hab <;> simp only [le_refl, true_or, or_true] <;> contradiction
+  rintro a (rfl | rfl) b (rfl | rfl) hab <;> (try simp only [le_refl, true_or, or_true]) <;>
+    contradiction
 #align set.le_einfsep_pair Set.le_einfsep_pair
 
 theorem einfsep_pair_le_left (hxy : x ≠ y) : ({x, y} : Set α).einfsep ≤ edist x y :=
diff --git a/lake-manifest.json b/lake-manifest.json
index 5f0c320319014..0ed66930b0954 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,33 +1,43 @@
-{"version": 4,
+{"version": 5,
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",
     "subDir?": null,
     "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
+    "opts": {},
     "name": "proofwidgets",
-    "inputRev?": "v0.0.13"}},
+    "inputRev?": "v0.0.13",
+    "inherited": false}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
     "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+    "opts": {},
     "name": "Cli",
-    "inputRev?": "nightly"}},
+    "inputRev?": "nightly",
+    "inherited": false}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
     "rev": "81cc13c524a68d0072561dbac276cd61b65872a6",
+    "opts": {},
     "name": "Qq",
-    "inputRev?": "master"}},
+    "inputRev?": "master",
+    "inherited": false}},
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "d13a9666e6f430b940ef8d092f1219e964b52a09",
+    "rev": "086c98bb129ca856381d4414dc0afd6e3e4ae2ef",
+    "opts": {},
     "name": "aesop",
-    "inputRev?": "master"}},
+    "inputRev?": "master",
+    "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "8b864260672b21d964d79ecb2376e01d0eab9f5b",
+    "rev": "49353fa54abdac7221fe27f7b57a6ed9ff559d5c",
+    "opts": {},
     "name": "std",
-    "inputRev?": "main"}}]}
+    "inputRev?": "main",
+    "inherited": false}}]}
diff --git a/lean-toolchain b/lean-toolchain
index 1ea4b7cbf4d94..ea806c142f3ec 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-08-15
+leanprover/lean4:nightly-2023-08-17
diff --git a/test/NoncommRing.lean b/test/NoncommRing.lean
index bb8c54080bee9..90f544eec2466 100644
--- a/test/NoncommRing.lean
+++ b/test/NoncommRing.lean
@@ -57,5 +57,10 @@ example : ⁅a, b ⚬ c⁆ = ⁅a, b⁆ ⚬ c + b ⚬ ⁅a, c⁆ := by noncomm_r
 example : ⁅a ⚬ b, c⁆ = a ⚬ ⁅b, c⁆ + ⁅a, c⁆ ⚬ b := by noncomm_ring
 example : (a ⚬ b) ⚬ c - a ⚬ (b ⚬ c) = -⁅⁅a, b⁆, c⁆ + ⁅a, ⁅b, c⁆⁆ := by noncomm_ring
 
-example : a + -b = -b + a := by noncomm_ring
+example : a + -b = -b + a := by
+  -- This should print "`noncomm_ring` simp lemmas don't apply; try `abel` instead"
+  -- but I don't know how to test for this:
+  -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60fail.60.20that.20doesn't.20print.20the.20goal.3F/near/382280010
+  fail_if_success noncomm_ring
+  abel
 example : a ^ 50 * a ^ 37 = a ^ 23 * a ^ 64 := by noncomm_ring
diff --git a/test/says.lean b/test/says.lean
index f60d86c39c29b..cd1da022afa00 100644
--- a/test/says.lean
+++ b/test/says.lean
@@ -65,10 +65,9 @@ example : True := by
   trivial
 
 set_option says.verify true in
-example : Nat := by
-  simp? says simp only
+example (x y : List α) : (x ++ y).length = x.length + y.length := by
+  simp? says simp only [List.length_append]
   -- This is a comment to test that `says` ignores following comments.
-  exact 0
 
 set_option says.no_verify_in_CI true in
 example : True := by