doc.verso: deleting prose from one docstring makes a later proof fail Decidable synthesis (elaboration state leak?)

[Deicyde]

Setup

• Lean v4.33.0, verso v4.33.0 (3bdedf29bada), Mathlib v4.33.0, macOS 14.4 (arm64)
• doc.verso = true in the package's leanOptions (docstrings elaborated as Verso markup during lake build)

Symptom

In a ~1,000-line Mathlib-based module, shortening the prose of either of two specific docstrings changes the elaboration of an unrelated declaration ~700 lines later. The proof there fails with:

error: TaoMeasure/Section_1_3_1.lean:887:6: failed to synthesize instance of type class
  Decidable (f x = g x)
error: TaoMeasure/Section_1_3_1.lean:888:6: No goals to be solved

at this (previously fine) by_cases:

theorem aeEq_equivalence {d : ℕ} (hd : 0 < d) (Z : Type*) :
    Equivalence fun f g : EuclideanSpace ℝ (Fin d) → Z => AEEq f g := by
  constructor
  ...
  · intro f g h hfg hgh
    have hsub : {x | ¬ f x = h x} ⊆ {x | ¬ f x = g x} ∪ {x | ¬ g x = h x} := by
      intro x hx
      by_cases hfgx : f x = g x     -- ← fails here after the docstring edit
      · exact Or.inr fun hghx => hx (hfgx.trans hghx)
      · exact Or.inl hfgx
  ...

(by_cases on a proposition over an arbitrary Type* — the classical fallback normally handles this, and does when the docstring prose is restored.)

One of the two load-bearing docstrings (attached to a plain def IsSimpleFunc ... : Prop), original on the left, edited on the right:

/-- `Definition 1.3.2` (Simple function; book p. 50).      /-- `Definition 1.3.2` (Simple function; book p. 50).
A *(complex-valued) simple function* `f : ℝᵈ → ℂ` is a     The book's `Simp(ℝᵈ)`, a commutative ∗-algebra
finite linear combination (1.8)                            (`isSimpleFunc_algebra_ops`); the same emphases as
`f = c₁ 1_{E₁} + ⋯ + c_k 1_{E_k}` of indicator             for the unsigned case apply. -/
functions of Lebesgue measurable sets `Eᵢ ⊆ ℝᵈ`,
where `k ≥ 0` and `c₁, …, c_k ∈ ℂ`. ... -/

The other is a similar prose-only shortening of a nearby lemma docstring; either edit alone triggers the failure, and reverting either prose edit alone fixes it when the other is intact.

What we ruled out

• Code changes: after stripping comments, the passing and failing files are byte-identical including all whitespace and layout (verified with a nesting-aware comment stripper + diff).
• Stale build state: reproduced across forced clean recompiles (artifacts deleted) in both directions, and distinguished true recompiles from Lake's log replay.
• Nondeterminism: an automated bisection over the file's 45 comment-only diff hunks ran 13 builds with perfectly consistent pass/fail results, isolating exactly these two hunks.
• Environment: the original-prose file builds green both locally and in CI on the same toolchain.

Hypothesis

Something in the doc.verso docstring elaboration path (possibly the code-element suggestion machinery — the module emits many "Code element could be more specific" hints for unresolvable spans) perturbs state that later term elaboration observes — the failure surfaces as Decidable instance synthesis failing where the classical fallback should (and otherwise does) engage. The removed docstring text is rich in code spans that don't elaborate (f = c₁ 1_{E₁} + ⋯ + c_k 1_{E_k}, Eᵢ ⊆ ℝᵈ), so the number/kind of failed span elaborations changing is one candidate mechanism.

Repro access

The module lives in a private repo (mathlib-initiative/tao-measure-lean, TaoMeasure/Section_1_3_1.lean; the failing/passing pair differs only in comments). Happy to give a maintainer access, run instrumented builds, or attempt a standalone minimization if this doesn't ring a bell.

🤖 Filed with Claude Code after an automated bisection; details verified by hand.

[Deicyde]

bug