fix: mathlib4 deprecation-linter breakage from the mathlib merge

[Kha]

Fixes the red master of run 34180042869 (leanprover/lean4:nightly-2026-09-06), whose only genuinely new failure is mathlib4. The repo builds with --wfail, so both of the following are warnings that fail the build.

mathlib4

Ten dropped +typeChanged markers

downstream: update repo mathlib4 (4b1d310) resolves conflicts in favour of upstream, and upstream touched the very lines that carry the +typeChanged markers this repo has been adding since lean4#14600 — so the merge silently removed all ten of them:

file	declaration
Mathlib/Data/ENat/Monoid.lean	ENat.add_one_pos → add_pos_of_right
Mathlib/Algebra/Ring/Subsemiring/Basic.lean	closureCommSemiringOfComm → isMulCommutative_closure
Mathlib/Algebra/Ring/Subring/Basic.lean	closureCommRingOfComm → isMulCommutative_closure
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean	adjoinNonUnitalCommSemiringOfComm → isMulCommutative_adjoin
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	adjoinNonUnitalCommSemiringOfComm → isMulCommutative_adjoin
Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean	adjoinCommSemiringOfComm, adjoinCommRingOfComm → isMulCommutative_adjoin
Mathlib/Algebra/Star/Subalgebra.lean	adjoinCommSemiringOfComm, adjoinCommRingOfComm → isMulCommutative_adjoin
Mathlib/RingTheory/PowerSeries/Derivative.lean	derivativeFun → derivative

All ten are the intended kind of type change (an abbrev producing a CommSemiring/CommRing instance deprecated towards the IsMulCommutative lemma; a plain function deprecated towards a Derivation), so the markers are re-added verbatim. NonUnitalSubalgebra.lean shows the situation nicely: the sibling deprecation twelve lines further down kept its marker because upstream did not touch that line.

This will keep recurring: mathlib master builds on a release toolchain, so upstream never sees the warning that makes the marker necessary and has no reason to preserve it across a rewrite.

Eight deprecated aliases pointing at deprecated aliases

Independently, the merge brought in upstream's rename of Ideal.IsIntegral.comap_* to Ideal.IsIntegral.under_* (mathlib, since := "2026-09-03"). The older Ideal.IsIntegralClosure.* and Ideal.IntegralClosure.* aliases in Mathlib/RingTheory/Ideal/GoingUp.lean still pointed at the comap_* names, which are now themselves deprecated — the case linter.deprecated.deprecatedTarget reports:

warning: Mathlib/RingTheory/Ideal/GoingUp.lean:245:2: `Ideal.IsIntegral.comap_lt_comap` is
itself deprecated in favor of `Ideal.IsIntegral.under_lt_under`; consider deprecating
`Ideal.IsIntegralClosure.comap_le_comap` in favor of `Ideal.IsIntegral.under_lt_under` instead

Retargeted all eight at the final names, which is the linter's own suggestion. An alias has the type of its target and these are aliases of aliases, so no statement changes and no +typeChanged becomes necessary.

Verified

mathlib4 locally, with the run's artifact cache restored:

• lake build Mathlib Archive Counterexamples Wanted --wfail — 9043 jobs, no warnings
• lake test --iofail
• lake lint (batteries/runLinter Mathlib)

Not in this PR

cslib is the run's other red repo, and it was only skipped behind mathlib4. Its own failure — two instance-based deprecations in Cslib/Foundations/Relation/Basic.lean — is already fixed by #54, which still applies; both have to land for the run to go green.

[downstream-lean4]

Build report for fix: mathlib4 deprecation-linter breakage from the mathlib merge

Turned green:

Repo	Critical	Build	Test	Lint
mathlib4	✅	✅ in 322s	✅ in 46s	✅ in 91s

Stayed red

Repo	Critical	Build	Test	Lint
cslib		🟥 in 35s	⏭️	⏭️

Stayed green

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 7s	✅ in 5s	⏭️
batteries	✅	✅ in 5s	✅ in 4s	✅ in 1s
import-graph	✅	✅ in 2s	✅ in 3s	⏭️
lean4-cli	✅	✅ in 1s	✅ in 0s	⏭️
plausible	✅	✅ in 1s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 3s	✅ in 1s	⏭️
quote4	✅	✅ in 2s	✅ in 1s	⏭️
reference-manual	✅	✅ in 74s	⏭️	⏭️
BibtexQuery		✅ in 3s	⏭️	⏭️
comparator		✅ in 2s	⏭️	⏭️
doc-gen4		✅ in 8s	⏭️	⏭️
illuminate		✅ in 3s	✅ in 10s	⏭️
lean4-unicode-basic		✅ in 2s	⏭️	⏭️
lean4export		✅ in 0s	✅ in 7s	⏭️
LeanSearchClient		✅ in 1s	✅ in 0s	⏭️
leansqlite		✅ in 7s	✅ in 15s	⏭️
nerodia		✅ in 2s	✅ in 21s	⏭️
repl		✅ in 1s	✅ in 55s	⏭️
verso		✅ in 90s	✅ in 82s	⏭️
verso-slides		✅ in 58s	✅ in 6s	⏭️
verso-web-components		✅ in 34s	⏭️	⏭️

View run