Bump toolchain to v4.35.0

[zhikaip]

Bumps the project from v4.29.0-rc8 to v4.35.0 (Lean and Mathlib).

Dependency changes

• lean-toolchain: leanprover/lean4:v4.35.0
• lakefile.lean: Mathlib pinned to v4.35.0; verso and doc-gen4 pinned to their v4.35.0 tags (their main branches have already moved on to v4.36.0-rc1, which would not build on this toolchain).
• lake-manifest.json regenerated with lake update -R -Kenv=dev. Verso now pulls in illuminate as a transitive dependency.

Source changes

Only proofs were changed; no statements, definitions or exercise sorrys were touched, and no sorry was added. Recurring causes, in rough order of frequency:

• Mathlib.Tactic no longer transitively imports analysis/topology modules, so explicit imports were added where EuclideanSpace, HasDerivWithinAt, exists_deriv_eq_slope, CauSeq.tendsto_limit, Real.mem_closure_iff, ContDiffOn, Uncountable ℝ etc. are used.
• Structures built inline with a tactic proof for a proof field (Function.Embedding.inj', AddMonoidHom.map_add') are no longer unfolded by simp/rw under the new transparency check; the proof field now gets an explicit show Function.Injective _ by ... (or the surrounding step avoids the coercion).
• simp fails when it makes no progress; convert leaves side goals that previously closed by rfl; a few grind calls now time out on integ/upper_integral goals and were replaced by unfold ...; linarith.
• List.TFAE.out is now 1-indexed (all call sites bumped; the Appendix A.1 note about 0-indexing was updated).
• Renames/removals: Finset.prod_le_prod → Finset.prod_le_prod₀ (ordered semiring version), Finset.sum_inter_add_sum_diff → Finset.sum_inter_add_sum_sdiff, tendsto_finset_sum → tendsto_finsetSum, Finsupp.single_* on AddMonoidAlgebra → AddMonoidAlgebra.single_*, _root_.not_imp → Classical.not_imp, DFunLike.coe_injective' → coe_injective, isWellFounded_iff no longer needed for WellFoundedLT.
• HasSubset.Subset.trans dot-notation no longer applies to the custom ⊆ on BoundedInterval; replaced by _root_.trans (the IsTrans instance already exists).
• instance declarations with explicit non-inferable hypotheses are now errors; two were changed to theorem/def (TaggedPartition.nhds_zero_neBot, IsElementary.ae_equiv), their call sites pass the arguments explicitly already.
• A declaration header continuation line starting at column 0 is now a parse error (Sections 5.2, 10.1).
• Verso docstrings: {kw (of := «term_≤_»)} fails because core now defines ≤ via unicode(" ≤ ", " <= "), which the kw role's atom matcher does not handle; switched to {kw! (of := «term_≤_»)} for those three sites, the documented way to skip the atom check while still validating the kind name (< and the other kw uses still resolve). This is a core Lean bug, reported on Zulip: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.7Bkw.7D.20docstring.20role.20fails.20for.20unicode.28.2E.2E.2E.29.20notations.20like.20.E2.89.A4/with/632378234

Verification

• lake build of the whole library passes locally (Windows, Lean v4.35.0).
• lake query :literateHtml (the Verso book) builds.
• lake -R -Kenv=dev build Analysis:docs was not run locally: compiling doc-gen4's C dependencies fails with the local mingw cc, unrelated to this change. CI (Ubuntu) should exercise it.

Deprecation renames (second commit)

The second commit mechanically applies the deprecation warnings Mathlib v4.35.0 emits for this library: push_neg → push Not, Set.mem_setOf_eq → Set.mem_ofPred_eq, if_pos/if_neg/if_true/if_false → ite_eq_left/ite_eq_right/ite_true/ite_false, dif_pos/dif_neg → dite_eq_left/dite_eq_right, the Set.*diff* family → Set.*sdiff*, tendsto_finset_sum/continuous_finset_prod and friends → camelCase, and the deprecated imports Mathlib.Data.Real.Sign → Mathlib.Basic.Real.Sign and Mathlib.Algebra.Field.Power → Mathlib.Algebra.Ring.Int.Parity. All replacements are statement-identical aliases except Equiv.apply_eq_iff_eq_symm_apply → Equiv.eq_symm_apply (sides of the iff swapped, so the ← was dropped) and one List.tfae_cons_self → List.tfae_cons_of_mem in a simp_all list where the argument is unused either way. After this commit the only remaining deprecation warnings are the 40 uses of peel, whose suggested replacements (gconvert/congr!) are not drop-in and are left for a follow-up. The 136 "consider adding module" notices are likewise left for a separate PR.

Rebase onto #737 (third commit)

Rebased onto main after #737 put Section 1.4 into the build. The MeasureTheory PRs merged in between (#694–#737) were written against 4.29 and needed the same kinds of repair under 4.35, kept in a separate commit: eleven new List.TFAE.out calls in Section_1_3_2 shifted to 1-based indices; in Section_1_4_1 two simpa [LebesgueMeasurable.boolean_algebra] steps now show the unfolded goal first and two exercise statements declared as instance with non-class types became theorems; Section_1_4_2 imports Mathlib.MeasureTheory.MeasurableSpace.Defs and Section_1_4_3 imports Mathlib.MeasureTheory.Measure.NullMeasurable (no longer provided transitively by Mathlib.Tactic); and Measure.toCountablyAdditiveMeasure is marked noncomputable since ENNReal.toEReal now is. Section_1_4_4 and Section_1_4_5 compiled without changes. Every file on disk is reached from Analysis.lean except Misc/equational.lean, which has never been imported and compiles cleanly standalone on 4.35.

New Lean linters (fourth commit)

Two linters added since 4.29 fire on the MeasureTheory files. linter.defProp flagged 40 proofs declared with def; they are now theorem (the 10 carrying a book label, plus the 14 helpers in the all-theorem Section 1.4 files) or lemma (the 16 unlabelled helpers in Sections 1.1.1, 1.3.1 and 1.3.4, following the tree's tendency for helpers). warn.classDefReducibility flagged 32 defs that build values of the class types ConcreteBooleanAlgebra, ConcreteSigmaAlgebra and MeasurableSpace; they now carry @[instance_reducible] as the warning suggests. Keyword and attribute changes only. Warnings drop from 319 to 247; what remains is the 140 module-system notices, the 40 peel deprecations and style lints (haveI, unused simp args, unused tactics).

🤖 Generated with Claude Code

[zhikaip]

Hi @teorth , I noticed that this project has diverged from mathlib quite significantly, so I took the time to bump the version with the help of Claude. I haven't worked through the textbook yet, so I can't vouch for the faithfulness of all fixes, but I think they look reasonable and nothing stands out in particular to me. Hopefully you're ok with this and I'll propose fixes if I notice any in the future.

There are still some outstanding tasks which I'm planning to do if this is merged, including moving the project to the module system, some style warnings and replacing the peel tactic. but this PR is already substantial and I'd rather fix those separately.

[teorth]

Thanks for this — and for pinning doc-gen4 and verso to v4.35.0 rather than leaving them on main, which makes the build reproducible as a side benefit.

I'm not merging it on my own initiative, because the pinned toolchain and Mathlib version are a project-wide decision for @teorth rather than a routine review call, so I've flagged it for him.

Two notes meanwhile, neither a problem with the PR:

1. It will need a rebase. A fair number of MeasureTheory PRs landed today (Fill Lebesgue positivity/empty and Dirac finite additivity #694, Fill scalar multiplication of finitely additive measures #700, Compile Boolean and sigma algebras and complete null-set unions #711, Fill finite additivity of counting measure #712, Prove measurability of continuous real and complex functions #721–Prove measurability of nonnegative almost-everywhere limits #730, Require nonnegative integrands for unsigned Riemann compatibility #734), plus build-tooling changes (Handle HEAD and query strings in preview redirects #731–Avoid preview hangs caused by idle browser connections #733, Keep preview symlink targets inside the generated site #735). They don't conflict with your diff textually — I checked each one against this branch — but they add new proofs written against 4.29, and those have not been exercised under 4.35. None of them uses Set.mem_setOf_eq, which is the lemma most of your repairs are about, so the overlap looks small.

2. More importantly: Analysis.lean was not importing Section_1_4_1, Section_1_4_2, Section_1_4_3, Section_1_4_4 or Section_1_4_5, so none of those five files was being compiled by CI at all. fix(MeasureTheory): Section 1.4 was never in the build; add imports and repair it #737 adds the imports and repairs what had broken while unobserved. Once that lands, this PR's CI will start covering ~5 more files than it does now, so expect some additional 4.35 fixes to be needed there. Rebasing after fix(MeasureTheory): Section 1.4 was never in the build; add imports and repair it #737 rather than before will save you a round.

Sorry to add a rebase to a 70-file PR — the import gap is the reason, and it's now fixed.

[zhikaip]

Rebased on the latest main, please see updated PR summary for details and let me know if there's any issues. Will do a further follow-up cleanup PR after this is merged.