mathlib bump needs manual repair: fa97836994f0 (5 files)

[CBirkbeck]

Daily bump b4384330e5b9 → fa97836994f0 (same toolchain v4.32.0-rc1 — mathlib-commit churn, not a toolchain jump) breaks 5 files across 4 projects. Exceeds quick-mechanical repair (no renamed-lemma/deprecation one-liners), so the bump was discarded — main stays green at b4384330e5b9. Needs a producer/manual pass:

1. projects/HasseWeil/HasseWeil/FormalGroup/PDeriv.lean:412 — typeclass instance stuck: ContinuousConstSMul ?m R (first/fourth args are metavariables). Needs a type annotation to pin them.
2. projects/FltRegularBernoulli/BernoulliRegular/LValueAtOne/Cosine.lean:376 — unsolved goals (case e'_5, a Tendsto … cos … goal).
3. projects/LeanModularForms/LeanModularForms/ForMathlib/GeneralizedResidueTheory/Residue.lean:325 — invalid ▸ notation: the funext hg_eq_at equality is no longer mentioned in the ContinuousAt target (rewrite the ▸ explicitly).
4. projects/LeanModularForms/LeanModularForms/ForMathlib/HungerbuhlerWasem/CrossingDataBuilder.lean:407 — ring failed (ring expressions not equal).
5. projects/PadicLFunctions/PadicLFunctions/IwasawaProof/LogDerivative.lean:1389 — typeclass instance stuck: ContinuousConstSMul ?m ℤ_[p] (same root as cleanup: golf padicLog_mul_of_norm_lt_one #1).

Likely shared root: #1 + #5 are the same ContinuousConstSMul metavariable-stuck pattern (one fix style). #2/#3/#4 are distinct proof breakages. Once repaired, the next daily bump carries them. Full-tree build_all RC=1, 5 broken files, no toolchain/cache errors.

[CBirkbeck]

The 2026-06-26 daily mathlib bump needs manual repair. Same toolchain (v4.32.0-rc1), so no toolchain jump — but the +101-commit mathlib churn (b4384330e5b9 → 11b908e5cdd941b2d54b1b2ab55d069f5d8281d4) breaks 7 files across 6 projects with a mix of non-trivial error types, beyond the unattended quick-mechanical bar. Branch discarded; main stays green on b4384330e5b9.

Full-tree build_all RC=1, 0 EMFILE (all real breakages). Broken files + first errors:

file	error(s)	likely fix
FltRegular/NumberTheory/Cyclotomic/CyclRat.lean	nthRootsFinset_eq_of_prime, mem_primitiveRoots_of_mem_nthRootsFinset, isPrimitiveRoot_of_mem_nthRootsFinset "has already been declared"	mechanical — mathlib upstreamed these; delete the local duplicates
HasseWeil/GapQfKernel.lean	5× rewrite failed: Did not find an occurrence of the pattern (L393/401/441/449/466)	a rewritten lemma changed form/name — re-point the rws
BernoulliRegular/LValueAtOne/Cosine.lean	unsolved goals (L376)	likely simp-set change; add a closing lemma/tactic
HasseWeil/FormalGroup/PDeriv.lean	typeclass instance problem is stuck (L455)	instance moved/changed — supply explicitly
LeanModularForms/ForMathlib/GeneralizedResidueTheory/Residue.lean	invalid ▸ notation, the equality (L325)	an equality's type changed — fix the ▸
LeanModularForms/ForMathlib/HungerbuhlerWasem/CrossingDataBuilder.lean	ring failed, ring expressions not equal (L407)	normal-form/API change — inspect
PadicLFunctions/IwasawaProof/LogDerivative.lean	(in broken set)	inspect

These are independent breakages from different mathlib changes (not one root cause), so it's 7 separate repairs of varying difficulty — a producer/coordinator session, not the unattended bump cron. Start with CyclRat.lean (trivial upstreamed-dup deletion). NEVER add sorry or change statements; keep main green throughout.

Reproduce: branch off main, set lakefile.toml rev → 11b908e5cdd9 (+ lake update mathlib, lake exe cache get), then bash .mathlibable/tooling/build_all.sh 2>&1. Toolchain stays v4.32.0-rc1.