From fe7524ba99cfee8543450dca83b28a3fa9a28bcc Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 25 Jul 2024 11:41:56 +1000
Subject: [PATCH] chore: deprecate sizeOf_dropSlice_lt

---
 Mathlib/Data/List/Basic.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
index 05396a0cc0190f..5a595878eb10d7 100644
--- a/Mathlib/Data/List/Basic.lean
+++ b/Mathlib/Data/List/Basic.lean
@@ -2708,6 +2708,23 @@ theorem dropSlice_eq (xs : List α) (n m : ℕ) : dropSlice n m xs = xs.take n +
   · cases xs <;> simp [dropSlice]
   · cases xs <;> simp [dropSlice, *, Nat.succ_add]
 
+@[simp]
+theorem length_dropSlice (i j : ℕ) (xs : List α) :
+    (List.dropSlice i j xs).length = xs.length - min j (xs.length - i) := by
+  induction xs generalizing i j with
+  | nil => simp
+  | cons x xs xs_ih =>
+    cases i <;> simp only [List.dropSlice]
+    · cases j with
+      | zero => simp
+      | succ n => simp_all [xs_ih]; omega
+    · simp [xs_ih]; omega
+
+theorem length_dropSlice_lt (i j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < xs.length) :
+    (List.dropSlice i j xs).length < xs.length := by
+  simp; omega
+
+@[deprecated (since := "2024-07-25")]
 theorem sizeOf_dropSlice_lt [SizeOf α] (i j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < xs.length) :
     SizeOf.sizeOf (List.dropSlice i j xs) < SizeOf.sizeOf xs := by
   induction xs generalizing i j hj with