fix: CI version validation for CACHE STRING CMake format

The `sed` regex for LEAN_VERSION_IS_RELEASE expected the line to end
with `)` immediately after the number, but the line now has `CACHE
STRING ""` after the value. Use `grep -oE` consistent with the other
version extractions.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

chore: remove lean4checker from release repos (#13121)

Lean4checker has been merged into this repository and is no longer a
standalone repo.

[Backport releases/v4.29.0] chore: stop using cached namespace.so che…

chore: remove non-deterministic bv_decide counterexample tests

Remove bv_decide tests that match specific counterexample values, as the
SAT solver output is non-deterministic across runs.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

chore: make fsanitize CI non-blocking for releases

This makes the fsanitize job secondary at all CI levels, including
tag pushes (level 3). The fsanitize build has been OOM-killing on
CI runners, blocking release page creation.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

perf: add high priority to `OfSemiring.Q` instances (#12782)

This PR adds high priority to instances for `OfSemiring.Q` in the grind
ring envelope. When Mathlib is imported, instance synthesis for types
like `OfSemiring.Q Nat` becomes very expensive because the solver
explores many irrelevant paths before finding the correct instances. By
marking these instances as high priority and adding shortcut instances
for basic operations (`Add`, `Sub`, `Mul`, `Neg`, `OfNat`, `NatCast`,
`IntCast`, `HPow`), instance synthesis resolves quickly.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Kim Morrison <kim@tqft.net>

fix: normalize instance argument in getStuckMVar? for class projectio…

fix: set implicitReducible on grandparent subobject projections (#12701)

This PR fixes a gap in how `@[implicit_reducible]` is assigned to parent
projections during structure elaboration.

When `class C extends P₁, P₂` has diamond inheritance, some ancestor
structures become constructor subobject fields even though they aren't
direct parents. For example, in `Monoid extends Semigroup, MulOneClass`,
`One` becomes a constructor subobject of `Monoid` — its field `one`
doesn't overlap with `Semigroup`'s fields, and `inSubobject?` is `none`
during `MulOneClass` flattening.

`mkProjections` creates the projection `Monoid.toOne` but defers
reducibility to `addParentInstances` (guarded by `if !instImplicit`).
However, `addParentInstances` only processes direct parents from the
`extends` clause. Grandparent subobject projections fall through the gap
and stay `semireducible`.

This causes defeq failures when `backward.isDefEq.respectTransparency`
is enabled (#12179): at `.instances` transparency, the semireducible
grandparent projection can't unfold, so two paths to the same ancestor
structure aren't recognized as definitionally equal.

Fix: before `addParentInstances`, iterate over all `.subobject` fields
and set `implicitReducible` on those whose parent is a class.

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

chore: fix LEAN_VERSION_MINOR for v4.29.0

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

chore: set LEAN_VERSION_IS_RELEASE for v4.29.0

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>