fix: cslib breakage from the mathlib merge

[Kha]

Run 35484035829 on nightly-2026-09-17 failed in cslib only. cslib is noncritical, so the build report and GitHub both call the run successful, but the repo is red and is fixed here like any other break.

cslib

Root cause. The downstream: update repo mathlib4 merge at the head of that run brought in mathlib4#42705, which makes the element type of LE.ofMembership, Preorder.ofMembership and PartialOrder.ofSetLike implicit:

-variable (A B : Type*)
+variable (A : Type*) {B : Type*}

Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean still wrote PartialOrder.ofSetLike (Fact P) P, which now elaborates as an over-applied term (Function expected at PartialOrder.ofSetLike (Fact P)). With the PartialOrder (Fact P) instance broken, ≤ on Fact P lost its definitional unfolding to set inclusion, so the remaining 11 errors in the file — Set.mul_subset_mul applied to G ≤ K, the IsConcreteLE (Fact P) P synthesis failures, the PhaseSpace Prop failures — were all downstream of that one line.

Fix. Drop the now-implicit argument:

-instance : PartialOrder (Fact P) := PartialOrder.ofSetLike (Fact P) P
+instance : PartialOrder (Fact P) := PartialOrder.ofSetLike (Fact P)

That is the only occurrence of ofSetLike/ofMembership in cslib.

Verified locally on nightly-2026-09-17, with --wfail --iofail as repos.toml configures: lake build (3244 jobs), lake test and lake lint (batteries/runLinter) all pass. CI had stopped cslib at the build, so its test and lint phases had not run this round; both are green here.

Nothing was left unfinished: cslib was the only repo not green in that run, no repo was skipped behind it, and the whole red set is covered.

[downstream-lean4]

Build report for fix: cslib breakage from the mathlib merge

Turned green:

Repo	Critical	Build	Test	Lint
cslib		✅ in 7s	✅ in 9s	✅ in 3s

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 184s	✅ in 334s	✅ in 97s
plausible	✅	✅ in 2s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 3s	✅ in 1s	⏭️
quote4	✅	✅ in 2s	✅ in 1s	⏭️
reference-manual	✅	✅ in 73s	⏭️	⏭️
BibtexQuery		✅ in 3s	⏭️	⏭️
comparator		✅ in 2s	⏭️	⏭️
doc-gen4		✅ in 9s	⏭️	⏭️
illuminate		✅ in 4s	✅ in 11s	⏭️
lean4-unicode-basic		✅ in 2s	⏭️	⏭️
lean4export		✅ in 0s	✅ in 8s	⏭️
LeanSearchClient		✅ in 1s	✅ in 0s	⏭️
leansqlite		✅ in 7s	✅ in 20s	⏭️
nerodia		✅ in 3s	✅ in 21s	⏭️
repl		✅ in 1s	✅ in 61s	⏭️
verso		✅ in 90s	✅ in 172s	⏭️
verso-slides		✅ in 18s	✅ in 9s	⏭️
verso-web-components		✅ in 7s	⏭️	⏭️

View run