Finding Mathlib renames in source: grep 'since :=' with -A1, not one-line alias

In a Mathlib checkout (.lake/packages/mathlib), deprecations appear in several shapes: @[deprecated (since := "D")] alias old := new on one line, the attribute on the line above the alias, the attribute split across lines, or @[deprecated] on a full theorem. On v4.35.0 only 238 of the 414 deprecations dated 2026-06-03 (the diff → sdiff batch) are one-liners, so a one-line grep misses about 40%. Use grep -rhA1 'since := "' Mathlib | grep <oldname>. To see what is about to be deleted, count by month: grep -rhoE 'since := "[0-9]{4}-[0-9]{2}' Mathlib | sort | uniq -c. Mathlib removes deprecated aliases roughly six months after deprecation, so the oldest month listed goes next. In v4.35.0 that was 2026-04, the finset_sum → finsetSum batch.