fix: mathlib4 and cslib breakage from nightly-2026-09-04

[Kha]

master is red on nightly-2026-09-04
(run 33939047804):
mathlib4 fails to build, cslib and repl are red behind it, and verso fails
independently, taking verso-slides, verso-web-components and the critical
reference-manual with it. This PR fixes the mathlib4 half, so it will not by itself make
the run green.

mathlib4 — rwa no longer has one syntax with an optional location

lean4#14937 split rwa into rwa [rules], rwa [rules] at h and a low-priority
rwa [rules] <location> that is deprecated on arrival. Nothing accepts an optional location any
more, so the quotation in the brand-new Mathlib.TacticAnalysis.rwaSuggestion — which came in
with this same downstream: update repo mathlib4 — stopped parsing:

error: Mathlib/Tactic/TacticAnalysis/Declarations.lean:241:77: unexpected token '$'; expected ')'

The suggestion is now built per case: no location ⇒ rwa [rules], a single hypothesis ⇒
rwa [rules] at h, anything else (at *, at ⊢, several hypotheses) ⇒ no suggestion, since
only the deprecated legacy syntax could express those. The two existing expectations in
MathlibTest/TacticAnalysis.lean (rwa [hab] at h and rwa [h₁, ← h₂]) are unchanged; a case
for the third kind is added.

Two details worth recording. The location match has to be $h:ident, not $h:term:
locationHyp also admits ⊢, which a term antiquotation happily captures and would turn into
the unparseable rwa [rules] at ⊢. And it has to be a nested match rather than
| some \(location| …) =>— a quotation pattern underneath another constructor pattern is rejected withInvalid pattern`.

mathlib4 — two @[deprecated] aliases need +typeChanged

Unmasked once the build got past the parse error, so it is nowhere in the run's log:

warning: Mathlib/Algebra/Order/BigOperators/Group/Finset.lean:159:11: The updated constant has a different type
warning: Mathlib/Algebra/Order/BigOperators/Group/Finset.lean:160:11: The updated constant has a different type

sum_nonneg'/one_le_prod'' take ∀ i, 0 ≤ f i where their replacements take
∀ i ∈ s, 0 ≤ f i; the lean4#14600 check reports that and --wfail turns it into a failure.
Marked +typeChanged, the difference being intended. This keeps arriving in batches: mathlib
master builds on a release toolchain, so a deprecation wave landing upstream is invisible to its
own CI and only surfaces here.

cslib — the new linter is on by default, and cslib builds with --iofail

rwaSuggestion defaults to true and cslib enables linter.mathlibStandardSet, so its one
rw … at h / assumption pair in Cslib.Computability.Languages.MyhillNerode produces a
Try this: info — which --iofail turns into a build and test failure. Applied the
suggestion. Expect more of these as the linter reaches other downstream repos.

Verified

• mathlib4: lake build Mathlib Archive Counterexamples Wanted --wfail, lake test --iofail,
  lake lint.
• cslib: lake build and lake test (both --wfail --iofail), lake lint.
• repl: lake build and lake test pass unchanged — its failure was only the test/Mathlib
  build hitting the parse error.

Not fixed here

verso is red for the reason already set out in #41 and unchanged since: downstream: fixup repo verso writes the in-tree subverso into the .lake/package-overrides.json of verso's nested
test projects, which pin leanprover/lean4:v4.31.0 themselves, so building them rewrites
subverso/.lake/build and every verso module importing subverso then fails on
SubVerso/Highlighting/Highlighted.olean. The fix is a guard in
Updater.fixup_subrepo_dependencies, which is outside this PR.

Nothing else is wrong with them on this nightly: with those four override entries emptied
locally, verso, verso-web-components, verso-slides and reference-manual all build clean.
(The Verso/Parser.lean constructor-ambiguity and Conditionals.lean unused-variable messages
in the run are warnings, and verso does not build with --wfail.)

🤖 Generated with Claude Code

[downstream-lean4]

Build report for fix: cslib breakage from the new mathlib rwaSuggestion linter

Turned green:

Repo	Critical	Build	Test	Lint
mathlib4	✅	✅ in 1162s	✅ in 46s	✅ in 91s
cslib		✅ in 35s	✅ in 8s	✅ in 3s
repl		✅ in 1s	✅ in 56s	⏭️

Stayed red

Repo	Critical	Build	Test	Lint
reference-manual	✅	⏭️	⏭️	⏭️
verso		🟥 in 60s	⏭️	⏭️
verso-slides		⏭️	⏭️	⏭️
verso-web-components		⏭️	⏭️	⏭️

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	⏭️
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	⏭️
subverso		✅ in 6s	⏭️	⏭️

View run