linter.fugue.unusedHave

A have / haveI whose hypothesis the rest of the proof never touches is dead weight: it survives every refactor that made it dead, and — for an instance haveI — Lean's unusedVariables does not flag it at all.

The check reads the InfoTree. A tactic have h : T := v runs as assert + intro, leaving a continuation goal g' with h in its local context; h is used exactly when its free variable occurs in g''s final assignment. That assignment is read from the command's last-finishing tactic snapshot (every goal solved by then). Uses of h under the fun h => … the have compiles to would read as bound variables, so the continuation goal is inspected directly, not the whole proof term.

A continuation whose instantiated term still carries sorry or an unassigned metavariable is skipped: the linter could not read the finished proof there (a decreasing_by block, elaborated in its own later pass, is the usual reason), so it says nothing rather than guess "unused".