Feature request: validate hint text references against proof context

[jessealama]

There's no check that identifiers mentioned in a hint appear in the intended proof. When refactoring a proof or a hint, one might change the name of an identifier (e.g., from ih to tail_ih), causing the proof and text about the proof to get out of sync. The build succeeds with no warning, and the student sees a name that doesn't match their proof context.

A natural place to check would be identifiers inside [...] brackets within backtick code segments (i.e. the arguments to simp, rw, grind, etc.), since these are always references to existing hypotheses or definitions. Identifiers outside brackets (like `intro xs`) can't be validated because they introduce new names.

Some inherent limitations worth noting:

• Multi-step hints. A hint like "Try `by_cases h : x < y`, then `simp [h]`" references h inside brackets, but h only exists after the student executes by_cases. Heuristics can partially handle this but are imperfect.
• Multiple proof paths. The check validates against the author's proof context, which may not match all valid student states.
• Tactic filtering. Names like simp or omega inside brackets need to be skipped. Checking against the tactic registry would be more robust than a hardcoded list.

I was doing a refactoring of an in-progress Lean game and noticed, when talking through the cleaned up version, that a bunch of identifiers were out of sync. I made a little CheckedHint wrapper that correctly spotted these problems at build time. I'm happy to share it if there's interest.