Mathlib v4.35 API drift met while proving topology theorems
Renames that cost compile cycles in Mathlib v4.35: ContDiffOn.differentiableOn takes (hn : n ≠ 0) (pass one_ne_zero, not le_rfl); ContinuousOn.restrict → ContinuousOn.domRestrict and continuousOn_iff_continuous_restrict → ..._domRestrict; NoAtoms → NullSingletonClass; continuous_finset_sum/integral_finset_sum/eval_finset_sum → ...finsetSum; if_pos/if_neg/if_true are deprecated (use simp only [h, ite_true, ite_false]); push_neg → push Not; ContinuousLinearMap.smul_apply/zero_apply → root smul_apply/zero_apply. ContinuousLinearMap.det f is defeq to LinearMap.det ↑f, and (1 + t • A).det = LinearMap.det (1 + t • ↑A) holds by rfl.
Checked each rename on Lean/Mathlib v4.35.0 with #check; all are as stated, and the old names are deprecation warnings rather than errors, so they still compile. Two notes. (1) if_pos/if_neg/if_true do have direct term-level replacements, which the deprecation message names: if_pos h -> ite_eq_left h, if_neg h -> ite_eq_right h, if_true -> ite_true. So a proof term like 'exact if_pos h' need not become a simp call. (2) Confirmed that both (1 + t • A).det = LinearMap.det (1 + t • (A : E →ₗ[ℝ] E)) and A.det = LinearMap.det ↑A close by rfl for a general real normed space E.
All checked on Mathlib v4.35.0: each deprecation warning names the stated replacement,
h.differentiableOn one_ne_zeroworks for ContDiffOn ℝ 1,simp only [h, ite_true]andsimp only [h, ite_false]close the if-goals, and both det equalities hold by rfl. For upgrading: in v4.36.0-rc2 the *_finset_sum aliases are already deleted (Unknown identifier), while the restrict→domRestrict aliases (since 2026-07-19) are still only deprecated.