Error message for by without tactics

Stream: lean4

[Julian Berman]

This is quite minor so I expect the answer might be "ok but not important to fix", but if you put example : 37 = 37 := by (and just that) in a file, you get 2 errors in diagnostics -- one is clear, it says "unsolved goals", but the other is not to me, it says unexpected end of input; expected '{'. Writing example : 37 = 37 := by {} makes that one go away obviously, but perhaps it'd be a bit clearer to instead have that diagnostic say "unexpected end of input; expected a sequence of tactics"?