From 0d94db201e1b16df6239d37ebb3a5511fcdd1c77 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Thu, 12 Feb 2026 10:54:04 +0100
Subject: [PATCH 01/10] scanl/r

---
 src/Init/Core.lean                  |   8 +
 src/Init/Data/List/Scan.lean        |  10 +
 src/Init/Data/List/Scan/Basic.lean  |  62 +++++
 src/Init/Data/List/Scan/Lemmas.lean | 345 ++++++++++++++++++++++++++++
 4 files changed, 425 insertions(+)
 create mode 100644 src/Init/Data/List/Scan.lean
 create mode 100644 src/Init/Data/List/Scan/Basic.lean
 create mode 100644 src/Init/Data/List/Scan/Lemmas.lean

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 6e5341ceddbd..f82999762d4f 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -2583,3 +2583,11 @@ class Trichotomous (r : α → α → Prop) : Prop where
   trichotomous (a b : α) : ¬ r a b → ¬ r b a → a = b
 
 end Std
+
+@[simp] theorem flip_flip {α : Sort u} {β : Sort v} {φ : Sort w} {f : α → β → φ} :
+    flip (flip f) = f := by
+  apply funext
+  intro a
+  apply funext
+  intro b
+  rw [flip, flip]
diff --git a/src/Init/Data/List/Scan.lean b/src/Init/Data/List/Scan.lean
new file mode 100644
index 000000000000..889753bcad4d
--- /dev/null
+++ b/src/Init/Data/List/Scan.lean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.List.Scan.Basic
+public import Init.Data.List.Scan.Lemmas
diff --git a/src/Init/Data/List/Scan/Basic.lean b/src/Init/Data/List/Scan/Basic.lean
new file mode 100644
index 000000000000..1a5dbd2421b9
--- /dev/null
+++ b/src/Init/Data/List/Scan/Basic.lean
@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chad Sharp
+-/
+module
+
+prelude
+public import Init.Data.List.Basic
+public import Init.Control.Id
+
+public section
+
+namespace List
+
+/-- Tail-recursive helper function for `scanlM` and `scanrM` -/
+@[inline]
+private def scanAuxM [Monad m] (f : β → α → m β) (init : β) (l : List α) : m (List β) :=
+  go l init []
+where
+  /-- Auxiliary for `scanAuxM` -/
+  @[specialize] go : List α → β → List β → m (List β)
+    | [], last, acc => pure <| last :: acc
+    | x :: xs, last, acc => do go xs (← f last x) (last :: acc)
+
+/--
+Folds a monadic function over a list from the left, accumulating partial results starting with
+`init`. The accumulated values are combined with the each element of the list in order, using `f`.
+-/
+@[inline]
+def scanlM [Monad m] (f : β → α → m β) (init : β) (l : List α) : m (List β) :=
+  List.reverse <$> scanAuxM f init l
+
+/--
+Folds a monadic function over a list from the right, accumulating partial results starting with
+`init`. The accumulated values are combined with the each element of the list in order, using `f`.
+-/
+@[inline]
+def scanrM [Monad m] (f : α → β → m β) (init : β) (xs : List α) : m (List β) :=
+  scanAuxM (flip f) init xs.reverse
+
+/--
+Fold a function `f` over the list from the left, returning the list of partial results.
+```
+scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]
+```
+-/
+@[inline]
+def scanl (f : β → α → β) (init : β) (as : List α) : List β :=
+  Id.run <| as.scanlM (pure <| f · ·) init
+
+/--
+Fold a function `f` over the list from the right, returning the list of partial results.
+```
+scanr (+) 0 [1, 2, 3] = [6, 5, 3, 0]
+```
+-/
+@[inline]
+def scanr (f : α → β → β) (init : β) (as : List α) : List β :=
+  Id.run <| as.scanrM (pure <| f · ·) init
+
+end List
diff --git a/src/Init/Data/List/Scan/Lemmas.lean b/src/Init/Data/List/Scan/Lemmas.lean
new file mode 100644
index 000000000000..2c41fce8eb3e
--- /dev/null
+++ b/src/Init/Data/List/Scan/Lemmas.lean
@@ -0,0 +1,345 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+module
+
+prelude
+public import Init.Data.List.Scan.Basic
+public import Init.Data.List.Lemmas
+import all Init.Data.List.Scan.Basic
+import Init.Data.List.TakeDrop
+import Init.Data.Option.Lemmas
+import Init.Data.Nat.Lemmas
+-- public import Init
+
+public section
+
+/-!
+# List scan
+
+Prove basic results about `List.scanl`, `List.scanr`, `List.scanlM` and `List.scanrM`.
+-/
+
+namespace List
+
+/-! ### `List.scanlM` and `List.scanrM` -/
+
+@[local simp]
+private theorem scanAuxM.go_eq_append_map [Monad m] [LawfulMonad m] {f : α → β → m α} :
+    go f xs last acc = (· ++ acc) <$> scanAuxM f last xs := by
+  unfold scanAuxM
+  induction xs generalizing last acc with
+  | nil => simp [scanAuxM.go]
+  | cons _ _ ih => simp [scanAuxM.go, ih (acc := last :: acc), ih (acc := [last])]
+
+private theorem scanAuxM_nil [Monad m] {f : α → β → m α} :
+    scanAuxM f init [] = return [init] := rfl
+
+private theorem scanAuxM_cons [Monad m] [LawfulMonad m] {f : α → β → m α} :
+    scanAuxM f init (x :: xs) = return (← scanAuxM f (← f init x) xs) ++ [init] := by
+  rw [scanAuxM, scanAuxM.go]
+  simp
+
+@[simp, grind =]
+theorem scanlM_nil [Monad m] [LawfulMonad m] {f : α → β → m α} :
+    scanlM f init [] = return [init] := by
+  simp [scanlM, scanAuxM_nil]
+
+@[simp, grind =]
+theorem scanlM_cons [Monad m] [LawfulMonad m] {f : α → β → m α} :
+    scanlM f init (x :: xs) = return init :: (← scanlM f (← f init x) xs) := by
+  simp [scanlM, scanAuxM_cons]
+
+@[simp, grind =]
+theorem scanrM_concat [Monad m] [LawfulMonad m] {f : α → β → m β} :
+    scanrM f init (xs ++ [x]) = return (← scanrM f (← f x init) xs) ++ [init] := by
+  simp [scanrM, flip, scanAuxM_cons]
+
+@[simp, grind =]
+theorem scanrM_nil [Monad m] {f : α → β → m β} :
+    scanrM f init [] = return [init] :=
+  (rfl)
+
+theorem scanlM_eq_scanrM_reverse [Monad m] {f : β → α → m β} :
+    scanlM f init as = reverse <$> (scanrM (flip f) init as.reverse) := by
+  simp only [scanrM, reverse_reverse]
+  rfl
+
+theorem scanrM_eq_scanlM_reverse [Monad m] [LawfulMonad m] {f : α → β → m β} :
+    scanrM f init as = reverse <$> (scanlM (flip f) init as.reverse) := by
+  simp only [scanlM_eq_scanrM_reverse, reverse_reverse, id_map', Functor.map_map]
+  rfl
+
+@[simp, grind =]
+theorem scanrM_reverse [Monad m] [LawfulMonad m] {f : α → β → m β} :
+    scanrM f init as.reverse = reverse <$> (scanlM (flip f) init as) := by
+  simp [scanrM_eq_scanlM_reverse (as := as.reverse)]
+
+@[simp, grind =]
+theorem scanlM_reverse [Monad m] {f : β → α → m β} :
+    scanlM f init as.reverse = reverse <$> (scanrM (flip f) init as) := by
+  simp [scanlM_eq_scanrM_reverse (as := as.reverse)]
+
+theorem scanlM_pure [Monad m] [LawfulMonad m] {f: β → α → β} {as : List α} :
+    as.scanlM (m := m) (pure <| f · ·) init = pure (as.scanl f init) := by
+  induction as generalizing init with simp_all [scanlM_cons, scanl]
+
+theorem scanrM_pure [Monad m] [LawfulMonad m] {f : α → β → β} {as : List α} :
+    as.scanrM (m := m) (pure <| f · · ) init = pure (as.scanr f init) := by
+  simp only [scanrM_eq_scanlM_reverse]
+  unfold flip
+  simp only [scanlM_pure, map_pure, scanr,  scanrM_eq_scanlM_reverse]
+  rfl
+
+theorem idRun_scanlM {f : β → α → Id β} {as : List α} :
+    (as.scanlM f init).run = as.scanl (f · · |>.run) init :=
+  scanlM_pure
+
+theorem idRun_scanrM {f : α → β → Id β} {as : List α} :
+    (as.scanrM f init).run = as.scanr (f · · |>.run) init :=
+  scanrM_pure
+
+@[simp, grind =]
+theorem scanlM_map [Monad m] [LawfulMonad m]
+    {f : α₁ → α₂} {g: β → α₂ → m β} {as : List α₁} :
+    (as.map f).scanlM g init = as.scanlM (g · <| f ·) init := by
+  induction as generalizing g init with simp [*]
+
+@[simp, grind =]
+theorem scanrM_map [Monad m] [LawfulMonad m]
+    {f : α₁ → α₂} {g: α₂ → β → m β} {as : List α₁} :
+    (as.map f).scanrM g init = as.scanrM (fun a b => g (f a) b) init := by
+  simp only [← map_reverse, scanlM_map, scanrM_eq_scanlM_reverse]
+  rfl
+
+/-! ### `List.scanl` and `List.scanr` -/
+
+@[simp]
+theorem length_scanl {f : β → α → β} : (scanl f init as).length = as.length + 1 := by
+  induction as generalizing init <;> simp_all [scanl, pure, bind, Id.run]
+
+grind_pattern length_scanl => scanl f init as
+
+@[simp, grind =]
+theorem scanl_nil {f : β → α → β} : scanl f init [] = [init] := by simp [scanl]
+
+@[simp, grind =]
+theorem scanl_cons {f : β → α → β} : scanl f b (a :: l) = b :: scanl f (f b a) l := by
+  simp [scanl]
+
+theorem scanl_singleton {f : β → α → β} : scanl f b [a] = [b, f b a] := by simp
+
+@[simp]
+theorem scanl_ne_nil {f : β → α → β} : scanl f b l ≠ [] := by
+  cases l <;> simp
+
+-- This pattern can be removed after moving to a lean version containing
+-- https://github.com/leanprover/lean4/pull/11760
+local grind_pattern List.eq_nil_of_length_eq_zero => l.length where
+  guard l.length = 0
+
+@[simp]
+theorem scanl_iff_nil {f : β → α → β} (c : β) : scanl f b l = [c] ↔ c = b ∧ l = [] := by
+  cases l
+  · simp [eq_comm]
+  · simp
+
+@[simp, grind =]
+theorem getElem_scanl {f : α → β → α} (h : i < (scanl f a l).length) :
+    (scanl f a l)[i] = foldl f a (l.take i) := by
+  induction l generalizing a i
+  · simp
+  · cases i <;> simp [*]
+
+@[grind =]
+theorem getElem?_scanl {f : α → β → α} :
+    (scanl f a l)[i]? = if i ≤ l.length then some (foldl f a (l.take i)) else none := by
+  split
+  · rw [getElem?_pos _ _ (by simpa using Nat.lt_add_one_iff.mpr ‹_›), getElem_scanl]
+  · rw [getElem?_neg]
+    simpa only [length_scanl, Nat.lt_add_one_iff]
+
+@[grind _=_]
+theorem take_scanl {f : β → α → β} (init : β) (as : List α) (i : Nat) :
+    (scanl f init as).take (i + 1) = scanl f init (as.take i) := by
+  induction as generalizing init i
+  · simp
+  · cases i
+    · simp
+    · simp [*]
+
+theorem getElem?_scanl_zero {f : β → α → β} : (scanl f b l)[0]? = some b := by
+  simp
+
+theorem getElem_scanl_zero {f : β → α → β} : (scanl f b l)[0] = b := by
+  simp
+
+@[simp]
+theorem head_scanl {f : β → α → β} (h : scanl f b l ≠ []) : (scanl f b l).head h = b := by
+  simp [head_eq_getElem]
+
+@[simp]
+theorem head?_scanl {f : β → α → β} : (scanl f b l).head? = some b := by
+  simp [head?_eq_getElem?]
+
+theorem getLast_scanl {f : β → α → β} (h : scanl f b l ≠ []) :
+    (scanl f b l).getLast h = foldl f b l := by
+  simp [getLast_eq_getElem]
+
+theorem getLast?_scanl {f : β → α → β} : (scanl f b l).getLast? = some (foldl f b l) := by
+  simp [getLast?_eq_getElem?]
+
+@[grind =]
+theorem tail_scanl {f : β → α → β} (h : 0 < l.length) :
+    (scanl f b l).tail = scanl f (f b (l.head (ne_nil_of_length_pos h))) l.tail := by
+  induction l
+  · simp at h
+  · simp
+
+theorem getElem?_succ_scanl {f : β → α → β} :
+    (scanl f b l)[i + 1]? = (scanl f b l)[i]?.bind fun x => l[i]?.map fun y => f x y := by
+  simp only [getElem?_scanl, take_add_one]
+  split
+  · have : i < l.length := Nat.add_one_le_iff.mp ‹_›
+    have : i ≤ l.length := Nat.le_of_lt ‹_›
+    simp [*, - take_append_getElem]
+  · split
+    · apply Eq.symm
+      simpa using Nat.lt_add_one_iff.mp (Nat.not_le.mp ‹_›)
+    · simp
+
+theorem getElem_succ_scanl {f : β → α → β} (h : i + 1 < (scanl f b l).length) :
+    (scanl f b l)[i + 1] = f ((l.scanl f b)[i]'(Nat.lt_trans (Nat.lt_add_one _) h)) (l[i]'(by simpa using h)) := by
+  simp only [length_scanl, Nat.add_lt_add_iff_right] at h
+  simp [take_add_one, *, - take_append_getElem]
+
+@[grind =]
+theorem scanl_append {f : β → α → β} {l₁ l₂ : List α} :
+    scanl f b (l₁ ++ l₂) = scanl f b l₁ ++ (scanl f (foldl f b l₁) l₂).tail := by
+  induction l₁ generalizing b
+  case nil => cases l₂ <;> simp
+  case cons head tail ih => simp [ih]
+
+@[grind =]
+theorem scanl_map {f : β → γ → β} {g : α → γ} {as : List α} :
+    scanl f init (as.map g) = scanl (fun acc x => f acc (g x)) init as := by
+  induction as generalizing init with simp [*]
+
+theorem scanl_eq_scanr_reverse {f : β → α → β} :
+    scanl f init as = reverse (scanr (flip f) init as.reverse) := by
+  simp only [scanl, scanr, Id.run, scanrM_reverse, Functor.map, reverse_reverse]
+  rfl
+
+theorem scanr_eq_scanl_reverse  {f : α → β → β} :
+    scanr f init as = reverse (scanl (flip f) init as.reverse) := by
+  simp only [scanl_eq_scanr_reverse, reverse_reverse]
+  rfl
+
+@[simp, grind =]
+theorem scanl_reverse {f : β → α → β} {as : List α} :
+    scanl f init as.reverse = reverse (scanr (flip f) init as) := by
+  simp [scanr_eq_scanl_reverse]
+
+@[simp, grind =]
+theorem scanr_reverse {f : α → β → β} {as : List α} :
+    scanr f init as.reverse = reverse (scanl (flip f) init as) := by
+  simp [scanl_eq_scanr_reverse]
+
+@[simp, grind =]
+theorem scanr_nil {f : α → β → β} : scanr f init [] = [init] := by simp [scanr]
+
+@[simp, grind =]
+theorem scanr_cons {f : α → β → β} :
+    scanr f b (a :: l) = foldr f b (a :: l) :: scanr f b l := by
+  simp [scanr_eq_scanl_reverse, reverse_cons, scanl_append, flip, - scanl_reverse]
+
+@[simp]
+theorem scanr_ne_nil {f : α → β → β} : scanr f b l ≠ [] := by
+  simp [scanr_eq_scanl_reverse, - scanl_reverse]
+
+theorem scanr_singleton {f : α → β → β} : scanr f b [a] = [f a b, b] := by
+  simp
+
+@[simp]
+theorem length_scanr {f : α → β → β} {as : List α} :
+    length (scanr f init as) = as.length + 1 := by
+  simp [scanr_eq_scanl_reverse, - scanl_reverse]
+
+grind_pattern length_scanr => scanr f init as
+
+@[simp]
+theorem scanr_iff_nil {f : α → β → β} (c : β) : scanr f b l = [c] ↔ c = b ∧ l = [] := by
+  simp [scanr_eq_scanl_reverse, - scanl_reverse]
+
+@[grind =]
+theorem scanr_append {f : α → β → β} (l₁ l₂ : List α) :
+    scanr f b (l₁ ++ l₂) = (scanr f (foldr f b l₂) l₁) ++ (scanr f b l₂).tail := by
+  induction l₁ <;> induction l₂ <;> simp [*]
+
+@[simp]
+theorem head_scanr {f : α → β → β} (h : scanr f b l ≠ []) :
+    (scanr f b l).head h = foldr f b l := by
+  simp [scanr_eq_scanl_reverse, - scanl_reverse, getLast_scanl, flip]
+
+@[simp]
+theorem head?_scanr {f : β → α → β} : (scanl f b l).head? = some b := by
+  simp [head?_eq_getElem?]
+
+@[grind =]
+theorem getLast_scanr {f : α → β → β} (h : scanr f b l ≠ []) :
+    (scanr f b l).getLast h = b := by
+  simp [scanr_eq_scanl_reverse, - scanl_reverse]
+
+theorem getLast?_scanr {f : α → β → β} : (scanr f b l).getLast? = some b := by
+  simp [scanr_eq_scanl_reverse, - scanl_reverse]
+
+@[grind =]
+theorem tail_scanr {f : α → β → β} (h : 0 < l.length) :
+    (scanr f b l).tail = scanr f b l.tail := by
+  induction l with simp_all
+
+@[grind _=_]
+theorem drop_scanr {f : α → β → β} (h : i ≤ l.length) :
+    (scanr f b l).drop i = scanr f b (l.drop i) := by
+  induction i generalizing l
+  · simp
+  · rename_i i ih
+    rw [drop_add_one_eq_tail_drop (i := i), drop_add_one_eq_tail_drop (i := i), ih]
+    · rw [tail_scanr]
+      simpa [length_drop, Nat.lt_sub_iff_add_lt]
+    · exact Nat.le_of_lt (Nat.add_one_le_iff.mp ‹_›)
+
+@[simp, grind =]
+theorem getElem_scanr {f : α → β → β} (h : i < (scanr f b l).length) :
+    (scanr f b l)[i] = foldr f b (l.drop i) := by
+  induction l generalizing b i
+  · simp
+  · cases i <;> simp [*]
+
+@[grind =]
+theorem getElem?_scanr {f : α → β → β} :
+    (scanr f b l)[i]? = if i < l.length + 1 then some (foldr f b (l.drop i)) else none := by
+  split
+  · rw [getElem?_pos _ _ (by simpa), getElem_scanr]
+  · rename_i h
+    simpa [getElem?_neg, length_scanr] using h
+
+theorem getElem_scanr_zero {f : α → β → β} : (scanr f b l)[0] = foldr f b l := by
+  simp
+
+theorem getElem?_scanr_zero {f : α → β → β} : (scanr f b l)[0]? = some (foldr f b l) := by
+  simp
+
+theorem getElem?_scanr_of_lt {f : α → β → β} (h : i < l.length + 1) :
+    (scanr f b l)[i]? = some (foldr f b (l.drop i)) := by
+  simp [h]
+
+@[grind =]
+theorem scanr_map {f : α → β → β} {g : γ → α} (b : β) (l : List γ) :
+    scanr f b (l.map g) = scanr (fun x acc => f (g x) acc) b l := by
+  suffices ∀ l, foldr f b (l.map g) = foldr (fun x acc => f (g x) acc) b l from by
+    induction l generalizing b with simp [*]
+  intro l
+  induction l with simp [*]

From 03a8d0cac62c734670eba2b1274fb6c754944339 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Thu, 12 Feb 2026 11:02:08 +0100
Subject: [PATCH 02/10] cleanups

---
 src/Init/Data/List/Scan/Basic.lean  | 2 +-
 src/Init/Data/List/Scan/Lemmas.lean | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/List/Scan/Basic.lean b/src/Init/Data/List/Scan/Basic.lean
index 1a5dbd2421b9..2ee8b210895e 100644
--- a/src/Init/Data/List/Scan/Basic.lean
+++ b/src/Init/Data/List/Scan/Basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Chad Sharp
+Authors: Mario Carneiro, Chad Sharp
 -/
 module
 
diff --git a/src/Init/Data/List/Scan/Lemmas.lean b/src/Init/Data/List/Scan/Lemmas.lean
index 2c41fce8eb3e..257c42780abe 100644
--- a/src/Init/Data/List/Scan/Lemmas.lean
+++ b/src/Init/Data/List/Scan/Lemmas.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro, Chad Sharp
 -/
 module
 
@@ -12,7 +12,6 @@ import all Init.Data.List.Scan.Basic
 import Init.Data.List.TakeDrop
 import Init.Data.Option.Lemmas
 import Init.Data.Nat.Lemmas
--- public import Init
 
 public section
 

From f22febe8262ed752b37d808dafd1b8a285582a23 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Thu, 12 Feb 2026 12:15:06 +0100
Subject: [PATCH 03/10] help orphan

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

diff --git a/src/Init/Data/List.lean b/src/Init/Data/List.lean
index 97377630d473..8d8f4b862267 100644
--- a/src/Init/Data/List.lean
+++ b/src/Init/Data/List.lean
@@ -35,3 +35,4 @@ public import Init.Data.List.OfFn
 public import Init.Data.List.FinRange
 public import Init.Data.List.Lex
 public import Init.Data.List.Range
+public import Init.Data.List.Scan

From 0437d6d24ecd4771adc504805bb4e8a4a6b82e06 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Thu, 12 Feb 2026 13:43:50 +0100
Subject: [PATCH 04/10] poke


From dd97f4f336bd80945ce61ffc8b52b435bf9db184 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 13 Feb 2026 17:25:27 +0100
Subject: [PATCH 05/10] 'fix' grind lint test

---
 src/Lean/Elab/Tactic/Grind/LintExceptions.lean | 1 +
 tests/lean/run/grind_lint_list.lean            | 9 ++++++++-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/Grind/LintExceptions.lean b/src/Lean/Elab/Tactic/Grind/LintExceptions.lean
index 77e29528f937..e1a78c596ba6 100644
--- a/src/Lean/Elab/Tactic/Grind/LintExceptions.lean
+++ b/src/Lean/Elab/Tactic/Grind/LintExceptions.lean
@@ -21,6 +21,7 @@ import Lean.Elab.Tactic.Grind.Lint
 #grind_lint skip List.getLast_attachWith
 #grind_lint skip List.head_attachWith
 #grind_lint skip List.drop_append_length
+#grind_lint skip List.getLast_scanr
 #grind_lint skip Array.back_singleton
 #grind_lint skip Array.count_singleton
 #grind_lint skip Array.foldl_empty
diff --git a/tests/lean/run/grind_lint_list.lean b/tests/lean/run/grind_lint_list.lean
index d5193e6a5e91..06e0d4c0df0a 100644
--- a/tests/lean/run/grind_lint_list.lean
+++ b/tests/lean/run/grind_lint_list.lean
@@ -39,7 +39,14 @@ import Lean.Elab.Tactic.Grind.LintExceptions
 #guard_msgs in
 #grind_lint inspect (min := 25) List.drop_append_length
 
+-- `List.getLast_scanr` is a very reasonable lemma.
+-- However, given the signature of it, `foldl_append` gets
+-- triggered very frequently. This seems to be an independent
+-- problem, having nothing to do with `getLast_scanr`.
+#guard_msgs in
+#grind_lint inspect (min := 100) List.drop_append_length
+
 /-! Check List namespace: -/
 
 #guard_msgs in
-#grind_lint check (min := 20) in List
+#grind_lint check  (min := 20) in List

From c26f84aca7a4011135464ce399fb91b0e72e8997 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 17 Feb 2026 01:14:29 +0100
Subject: [PATCH 06/10] remove obsolete grind pattern

---
 src/Init/Data/List/Scan/Lemmas.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/Init/Data/List/Scan/Lemmas.lean b/src/Init/Data/List/Scan/Lemmas.lean
index 257c42780abe..5c03b09b5b6b 100644
--- a/src/Init/Data/List/Scan/Lemmas.lean
+++ b/src/Init/Data/List/Scan/Lemmas.lean
@@ -134,11 +134,6 @@ theorem scanl_singleton {f : β → α → β} : scanl f b [a] = [b, f b a] := b
 theorem scanl_ne_nil {f : β → α → β} : scanl f b l ≠ [] := by
   cases l <;> simp
 
--- This pattern can be removed after moving to a lean version containing
--- https://github.com/leanprover/lean4/pull/11760
-local grind_pattern List.eq_nil_of_length_eq_zero => l.length where
-  guard l.length = 0
-
 @[simp]
 theorem scanl_iff_nil {f : β → α → β} (c : β) : scanl f b l = [c] ↔ c = b ∧ l = [] := by
   cases l

From 5f46e9ec261cd924520b8b467bb5eb0c28ab3da0 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 17 Feb 2026 01:16:18 +0100
Subject: [PATCH 07/10] remove double whitespace

---
 tests/lean/run/grind_lint_list.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/grind_lint_list.lean b/tests/lean/run/grind_lint_list.lean
index 06e0d4c0df0a..b95814d5cb3d 100644
--- a/tests/lean/run/grind_lint_list.lean
+++ b/tests/lean/run/grind_lint_list.lean
@@ -49,4 +49,4 @@ import Lean.Elab.Tactic.Grind.LintExceptions
 /-! Check List namespace: -/
 
 #guard_msgs in
-#grind_lint check  (min := 20) in List
+#grind_lint check (min := 20) in List

From 7a7a228f0cda719d053093914a4fed49e521fb0b Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 17 Feb 2026 01:24:04 +0100
Subject: [PATCH 08/10] fix test

---
 tests/lean/run/grind_lint_list.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/grind_lint_list.lean b/tests/lean/run/grind_lint_list.lean
index b95814d5cb3d..e90ab2131123 100644
--- a/tests/lean/run/grind_lint_list.lean
+++ b/tests/lean/run/grind_lint_list.lean
@@ -44,7 +44,7 @@ import Lean.Elab.Tactic.Grind.LintExceptions
 -- triggered very frequently. This seems to be an independent
 -- problem, having nothing to do with `getLast_scanr`.
 #guard_msgs in
-#grind_lint inspect (min := 100) List.drop_append_length
+#grind_lint inspect (min := 100) List.getLast_scanr
 
 /-! Check List namespace: -/
 

From d2b95d6c38cef7340b79fc139104abd707d2a5ed Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 17 Feb 2026 01:34:52 +0100
Subject: [PATCH 09/10] fix head?_scanr

---
 src/Init/Data/List/Scan/Lemmas.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Init/Data/List/Scan/Lemmas.lean b/src/Init/Data/List/Scan/Lemmas.lean
index 5c03b09b5b6b..505b4b025a14 100644
--- a/src/Init/Data/List/Scan/Lemmas.lean
+++ b/src/Init/Data/List/Scan/Lemmas.lean
@@ -277,10 +277,6 @@ theorem head_scanr {f : α → β → β} (h : scanr f b l ≠ []) :
     (scanr f b l).head h = foldr f b l := by
   simp [scanr_eq_scanl_reverse, - scanl_reverse, getLast_scanl, flip]
 
-@[simp]
-theorem head?_scanr {f : β → α → β} : (scanl f b l).head? = some b := by
-  simp [head?_eq_getElem?]
-
 @[grind =]
 theorem getLast_scanr {f : α → β → β} (h : scanr f b l ≠ []) :
     (scanr f b l).getLast h = b := by
@@ -320,6 +316,10 @@ theorem getElem?_scanr {f : α → β → β} :
   · rename_i h
     simpa [getElem?_neg, length_scanr] using h
 
+@[simp]
+theorem head?_scanr {f : α → β → β} : (scanr f b l).head? = some (foldr f b l) := by
+  simp [head?_eq_getElem?]
+
 theorem getElem_scanr_zero {f : α → β → β} : (scanr f b l)[0] = foldr f b l := by
   simp
 

From 8d1e6fe6b5abab6d870b304af206dd930806b18e Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 18 Feb 2026 10:55:58 +0100
Subject: [PATCH 10/10] fix test

---
 tests/lean/run/grind_lint_list.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/grind_lint_list.lean b/tests/lean/run/grind_lint_list.lean
index e90ab2131123..37f0c99f9e4e 100644
--- a/tests/lean/run/grind_lint_list.lean
+++ b/tests/lean/run/grind_lint_list.lean
@@ -44,7 +44,7 @@ import Lean.Elab.Tactic.Grind.LintExceptions
 -- triggered very frequently. This seems to be an independent
 -- problem, having nothing to do with `getLast_scanr`.
 #guard_msgs in
-#grind_lint inspect (min := 100) List.getLast_scanr
+#grind_lint inspect (min := 100) (detailed := 100) List.getLast_scanr
 
 /-! Check List namespace: -/