fix: cslib breakage from the mathlib rwaSuggestion linter

[Kha]

Adapts cslib to the rwaSuggestion tactic-analysis linter that came in with the
mathlib master merge. cslib builds and tests with --wfail --iofail, so the
linter's single Try this: info in
Cslib/Computability/Languages/MyhillNerode.lean is a build failure:

ℹ [3205/3211] Building Cslib.Computability.Languages.MyhillNerode
  [apply] rwa [Nat.card_congr (Equiv.ofInjective _ Quotient.out_injective).symm] at h1
Some required targets logged failures:
- Cslib.Computability.Languages.MyhillNerode

Applied the suggestion: rw … at h1; assumption becomes rwa … at h1.

Verified locally on nightly-2026-09-06: lake build --wfail --iofail,
lake test --wfail --iofail and lake lint all pass for cslib.

This is the same one-line hunk as in #48, which has since become CONFLICTING:
its other three files are mathlib4 adaptations that master has meanwhile
acquired from upstream (mathlib4 is green — build, test and lint — in
run 34027830326).
So #48 and #49 can be closed once this lands.

Not fixed here

verso — and reference-manual, verso-slides, verso-web-components skipped
behind it — remain red on the shared-subverso-build-directory problem, sixth day
running. .downstream/downstream/updater.py redirects the subverso requirement
of verso/test-projects/* to the one shared subverso/ checkout, and the nested
elan run … lake build processes that Verso.Code.External spawns then
materialize and prune subverso/.lake/build while the outer verso build reads
oleans out of it:

error: src/verso-manual/VersoManual.lean:7:0: failed to open file '…/subverso/.lake/build/lib/lean/SubVerso/Compat.olean': No such file or directory
error: … failed to load header from …/subverso/.lake/build/ir/SubVerso/Highlighting/Anchors/Check.setup.json: offset 0: unexpected end of input

That is not a source adaptation — 1106 of verso's 1114 targets built — and the
fix belongs in .downstream/ or repos.toml, which this PR does not touch.
reference-manual was skipped by CI and has not been built against
nightly-2026-09-06 by anyone, here or in CI.

[downstream-lean4]

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

Turned green:

Repo	Critical	Build	Test	Lint
cslib		✅ in 5s	✅ in 8s	✅ in 3s

Stayed red

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

Stayed green

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 7s	✅ in 4s	⏭️
batteries	✅	✅ in 4s	✅ in 4s	✅ in 2s
import-graph	✅	✅ in 2s	✅ in 4s	⏭️
lean4-cli	✅	✅ in 1s	✅ in 0s	⏭️
mathlib4	✅	✅ in 183s	✅ in 42s	✅ in 94s
plausible	✅	✅ in 1s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 3s	✅ in 1s	⏭️
quote4	✅	✅ in 2s	✅ in 1s	⏭️
BibtexQuery		✅ in 3s	⏭️	⏭️
comparator		✅ in 2s	⏭️	⏭️
doc-gen4		✅ in 9s	⏭️	⏭️
illuminate		✅ in 3s	✅ in 11s	⏭️
lean4-unicode-basic		✅ in 2s	⏭️	⏭️
lean4export		✅ in 0s	✅ in 8s	⏭️
LeanSearchClient		✅ in 1s	✅ in 0s	⏭️
leansqlite		✅ in 7s	✅ in 19s	⏭️
nerodia		✅ in 2s	✅ in 21s	⏭️
repl		✅ in 1s	✅ in 59s	⏭️
subverso		✅ in 6s	⏭️	⏭️

View run