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

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.