fix: mark List.length as @[implicit_reducible]

[leodemoura]

This PR fixes a regression introduced in Lean 4.29.0-rc2 where simp no longer simplifies inside type class instance arguments due to the backward.isDefEq.respectTransparency change. This breaks proofs where a term like (a :: l).length appears both in the main expression and inside implicit instance arguments (e.g., determining a BitVec width).

The problem: After simp only [List.length_cons], the main expression has l.length + 1 but instances still have (a :: l).length. Since simp no longer simplifies inside instances, and isDefEq won't unfold List.length at the default transparency, subsequent lemma applications fail.

Reproducer (from Son Ho, reported by Sebastian Ullrich):

theorem BitVec.getElem!_eq_testBit_toNat {w : Nat} (x : BitVec w) (i : Nat) :
     x[i]! = x.toNat.testBit i := by sorry

example (l : List Nat) (a : Nat) (j : Nat) :
  (0#((a :: l).length))[j]! = (0#((a :: l).length)).toNat.testBit j := by
  simp only [List.length_cons]
  simp only [BitVec.getElem!_eq_testBit_toNat] -- works in 4.28.0-rc1, fails in 4.29.0-rc6

The fix: Mark List.length as @[implicit_reducible], allowing isDefEq to unfold it when checking implicit arguments. Several proofs that previously needed a trailing rfl after simp now close directly, since simp can see through List.length in more positions.

Longer term: The root cause is that GetElem carries complex proof obligations in its type class instances, making implicit arguments sensitive to definitional equality of collection sizes. We are considering a redesign with a noncomputable GetElemV variant based on Nonempty that avoids these casts entirely, but that is a larger change planned for a future release.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-09 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-15 02:40:53)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-12924 build failed against this PR. (2026-03-15 03:27:08) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-12924 build this PR didn't complete normally. (2026-03-18 04:07:34) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-12924 build this PR didn't complete normally. (2026-03-18 04:08:44) View Log