From 47595540bbcd5ef218e60e11d6586589ff3788e1 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 22 Feb 2024 16:15:09 +1100
Subject: [PATCH] chore: more List lemmas for auto (#3454)

---
 src/Init/Data/List/Lemmas.lean | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 9cb8fd077f..cc78175354 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -242,6 +242,31 @@ theorem getLast?_eq_get? : ∀ (l : List α), getLast? l = l.get? (l.length - 1)
 @[simp] theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
   simp [getLast?_eq_get?, Nat.succ_sub_succ]
 
+theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a
+  | [], _, _ => rfl
+  | _a::_, 0, _ => rfl
+  | _::l, _+1, _ => getD_eq_get? (l := l) ..
+
+theorem get?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n →
+  (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length)
+| [], _, n, _ => rfl
+| a :: l, _, n+1, h₁ => by rw [cons_append]; simp [get?_append_right (Nat.lt_succ.1 h₁)]
+
+theorem get?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l →
+    get? l.reverse i = get? l j
+  | [], _, _, _ => rfl
+  | a::l, i, 0, h => by simp at h; simp [h, get?_append_right]
+  | a::l, i, j+1, h => by
+    have := Nat.succ.inj h; simp at this ⊢
+    rw [get?_append, get?_reverse' _ j this]
+    rw [length_reverse, ← this]; apply Nat.lt_add_of_pos_right (Nat.succ_pos _)
+
+theorem get?_reverse {l : List α} (i) (h : i < length l) :
+    get? l.reverse i = get? l (l.length - 1 - i) :=
+  get?_reverse' _ _ <| by
+    rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h),
+      Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)]
+
 /-! ### take and drop -/
 
 @[simp] theorem take_append_drop : ∀ (n : Nat) (l : List α), take n l ++ drop n l = l