diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index 2d6e73a14b..fc2cecae44 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -117,10 +117,8 @@ splitAt 2 [a, b, c] = ([a, b], [c])
 ```
 -/
 def splitAt (n : Nat) (l : List α) : List α × List α := go l n [] where
-  /-- Auxiliary for `splitAt`: `splitAt.go l n xs acc = (acc.reverse ++ take n xs, drop n xs)`
-  if `n < length xs`, else `(l, [])`. -/
+  /-- Auxiliary for `splitAt`: `splitAt.go xs n acc = (acc.reverse ++ take n xs, drop n xs)`. -/
   go : List α → Nat → List α → List α × List α
-  | [], _, _ => (l, [])
   | x :: xs, n+1, acc => go xs n (x :: acc)
   | xs, _, acc => (acc.reverse, xs)
 
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index 8d8b3e1cd6..9e5f4e3ace 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -189,6 +189,22 @@ theorem get?_set_of_lt' (a : α) {m n} (l : List α) (h : m < length l) :
 
 @[deprecated (since := "2024-05-06")] alias length_removeNth := length_eraseIdx
 
+/-! ### splitAt -/
+
+theorem splitAt_go (n : Nat) (l acc : List α) :
+    splitAt.go l n acc = (acc.reverse ++ l.take n, l.drop n) := by
+  induction l generalizing n acc with
+  | nil => simp [splitAt.go]
+  | cons x xs ih =>
+    cases n with
+    | zero => simp [splitAt.go]
+    | succ n =>
+      rw [splitAt.go, take_succ_cons, drop_succ_cons, ih n (x :: acc),
+        reverse_cons, append_assoc, singleton_append]
+
+theorem splitAt_eq (n : Nat) (l : List α) : splitAt n l = (l.take n, l.drop n) := by
+  rw [splitAt, splitAt_go, reverse_nil, nil_append]
+
 /-! ### eraseP -/
 
 @[simp] theorem extractP_eq_find?_eraseP