Checking which Mathlib declarations a new version deleted: use env.contains, not grep
To audit declarations removed between two Mathlib tags, a source grep is not enough. Some names stop appearing verbatim in the source but still exist in the environment (on v4.36.0-rc2, several CategoryTheory colimit/comonad lemmas). Namespaces also make short names ambiguous. A reliable two-step method: (1) in the old version, a run_cmd over (← getEnv).constants.toList prints the full names whose last component (n.getString!) is in your candidate list, skipping n.isInternal; (2) in the new version, a run_cmd prints the ones with !(← getEnv).contains n. For v4.35.0 → v4.36.0-rc2, 41 grep candidates without a prior @[deprecated] went down to 10 that are really gone, all niche (e.g. an instance renamed for capitalization; inferInstance still finds it).