From a827759f1dd331f064aba4b57d295a34f5e16639 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 30 Jul 2024 20:29:34 -0700 Subject: [PATCH] fix: mistake in statement of `List.take_takeWhile` (#4875) This theorem is meant to say that `List.take` and `List.takeWhile` commute. --- src/Init/Data/List/TakeDrop.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index 72baa785d1..6f4fd0df1f 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -411,11 +411,11 @@ theorem dropWhile_replicate (p : α → Bool) : split <;> simp_all theorem take_takeWhile {l : List α} (p : α → Bool) n : - (l.takeWhile p).take n = (l.takeWhile p).take n := by - induction l with - | nil => rfl + (l.takeWhile p).take n = (l.take n).takeWhile p := by + induction l generalizing n with + | nil => simp | cons x xs ih => - by_cases h : p x <;> simp [takeWhile_cons, h, ih] + by_cases h : p x <;> cases n <;> simp [takeWhile_cons, h, ih, take_succ_cons] @[simp] theorem all_takeWhile {l : List α} : (l.takeWhile p).all p = true := by induction l with