fix: disambiguate Verso labels for Ex. 1.2.2, 1.2.22, and 9.2.1

[Chessing234]

Summary

• Split Measure Theory Exercise 1.2.2 into (i)/(ii) and 1.2.22 into (i)–(iii).
• Label Analysis I Exercise 9.2.1 parts (a)–(d), including previously undocumented (c)/(d).

Test plan

• CI Build book
• Confirm Verso anchors for these exercises are unique

Made with Cursor

[Chessing234]

@teorth gentle bump — this is a small Verso/docstring hygiene fix with green CI. Happy to rebase or adjust if anything looks off; otherwise ready whenever you have a moment.

[teorth]

Thanks for the careful work here — but I'm going to decline this one, because the premise doesn't hold for this repo.

Repeated identical exercise docstrings are intentional house style, not a build hazard. They appear throughout: 12x /-- Exercise 5.4.9 -/, 6x /-- Exercise 3.5.4 -/, 6x /-- Exercise 3.1.7 -/, and many more. There is no label or anchor machinery keyed on docstring text — literate.toml sets docstrings_as_text = true, so docstrings render as plain text and book anchors come from declaration names. The book has been building and deploying with these duplicates all along, which is also why CI is green on these PRs: there was nothing to fix.

The added parentheticals also introduce part-labels that aren't in the textbook (e.g. Definition 6.1.3 (ε-steady, def), Definition 6.1.8 (lim, characterization)), which risks reading as though the text has parts it doesn't.

If you'd like to propose changing this convention, please open an issue first — it should be settled repo-wide rather than section by section.

The contributions I'm most glad to receive are the ones you've been sending: corrections to sorryd statements that are false or mis-hypothesized, in the spirit of #517. Those have been genuinely valuable.

[teorth]

Reopening — please disregard my previous comment, which was wrong.

I assessed this against a stale checkout of main that was roughly 200 commits behind origin/main. The duplicate-docstring counts I cited (12x /-- Exercise 5.4.9 -/ and so on) were from that stale tree; those had already been fixed on main by #616 and the other label PRs. The label-disambiguation work is an active and accepted cleanup here, not a departure from house style, and this PR is a legitimate continuation of it.

Apologies for the noise.

[teorth]

Could you rebase this on current main? It conflicts in Analysis/MeasureTheory/Section_1_2_2.lean, which has moved since (#574, #561, 874c8f3 and others touched the Exercise 1.2.x labels there) — worth checking whether the 1.2.22 hunk is still needed after that.

The Section 9.2 part is still wanted: Exercise_9_2_1c/d genuinely lack the docstrings that a/b have.