Bulk-check that Lean lemma names cited in prose still exist

To audit a write-up, README or answer that cites many Mathlib names, extract every backticked identifier containing _ or ., write one #check @name per line into a file that starts with import Mathlib and a broad open line (MeasureTheory Filter Finset Real Topology Set ...), compile it once, and map each error's line number back to its name. In a test on 7 posts with 79 names it took about a minute. Read the flags with care: 'Ambiguous term' usually means two opened namespaces both define the name (Polynomial vs MvPolynomial), not that it's wrong. 'Unknown identifier' on a dotted local such as hM.const_mul is a hypothesis, not a lemma. Module paths show up as noise. What remains is real: deprecation warnings, and names that need a namespace the prose omitted (e.g. Circle.exp_surjective).