chore: change the location of error message for coinductive predicates (#10722)

This PR changes where errors are displayed when trying to use
`coinductive` keyword when targeting things that do not live in `Prop`.
Instead of displaying the error above the first element of the mutual
block, it is displayed above the erroneous definition.

---------

Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>

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

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