chore: better hypothesis for Vector.getElem_take

2026-03-29 00:04:11 +00:00 · 2025-03-12 14:51:49 +11:00
1 changed files with 1 additions and 1 deletions
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -2838,7 +2838,7 @@ theorem swap_comm (xs : Vector α n) {i j : Nat} {hi hj} :

 /-! ### take -/

-@[simp] theorem getElem_take (xs : Vector α n) (j : Nat) (hi : i < min n j) :
+@[simp] theorem getElem_take (xs : Vector α n) (j : Nat) (hi : i < min j n) :
    (xs.take j)[i] = xs[i] := by
  cases xs
  simp