diff --git a/Mathlib/Data/List/TakeDrop.lean b/Mathlib/Data/List/TakeDrop.lean
index 5b87b33c5b3cd6..1d27d414a3ce96 100644
--- a/Mathlib/Data/List/TakeDrop.lean
+++ b/Mathlib/Data/List/TakeDrop.lean
@@ -88,28 +88,6 @@ theorem tail_iterate (l : List α) (n : ℕ) : (List.tail^[n]) l = l.drop n := b
   | zero => rfl
   | succ n ih => cases l <;> simp [*]
 
-section TailDropLast
-
-variable (l : List α) (n : ℕ)
-
-theorem tail_take_eq_take_tail : (l.take n).tail = l.tail.take (n - 1) := by
-  ext
-  grind
-
-theorem dropLast_take_eq_take_dropLast : (l.take n).dropLast = l.dropLast.take (n - 1) := by
-  ext
-  grind
-
-theorem tail_drop_eq_drop_tail : (l.drop n).tail = l.tail.drop n := by
-  ext
-  grind
-
-theorem dropLast_drop_eq_drop_dropLast : (l.drop n).dropLast = l.dropLast.drop n := by
-  ext
-  grind
-
-end TailDropLast
-
 section TakeI
 
 variable [Inhabited α]