variables names, need to leave the linter on

src/Init/Data/Array/Basic.lean

@@ -1102,6 +1102,20 @@ instance instLE [LT α] : LE (Array α) := ⟨fun as bs => as.toList ≤ bs.toLi
 We do not currently intend to provide verification theorems for these functions.
 -/
 
+/-! ### leftpad and rightpad -/
+
+/--
+Pads `l : Array α` on the left with repeated occurrences of `a : α` until it is of size `n`.
+If `l` is initially larger than `n`, just return `l`.
+-/
+def leftpad (n : Nat) (a : α) (xs : Array α) : Array α := mkArray (n - xs.size) a ++ xs
+
+/--
+Pads `l : Array α` on the right with repeated occurrences of `a : α` until it is of size `n`.
+If `l` is initially larger than `n`, just return `l`.
+-/
+def rightpad (n : Nat) (a : α) (xs : Array α) : Array α := xs ++ mkArray (n - xs.size) a
+
 /- ### reduceOption -/
 
 /-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/

src/Init/Data/Array/Lemmas.lean

@@ -3185,6 +3185,19 @@ theorem foldr_rel {xs : Array α} {f g : α → β → β} {a b : β} (r : β
   rcases xs with ⟨xs⟩
   simp
 
+/-! ## Additional operations -/
+
+/-! ### leftpad -/
+
+-- We unfold `leftpad` and `rightpad` for verification purposes.
+attribute [simp] leftpad rightpad
+
+theorem size_leftpad (n : Nat) (a : α) (xs : Array α) :
+    (leftpad n a xs).size = max n xs.size := by simp; omega
+
+theorem size_rightpad (n : Nat) (a : α) (xs : Array α) :
+    (rightpad n a xs).size = max n xs.size := by simp; omega
+
 /-! Content below this point has not yet been aligned with `List`. -/
 
 /-! ### sum -/

src/Init/Data/List/Lemmas.lean

@@ -2883,7 +2883,7 @@ theorem getLast?_replicate (a : α) (n : Nat) : (replicate n a).getLast? = if n
 -- We unfold `leftpad` and `rightpad` for verification purposes.
 attribute [simp] leftpad rightpad
 
--- `length_leftpad` is in `Init.Data.List.Nat.Basic`.
+-- `length_leftpad` and `length_rightpad` are in `Init.Data.List.Nat.Basic`.
 
 theorem leftpad_prefix (n : Nat) (a : α) (l : List α) :
     replicate (n - length l) a <+: leftpad n a l := by

src/Init/Data/List/Nat/Basic.lean

@@ -63,10 +63,18 @@ theorem getElem_eq_getElem_reverse {l : List α} {i} (h : i < l.length) :
   to the larger of `n` and `l.length` -/
 -- We don't mark this as a `@[simp]` lemma since we allow `simp` to unfold `leftpad`,
 -- so the left hand side simplifies directly to `n - l.length + l.length`.
-theorem leftpad_length (n : Nat) (a : α) (l : List α) :
+theorem length_lengthpad (n : Nat) (a : α) (l : List α) :
     (leftpad n a l).length = max n l.length := by
   simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max]
 
+@[deprecated length_lengthpad (since := "2025-02-24")]
+abbrev leftpad_length := @length_lengthpad
+
+theorem length_rightpad (n : Nat) (a : α) (l : List α) :
+    (rightpad n a l).length = max n l.length := by
+  simp [rightpad]
+  omega
+
 /-! ### eraseIdx -/
 
 theorem mem_eraseIdx_iff_getElem {x : α} :

src/Init/Data/List/ToArray.lean

@@ -633,4 +633,12 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j
   · simp only [size_toArray, Nat.not_le] at h'
     rw [List.insertIdx_of_length_lt (h := h')]
 
+@[simp] theorem leftpad_toArray (n : Nat) (a : α) (l : List α) :
+    Array.leftpad n a l.toArray = (leftpad n a l).toArray := by
+  simp [leftpad, Array.leftpad, ← toArray_replicate]
+
+@[simp] theorem rightpad_toArray (n : Nat) (a : α) (l : List α) :
+    Array.rightpad n a l.toArray = (rightpad n a l).toArray := by
+  simp [rightpad, Array.rightpad, ← toArray_replicate]
+
 end List

src/Init/Data/Vector/Basic.lean

@@ -455,6 +455,24 @@ to avoid having to have the predicate live in `p : α → m (ULift Bool)`.
 @[inline] def count [BEq α] (a : α) (xs : Vector α n) : Nat :=
   xs.toArray.count a
 
+/--
+Pad a vector on the left with a given element.
+
+Note that we immediately simplify this to an `++` operation,
+and do not provide separate verification theorems.
+-/
+@[inline, simp] def leftpad (n : Nat) (a : α) (xs : Vector α m) : Vector α (max n m) :=
+  (mkVector (n - m) a ++ xs).cast (by omega)
+
+/--
+Pad a vector on the right with a given element.
+
+Note that we immediately simplify this to an `++` operation,
+and do not provide separate verification theorems.
+-/
+@[inline, simp] def rightpad (n : Nat) (a : α) (xs : Vector α m) : Vector α (max n m) :=
+  (xs ++ mkVector (n - m) a).cast (by omega)
+
 /-! ### ForIn instance -/
 
 @[simp] theorem mem_toArray_iff (a : α) (xs : Vector α n) : a ∈ xs.toArray ↔ a ∈ xs :=

src/Init/Data/Vector/Lemmas.lean

@@ -2331,6 +2331,15 @@ theorem foldr_rel {xs : Array α} {f g : α → β → β} {a b : β} (r : β
   rcases xs with ⟨xs⟩
   simp
 
+/-! ### leftpad and rightpad -/
+
+@[simp] theorem leftpad_mk (n : Nat) (a : α) (xs : Array α) (h : xs.size = m) :
+    (Vector.mk xs h).leftpad n a = Vector.mk (Array.leftpad n a xs) (by simp [h]; omega) := by
+  simp [h]
+
+@[simp] theorem rightpad_mk (n : Nat) (a : α) (xs : Array α) (h : xs.size = m) :
+    (Vector.mk xs h).rightpad n a = Vector.mk (Array.rightpad n a xs) (by simp [h]; omega) := by
+  simp [h]
 
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/