diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean
index ffebba0a31..819ef56e72 100644
--- a/src/Lean/Elab/MutualInductive.lean
+++ b/src/Lean/Elab/MutualInductive.lean
@@ -1049,8 +1049,8 @@ private def mkInductiveDeclCore
   let view0 := views[0]!
   let isCoinductive := views.any (·.isCoinductive)
   if isCoinductive then
-    unless (←rs.allM (forallTelescopeReducing ·.type fun args body => pure body.isProp)) do
-      throwErrorAt view0.declId "`coinductive` keyword can only be used to define predicates"
+    if let some i ← rs.findIdxM? (forallTelescopeReducing ·.type fun _ body => pure !body.isProp) then
+      throwErrorAt views[i]!.declId "`coinductive` keyword can only be used to define predicates"
   let allUserLevelNames := rs[0]!.levelNames
   let isUnsafe          := view0.modifiers.isUnsafe
   let res ← withInductiveLocalDecls rs fun params indFVars => do
diff --git a/tests/lean/run/coinductive_syntax.lean b/tests/lean/run/coinductive_syntax.lean
index 8c03ca45fe..deaad49790 100644
--- a/tests/lean/run/coinductive_syntax.lean
+++ b/tests/lean/run/coinductive_syntax.lean
@@ -250,3 +250,16 @@ namespace unsafe_test
 unsafe coinductive infSeq2 (r : α → α → Prop) : α → Prop where
   | step : r a b → infSeq2 r b → infSeq2 r a
 end unsafe_test
+
+/--
+@ +4:14...20
+error: `coinductive` keyword can only be used to define predicates
+-/
+#guard_msgs (positions := true) in
+mutual
+  coinductive wrong1 : Prop where
+
+  coinductive wrong2  where
+    | zero : wrong2
+    | succ : wrong1 → wrong2
+end