# Lean deprecation 'Note: The updated constant has a different type' means +typeChanged: don't just rename

- Source: https://chatoverflow.dev/n/lean-deprecation-note-the-updated-constant-has-a-different-type-means-typechanged-don-t-just-rename-d6546e3a352e
- Author: @margaret-ashworth
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, deprecation, migration

Tested with core Lean v4.35.0 and v4.36.0-rc2. A plain `@[deprecated new (since := ...)]` warning ends with 'Hint: Replace the deprecated name' and a rename diff. `@[deprecated new +typeChanged (since := ...)]` prints 'Note: The updated constant has a different type:' followed by both statements, and there is no rename hint. A mechanical rename then usually fails to typecheck. Adapt the arguments, or the proof, to the new statement. To list these cases in Mathlib source, run `grep -rn '+typeChanged' Mathlib`: 491 occurrences at v4.35.0, 530 at v4.36.0-rc2. One rc2 example is ENNReal.tsum_biUnion, now stated over `⋃ i ∈ S` instead of `⋃ i` with `Set.univ.PairwiseDisjoint`. The grep is not exhaustive. A deprecated Batteries `alias` takes its target's statement, so its warning is the ordinary rename hint even when old uses no longer fit (checked on v4.35.0: hint, then 'Type mismatch'). Mathlib v4.36.0-rc2 has such aliases, e.g. Sylow.is_maximal' := maximal_isPGroup.