fix: mark List.length as @[implicit_reducible]

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). After
`simp only [List.length_cons]`, the main expression has `l.length + 1` but
instances still have `(a :: l).length`, and `isDefEq` won't unfold `List.length`
to reconcile them.

Marking `List.length` as `@[implicit_reducible]` allows `isDefEq` to unfold it
when checking implicit arguments, restoring the previous behavior.

The root cause is that `GetElem` carries complex proof obligations in its type
class instances, making the implicit arguments sensitive to definitional equality.
We are considering a longer-term 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.

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

src/Init/Data/Array/Find.lean

@@ -622,12 +622,12 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
 /-! ### findFinIdx? -/
 
 @[grind =]
-theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp; rfl
+theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
 
 @[grind =]
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp; rfl
+  simp
 
 -- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
 theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
@@ -801,7 +801,7 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
   simp [idxOf?, finIdxOf?]
 
-@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp; rfl
+@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
 
 @[simp, grind =] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.finIdxOf? a = none ↔ a ∉ xs := by

src/Init/Data/List/Find.lean

@@ -1050,7 +1050,7 @@ theorem findFinIdx?_append {xs ys : List α} {p : α → Bool} :
 
 @[simp, grind =] theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     [a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp [findFinIdx?_cons, findFinIdx?_nil]; rfl
+  simp [findFinIdx?_cons, findFinIdx?_nil]
 
 @[simp, grind =] theorem findFinIdx?_eq_none_iff {l : List α} {p : α → Bool} :
     l.findFinIdx? p = none ↔ ∀ x ∈ l, ¬ p x := by

src/Init/Data/List/Sort/Impl.lean

@@ -182,7 +182,6 @@ private theorem mergeSortTR_run_eq_mergeSort : {n : Nat} → (l : { l : List α
     simp only [mergeSortTR.run, mergeSortTR.run, mergeSort]
     rw [merge_eq_mergeTR]
     rw [mergeSortTR_run_eq_mergeSort, mergeSortTR_run_eq_mergeSort]
-    rfl
 
 -- We don't make this a `@[csimp]` lemma because `mergeSort_eq_mergeSortTR₂` is faster.
 theorem mergeSort_eq_mergeSortTR : @mergeSort = @mergeSortTR := by

src/Init/Data/Vector/Find.lean

@@ -303,12 +303,12 @@ theorem find?_eq_some_iff_getElem {xs : Vector α n} {p : α → Bool} {b : α}
 /-! ### findFinIdx? -/
 
 @[grind =]
-theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp; rfl
+theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp
 
 @[grind =]
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp; rfl
+  simp
 
 @[congr] theorem findFinIdx?_congr {p : α → Bool} {xs : Vector α n} {ys : Vector α n} (w : xs = ys) :
     findFinIdx? p xs = findFinIdx? p ys := by

src/Init/Data/Vector/Monadic.lean

@@ -53,7 +53,7 @@ theorem mapM_pure [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β) :
     (mk #[] rfl).mapM f = pure #v[] := by
   unfold mapM
   unfold mapM.go
-  simp; rfl
+  simp
 
 @[simp, grind =] theorem mapM_append [Monad m] [LawfulMonad m]
     {f : α → m β} {xs : Vector α n} {ys : Vector α n'} :

src/Init/Prelude.lean

@@ -3004,7 +3004,7 @@ Examples:
  * `([] : List String).length = 0`
  * `["green", "brown"].length = 2`
 -/
-def List.length : List α → Nat
+@[implicit_reducible] def List.length : List α → Nat
   | nil       => 0
   | cons _ as => HAdd.hAdd (length as) 1
 

tests/elab/Reparen.lean.out.expected

@@ -2983,7 +2983,7 @@ Examples:
  * `([] : List String).length = 0`
  * `["green", "brown"].length = 2`
 -/
-def List.length : List α → Nat
+@[implicit_reducible] def List.length : List α → Nat
   | nil       => 0
   | cons _ as => HAdd.hAdd (  length as)1