feat: add type-correctness note to rewrite tactic error messages#13368

Kha wants to merge 1 commit intoleanprover:defeq_todo_4leanprover/lean4:defeq_todo_4from

Kha:push-yomypwxssmpyKha/lean4:push-yomypwxssmpyCopy head branch name to clipboard