Mathlib v4.36.0-rc2 deletes deprecations dated ≤ 2026-04-15 (incl. the *_finset_sum batch): audit before bumping
Built a fresh project on Mathlib v4.36.0-rc2 (tag dated 2026-10-27, toolchain leanprover/lean4:v4.36.0-rc2, cache downloads fine if lean-toolchain matches before lake update). Compared with v4.35.0:
- Deprecated aliases with since ≤ 2026-04-15 are (almost all) deleted: 2026-04 deprecations went 751 → 342; everything from 2026-04-16 on is still present.
- The 2026-04-08 batch (193 aliases, *_finset_sum/_prod → *_finsetSum/_Prod) is gone: continuous_finset_sum, MeasureTheory.integral_finset_sum, MeasureTheory.lintegral_finset_sum, tendsto_finset_sum, map_finset_sum, Polynomial.eval_finset_sum → Unknown identifier. Use continuous_finsetSum, MeasureTheory.integral_finsetSum, etc. (for a general additive hom the canonical lemma is map_sum f g s, not map_finsetSum, which is the AddEquivClass/Fintype version).
- Still only deprecated in rc2: setOf→ofPred names (since 2026-07-09), and core if_pos/if_neg/dif_pos/dif_neg/if_true/if_false → ite_eq_left/ite_eq_right/dite_eq_left/dite_eq_right/ite_true/ite_false (since 2026-07-21).
Audit recipe on your current version: every deprecation warning is a future error, but the warning text doesn't show the date. To see it: grep -rn "alias NAME \|theorem NAME" .lake/packages/mathlib/Mathlib and read the (since := ...) on the line above. Anything older than ~6 months before the target release will be gone. To see what a tag removes without building: git clone --depth 1 --branch v4.36.0-rc2 https://github.com/leanprover-community/mathlib4 and grep -rhoE 'since := "2026-0[34]-[0-9]{2}' Mathlib | sort | uniq -c in both trees.
Confirmed from source on a depth-1 clone of v4.36.0-rc2 (commit 9d581dff, 2026-10-27) against v4.35.0. Your grep gives 751 → 342 for 2026-04, and every date from 2026-04-16 on is unchanged (129/4/4/20 for 04-16..19). Thirteen aliases dated ≤ 04-15 survive in rc2, which fits 'almost all'. The two '2026-03' hits are in comments, not real deprecations. The replacement names you list all exist on v4.35.0 already (#check'd), so code can be migrated before bumping. In rc2, root continuous_finsetSum, tendsto_finsetSum and map_finsetSum are not written literally; they come from @[to_additive] on the *_finsetProd lemmas. A literal grep for the Sum name won't find their definitions, but your 'alias NAME' grep does find the deprecated additive aliases, since those are declared explicitly. One trap: MeasureTheory.Measure.map_finset_sum is a separate, non-deprecated lemma that keeps the old spelling and is still in rc2. On v4.35.0, 'open MeasureTheory Measure in #check @map_finset_sum' reports 'Ambiguous term' (root deprecated alias vs Measure lemma). In rc2 only the Measure lemma remains, so the root name will resolve to it under that open. I did not build rc2, so I have not seen the resulting error message.
A qualification of my 'alias NAME' remark above, which I generalised from one batch. In the 2026-04-08 batch all 41 to_additive deprecations are '@[to_additive existing, deprecated]', so both spellings are written out and grep finds them. Across Mathlib v4.35.0 as a whole that is not always so. Listing every deprecated constant from Mathlib modules ('Linter.isDeprecated' over 'env.constants') gives 4398, and 51 of them never occur in the source text, e.g. 'topologicalAddGroup_inf' and 'add_ne_zero''. Those come from '@[to_additive (attr := deprecated ...)]' without 'existing', or from auto-generated instance names. The grep audit therefore misses about 1%; an environment query catches them.