From e0017bd4c7adacc3de25a0d7036d20968cb9e1c7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 9 Sep 2024 15:17:06 +1000 Subject: [PATCH] chore: fix some List.modifyNth lemma names (#831) --- Batteries/Data/List/Lemmas.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index bb7255f4d0..a68d820a52 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -72,11 +72,13 @@ theorem get?_modifyNth (f : α → α) (n) (l : List α) (m) : (modifyNth f n l).get? m = (fun a => if n = m then f a else a) <$> l.get? m := by simp [getElem?_modifyNth] -theorem modifyNthTail_length (f : List α → List α) (H : ∀ l, length (f l) = length l) : +theorem length_modifyNthTail (f : List α → List α) (H : ∀ l, length (f l) = length l) : ∀ n l, length (modifyNthTail f n l) = length l | 0, _ => H _ | _+1, [] => rfl - | _+1, _ :: _ => congrArg (·+1) (modifyNthTail_length _ H _ _) + | _+1, _ :: _ => congrArg (·+1) (length_modifyNthTail _ H _ _) + +@[deprecated (since := "2024-06-07")] alias modifyNthTail_length := length_modifyNthTail theorem modifyNthTail_add (f : List α → List α) (n) (l₁ l₂ : List α) : modifyNthTail f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ modifyNthTail f n l₂ := by @@ -88,8 +90,10 @@ theorem exists_of_modifyNthTail (f : List α → List α) {n} {l : List α} (h : ⟨_, _, (take_append_drop n l).symm, length_take_of_le h⟩ ⟨_, _, eq, hl, hl ▸ eq ▸ modifyNthTail_add (n := 0) ..⟩ -@[simp] theorem modify_get?_length (f : α → α) : ∀ n l, length (modifyNth f n l) = length l := - modifyNthTail_length _ fun l => by cases l <;> rfl +@[simp] theorem length_modifyNth (f : α → α) : ∀ n l, length (modifyNth f n l) = length l := + length_modifyNthTail _ fun l => by cases l <;> rfl + +@[deprecated (since := "2024-06-07")] alias modify_get?_length := length_modifyNth @[simp] theorem getElem?_modifyNth_eq (f : α → α) (n) (l : List α) : (modifyNth f n l)[n]? = f <$> l[n]? := by