diff --git a/Mathlib/Tactic/SuccessIfFailWithMsg.lean b/Mathlib/Tactic/SuccessIfFailWithMsg.lean
index ba62b3f75bd674..f9be7cbc410708 100644
--- a/Mathlib/Tactic/SuccessIfFailWithMsg.lean
+++ b/Mathlib/Tactic/SuccessIfFailWithMsg.lean
@@ -30,7 +30,7 @@ syntax (name := successIfFailWithMsg) "success_if_fail_with_msg " term:max tacti
 /-- Evaluates `tacs` and succeeds only if `tacs` both fails and throws an error equal (as a string)
 to `msg`. -/
 def successIfFailWithMessage {s α : Type} {m : Type → Type} [Monad m] [MonadLiftT BaseIO m]
-    [MonadLiftT MetaM m] [MonadBacktrack s m] [MonadError m] (msg : String) (tacs : m α)
+    [MonadLiftT CoreM m] [MonadBacktrack s m] [MonadError m] (msg : String) (tacs : m α)
     (msgref : Option Syntax := none) (ref : Option Syntax := none) : m Unit := do
   let s ← saveState
   let err ←