[Bug] [Lean] Use of hint and sorry marks input area as correct

[pimotte]

Followup issue to #313, mentioned in #327

The use of hint or sorry should not mark the input area as correct (i.e. mark it green).

Acceptance criteria:

• Any sorries should disqualify a proof from being green.
• help is only allowed to mark the proof green if the suggestion actually makes the proof correct, but also making use of help a disqualification for a correct proof is fine.

[DikieDick]

FYI: help is the Verbose tactic, hint is mathlib.

[pimotte]

@GitLuckier I have modified the issue to be about help, rather than hint, because help is likely to be used a lot by students

[GitLuckier]

I have opened a pull request #334 that uses string matching on the diagnostic messages. This should catch all instances of sorry and should be robust enough. However, I looked through the lean4 codebase and in theory we should be able to use leantags for this. These show directly whether a proof is actually completed or not (if the proof is not complete, then that indirectly implies that no sorry's exist). However, I believe this requires major changes to the way we currently check documents.

The solution in the pull request #334 is the best what we can do right now and it works perfectly fine.