[cjen1-msft]

The Lean packages now depend on a small subset of Mathlib, vendored in lean/mathlib-subset, instead of on Mathlib itself; a new CI workflow checks that subset against upstream Mathlib.

This is an alternative to #8702, which removes Mathlib by replacing the parts CCF uses with hand-written CCF.* modules.
It reuses #8702's proof rewrites, which cut what the proofs need from Mathlib to a few definitions, so it gets most of the same CI savings: no Mathlib clone or lake exe cache get in any package or replay job, and a much smaller import closure for lake check to re-check.
The difference is what replaces Mathlib:

	#8702	This PR
Finset, Stream'.Seq, Function.update, order lemmas	Hand-written CCF.Finset, CCF.Seq, CCF.Function, CCF.Order (565 lines)	The upstream declarations, copied with their module names (59 files, 2,595 lines)
Agreement with Mathlib	Reviewed by hand; CCF.Finset is a different representation	lean/mathlib-subset-check compares the vendored declarations with Mathlib v4.35.0
Theorem statements	Mention CCF.Finset and CCF.Seq	Unchanged
lemma declarations	276 renamed to theorem	Unchanged (Mathlib.Tactic.Lemma is vendored)
runLinter lint driver	Kept; kv and DR require Batteries for it	Removed
Using another Mathlib definition	Write a CCF version and the lemmas it needs	Copy the upstream declaration, its dependencies and imports into the subset
Lean toolchain upgrades	No Mathlib to move	Move the checker's Mathlib pin too, and copy the declarations the checker reports as changed
Extra CI	None	The Lean Mathlib Subset workflow, which runs only when the subset, the checker, the toolchain or the workflow changes

The checker requires each vendored declaration to have the same module, kind, universe parameters and type as upstream, the same value for definitions with proofs erased, and the same reducibility, instance priority and structure shape.
Theorems must have the upstream statement but may be proved differently, and only propext, Quot.sound and Classical.choice are allowed as axioms.
Metaprograms (such as notation and tactics) must match upstream in everything but their value, since they only affect elaboration and the terms they produce are checked.
Internal declarations, such as auxiliary proofs and matchers, need not exist upstream, but a definition that refers to one only matches if upstream refers to an identically named, matching declaration.
lean/mathlib-subset/README.md explains how to add a declaration and how to move to a new Mathlib version.

Discontinuities

• lean/mathlib-subset keeps upstream copyright headers and formatting, so scripts/lean-format-checks.sh skips it, and it carries Mathlib's Apache 2.0 LICENSE. The checker package is format-checked as usual.
• One upstream TODO line was dropped from a module docstring in Mathlib/Tactic/SetNotationForOrder.lean, to satisfy scripts/todo-checks.sh. Docstrings are not compared.
• runLinter is removed from kv and disaster-recovery because it needs all of Batteries. lake lint still runs Lean's builtin linters, but the Batteries and Mathlib environment linters no longer run.
• The check is a separate workflow, lean-mathlib-subset.yml, with a paths filter, like vendor-verification.yml. It is therefore not part of the Lean models and proofs gate, and cannot be a required check without blocking pull requests that do not trigger it. It does not cache Mathlib (about 7 GB), since it rarely runs.
• DisasterRecovery/Proofs/Deadlock.lean, added on main by lean: Prove deadlock freedom for consistency and recovery #8716, used aesop, which only came via Mathlib; it now uses core grind.

Testing

• The Lean Mathlib Subset workflow passes on this PR in 89s (subset lake build --wfail 4s, lake exe cache get 47s, check 8s); all 533 vendored declarations that are not internal match upstream. Locally, the check fails if abbrev PartialOrder.lift becomes a def, or if Finset.card's type is changed to mention Lean (which would otherwise be taken for a metaprogram).

• actionlint reports nothing for lean-mathlib-subset.yml and lean.yml beyond the custom runner labels it does not know.

• The Lean workflow passes on this PR (run 42668962868), as does a local replay of every package job's commands (lake check, check-imports, formatting, lake lint, replay fixtures) and the three replay jobs.

• CI job times, one run each, so indicative only (main: run 42611960081; Remove the Mathlib dependency from the Lean packages #8702: run 42501320257, attempt 2; this PR: run 42668962868):

  Job	main	Remove the Mathlib dependency from the Lean packages #8702	This PR
  Lean package (common)	216s	148s	153s
  Lean package (consistency)	234s	144s	172s
  Lean package (kv)	249s	142s	174s
  Lean package (disaster-recovery)	290s	155s	191s
  Lean package (consensus)	394s	272s	291s
  Replay native CCF consensus traces	138s	30s	37s
  Replay KV traces	107s	28s	57s
  Replay consistency traces	83s	25s	27s

  The Build, kernel and axiom check step (lake check), as build and export plus kernel and axiom check:

  Package	main	Remove the Mathlib dependency from the Lean packages #8702	This PR
  common	152s (32 + 120)	124s (24 + 100)	125s (25 + 100)
  consistency	150s (33 + 117)	109s (21 + 87)	115s (25 + 90)
  kv	154s (36 + 118)	107s (22 + 85)	119s (28 + 91)
  disaster-recovery	156s (37 + 119)	109s (22 + 87)	119s (28 + 91)
  consensus, two checks	309s (38 + 124, 30 + 117)	225s (24 + 93, 20 + 88)	232s (31 + 92, 21 + 89)

  Neither CI run of this PR hit the .lake/packages cache, which now holds only leanfmt: the first because this PR changes each package's lake-manifest.json, and the second, with the same keys, because the repository's Actions cache (about 30 GB in 50 entries) had evicted the first run's entries within 90 minutes. The jobs other than common, which skips formatting, therefore built leanfmt in the formatting step, taking 22 to 27s against 3 to 9s in the Remove the Mathlib dependency from the Lean packages #8702 run, which hit its cache; main's disaster-recovery job also missed its cache. The rest of the difference from Remove the Mathlib dependency from the Lean packages #8702 is in lake check, 1 to 12s per check, from building the vendored subset and re-checking it in the kernel. This run also includes the deadlock proofs added to consistency and disaster-recovery on main since Remove the Mathlib dependency from the Lean packages #8702's run. The replay jobs' build steps take 11, 7 and 4s against 5, 6 and 4s in Remove the Mathlib dependency from the Lean packages #8702; the KV replay job also spent 12s in Install Lean and 8s stopping containers, against 0 and 2s in Remove the Mathlib dependency from the Lean packages #8702's run and 0 and 1s in this PR's previous run.

Reviewed with sol-loop: 2 rounds with gpt-6.1-sol. Sol verdict: approved