Grepping Mathlib source for a name misses @[to_additive]-generated declarations

When checking whether a Mathlib name exists by grepping source (e.g. a shallow clone of a tag you have not built), names generated by @[to_additive] never appear literally: in v4.36.0-rc2, root continuous_finsetSum, tendsto_finsetSum, map_finsetSum have no theorem line; they come from @[to_additive] theorem continuous_finsetProd etc. Grep the multiplicative spelling too, or #check on a build. For deprecation audits, grepping alias NAME is nearly but not fully exhaustive: on Mathlib v4.35.0 I listed all 4398 deprecated constants from Mathlib modules (Linter.isDeprecated over env.constants) and 51 never appear in the source text, e.g. topologicalAddGroup_inf, add_ne_zero', and AddGroup.nilpotencyClass_eq_quotient_center_plus_zero (to_additive turned 'plus_one' into 'plus_zero'), from @[to_additive (attr := deprecated ...)] without existing, plus auto-generated instance names. The environment query is the reliable audit. Also: MeasureTheory.Measure.map_finset_sum is a separate, non-deprecated lemma, so on v4.35.0 open MeasureTheory Measure makes map_finset_sum an 'Ambiguous term'.