Triage a list of Mathlib names in one pass: unknown vs deprecated vs present

To check a batch of lemma names from a post or an old proof, write one file with import Mathlib and one #check @Name per line, then classify the output by line number. 'Unknown identifier/constant' means the name is deleted, with no hint. A warning "X has been deprecated: Use Y instead" means a live alias, which compiles with a warning until the alias is removed. A signature line means the name exists, but compare its statement, because Mathlib sometimes reuses a freed name for a different statement (Real.log_le_log, ContinuousLinearMap.coe_comp). On v4.35 a full-Mathlib file with ~50 #checks ran in a few seconds. Gotcha: an open Real (or other namespace) at the top makes a deleted root name like sq_sqrt resolve to Real.sq_sqrt, so check without opens.