diff --git a/Batteries/Data/Array.lean b/Batteries/Data/Array.lean
index 052d36d955..83e8902354 100644
--- a/Batteries/Data/Array.lean
+++ b/Batteries/Data/Array.lean
@@ -7,3 +7,4 @@ public import Batteries.Data.Array.Match
 public import Batteries.Data.Array.Merge
 public import Batteries.Data.Array.Monadic
 public import Batteries.Data.Array.Pairwise
+public import Batteries.Data.Array.Scan
diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean
index 24a17b2560..eb0f562362 100644
--- a/Batteries/Data/Array/Basic.lean
+++ b/Batteries/Data/Array/Basic.lean
@@ -136,11 +136,261 @@ This will perform the update destructively provided that `a` has a reference cou
 abbrev setN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : Array α :=
   a.set i x
 
+
+
+/--
+  This is guaranteed by the Array docs but it is unprovable.
+  May be asserted to be true in an unsafe context via `Array.unsafe_size_fits_usize
+-/
+private abbrev size_fits_usize {a : Array α}: Prop := a.size < USize.size
+
+@[grind .]
+private theorem nat_index_eq_usize_index {n : Nat} {a : Array α}
+    {h : a.size_fits_usize} {hn : n ≤ a.size}
+  : (USize.ofNat n).toNat = n
+  := USize.toNat_ofNat_of_lt' (Nat.lt_of_le_of_lt ‹_› ‹_›)
+
+
+/--
+  This is guaranteed by the Array docs but it is unprovable.
+  Can be used in unsafe functions to write more efficient implementations
+  that avoid boxed integer arithmetic.
+-/
+private unsafe def unsafe_size_fits_usize {a: Array α} : Array.size_fits_usize (a := a) :=
+  lcProof
+
+
+@[inline]
+private def scanlMFast [Monad m] (f : β → α → m β) (init : β) (as : Array α)
+    (start := 0) (stop := as.size) : m (Array β) :=
+  let stop := min stop as.size
+  let start := min start as.size
+
+  loop f init as
+    (start := USize.ofNat start) (stop := USize.ofNat stop)
+    (h_stop := by grind only [USize.size_eq, USize.ofNat_eq_iff_mod_eq_toNat, = Nat.min_def])
+    (acc := Array.mkEmpty <| stop - start + 1)
+where
+  @[specialize]
+  loop (f : β → α → m β) (init: β) (as: Array α) (start stop : USize)
+       (h_stop : stop.toNat ≤ as.size) (acc : Array β) : m (Array β) := do
+    if h_lt: start < stop then
+      let next ← f init (as.uget start <| Nat.lt_of_lt_of_le h_lt h_stop)
+      loop f next as (start + 1) stop h_stop (acc.push init)
+    else
+      pure <| acc.push init
+  termination_by stop.toNat - min start.toNat stop.toNat
+  decreasing_by
+      have : start < (start + 1) := by grind only [USize.size_eq]
+      grind only [Nat.min_def, USize.lt_iff_toNat_lt]
+
+
+/--
+Fold an effectful function `f` over the array from the left, returning the list of partial results.
+-/
+@[implemented_by scanlMFast]
+def scanlM [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start := 0)
+  (stop := as.size) : m (Array β) :=
+  loop f init as (min start as.size) (min stop as.size) (Nat.min_le_right _ _) #[]
+where
+  /-- auxiliary tail-recursive function for scanlM -/
+  loop (f : β → α → m β) (init : β ) (as : Array α) (start stop : Nat)
+       (h_stop : stop ≤ as.size) (acc : Array β) : m (Array β) := do
+    if h_lt : start < stop then
+      loop f (← f init as[start]) as (start + 1) stop h_stop (acc.push init)
+    else
+      pure <| acc.push init
+
+private theorem scanlM_loop_eq_scanlMFast_loop [Monad m]
+    {f : β → α → m β} {init : β} {as : Array α} {h_size : as.size_fits_usize}
+    {start stop : Nat} {h_start : start ≤ as.size}
+    {h_stop : stop ≤ as.size} {acc : Array β} :
+    scanlM.loop f init as start stop h_stop acc
+      = scanlMFast.loop f init as (USize.ofNat start) (USize.ofNat stop)
+      (by rw [USize.toNat_ofNat_of_lt' (Nat.lt_of_le_of_lt h_stop h_size)]; exact h_stop) acc := by
+
+  generalize h_n : stop - start = n
+  induction n using Nat.strongRecOn generalizing start acc init
+  rename_i n ih
+  rw [scanlM.loop, scanlMFast.loop]
+  have h_stop_usize := nat_index_eq_usize_index (h := h_size) (hn := h_stop)
+  have h_start_usize := nat_index_eq_usize_index (h := h_size) (hn := h_start)
+  split
+  case isTrue h_lt =>
+    simp_all only [USize.toNat_ofNat', ↓reduceDIte, uget,
+      show USize.ofNat start < USize.ofNat stop by simp_all [USize.lt_iff_toNat_lt]]
+    apply bind_congr
+    intro next
+    have h_start_succ : USize.ofNat start + 1 = USize.ofNat (start + 1) := by
+      simp_all only [← USize.toNat_inj, USize.toNat_add]
+      grind only [USize.size_eq, nat_index_eq_usize_index]
+    rw [h_start_succ]
+    apply ih (stop - (start + 1)) <;> omega
+  case isFalse h_nlt => grind [USize.lt_iff_toNat_lt]
+
+-- this theorem establishes that given the (unprovable) assumption that as.size < USize.size,
+-- the scanlMFast and scanlM are equivalent
+private theorem scanlM_eq_scanlMFast [Monad m]
+    {f : β → α → m β} {init : β} {as : Array α}
+    {h_size : as.size_fits_usize}
+    {start stop : Nat}
+  : scanlM f init as start stop = scanlMFast f init as start stop
+  := by
+    unfold scanlM scanlMFast
+    apply scanlM_loop_eq_scanlMFast_loop
+    simp_all only [gt_iff_lt]
+    apply Nat.min_le_right
+
+
+@[inline]
+private def scanrMFast [Monad m] (f : α → β → m β) (init : β) (as : Array α)
+    (h_size : as.size_fits_usize) (start := as.size) (stop := 0) : m (Array β) :=
+  let start := min start as.size
+  let stop := min stop start
+
+  loop f init as
+    (start := USize.ofNat start) (stop := USize.ofNat stop)
+    (h_start := by grind only [USize.size_eq, USize.ofNat_eq_iff_mod_eq_toNat, = Nat.min_def])
+    (acc := Array.replicate (start - stop + 1) init)
+    (by grind only [!Array.size_replicate, = Nat.min_def, Array.nat_index_eq_usize_index])
+where
+  @[specialize]
+  loop (f : α → β → m β) (init : β) (as : Array α)
+       (start stop : USize)
+       (h_start : start.toNat ≤ as.size)
+       (acc : Array β)
+       (h_bound : start.toNat - stop.toNat  < acc.size)
+     : m (Array β) := do
+    if h_gt : stop < start then
+      let startM1 := start - 1
+      have : startM1 < start := by grind only [!USize.sub_add_cancel, USize.lt_iff_le_and_ne,
+        USize.lt_add_one, USize.le_zero_iff]
+      have : startM1.toNat < as.size := Nat.lt_of_lt_of_le ‹_› ‹_›
+      have : (startM1 - stop) < (start - stop) := by grind only
+        [!USize.sub_add_cancel, USize.sub_right_inj, USize.add_comm, USize.lt_add_one,
+          USize.add_assoc, USize.add_right_inj]
+
+      let next ← f (as.uget startM1 ‹_›) init
+      loop f next as
+        (start := startM1)
+        (stop := stop)
+        (h_start := Nat.le_of_succ_le_succ (Nat.le_succ_of_le ‹_›))
+        (acc := acc.uset (startM1 - stop) next
+          (by grind only [USize.toNat_sub_of_le, USize.le_of_lt, USize.lt_iff_toNat_lt]))
+        (h_bound :=
+          (by grind only [USize.toNat_sub_of_le, = uset_eq_set, = size_set, USize.size_eq]))
+    else
+      pure acc
+  termination_by start.toNat - stop.toNat
+  decreasing_by
+    grind only [USize.lt_iff_toNat_lt, USize.toNat_sub,
+      USize.toNat_sub_of_le, USize.le_iff_toNat_le]
+
+
+@[inline]
+private unsafe def scanrMUnsafe [Monad m] (f : α → β → m β) (init : β) (as : Array α)
+    (start := as.size) (stop := 0) : m (Array β) :=
+  scanrMFast (h_size := Array.unsafe_size_fits_usize) f init as (start := start) (stop := stop)
+
+/--
+Folds a monadic function over a list from the left, accumulating the partial results starting with
+`init`. The accumulated value is combined with the each element of the list in order, using `f`.
+
+The optional parameters `start` and `stop` control the region of the array to be folded. Folding
+proceeds from `start` (inclusive) to `stop` (exclusive), so no folding occurs unless `start < stop`.
+By default, the entire array is folded.
+
+Examples:
+```lean example
+example [Monad m] (f : α → β → m α) :
+    Array.scanlM (m := m) f x₀ #[a, b, c] = (do
+      let x₁ ← f x₀ a
+      let x₂ ← f x₁ b
+      let x₃ ← f x₂ c
+      pure #[x₀, x₁, x₂, x₃])
+  := by rfl
+```
+
+```lean example
+example [Monad m] (f : α → β → m α) :
+    Array.scanlM (m := m) f x₀ #[a, b, c] (start := 1) = (do
+      let x₁ ← f x₀ b
+      let x₂ ← f x₁ c
+      pure #[x₀, x₁, x₂])
+  := by rfl
+-/
+@[implemented_by scanrMUnsafe]
+def scanrM [Monad m]
+    (f : α → β → m β) (init : β) (as : Array α) (start := as.size) (stop := 0) : m (Array β) :=
+  let start := min start as.size
+  loop f init as start stop (Nat.min_le_right _ _) #[]
+where
+  /-- auxiliary tail-recursive function for scanrM -/
+  loop (f : α → β → m β) (init : β) (as : Array α)
+       (start stop : Nat)
+       (h_start : start ≤ as.size)
+       (acc : Array β)
+     : m (Array β) := do
+    if h_gt : stop < start then
+      let i := start - 1
+      let next ← f as[i] init
+      loop f next as i stop (by omega) (acc.push init)
+    else
+      pure <| acc.push init |>.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 : Array α) (start := 0) (stop := as.size) : Array β :=
+  Id.run <| as.scanlM (pure <| f · ·) init start stop
+
+/--
+
+Fold a function `f` over the list from the right, returning the list of partial results.
+```
+scanl (+) 0 #[1, 2, 3] = #[0, 1, 3, 6]
+```
+-/
+@[inline]
+def scanr (f : α → β → β) (init : β) (as : Array α) (start := as.size) (stop := 0) : Array β :=
+  Id.run <| as.scanrM (pure <| f · ·) init start stop
+
 end Array
 
 
 namespace Subarray
 
+/--
+Fold an effectful function `f` over the array from the left, returning the list of partial results.
+-/
+@[inline]
+def scanlM [Monad m] (f : β → α → m β) (init : β) (as : Subarray α) : m (Array β) :=
+  as.array.scanlM f init (start := as.start) (stop := as.stop)
+
+/--
+Fold an effectful function `f` over the array from the right, returning the list of partial results.
+-/
+@[inline]
+def scanrM [Monad m] (f : α → β → m β) (init : β) (as : Subarray α) : m (Array β) :=
+  as.array.scanrM f init (start := as.start) (stop := as.stop)
+
+/--
+Fold a pure function `f` over the array from the left, returning the list of partial results.
+-/
+@[inline]
+def scanl (f : β → α → β) (init : β) (as : Subarray α): Array β :=
+  as.array.scanl f init (start := as.start) (stop := as.stop)
+
+/--
+Fold a pure function `f` over the array from the left, returning the list of partial results.
+-/
+def scanr (f : α → β → β) (init : β) (as : Subarray α): Array β :=
+  as.array.scanr f init (start := as.start) (stop := as.stop)
+
 /--
 Check whether a subarray is empty.
 -/
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index e65879bcb6..0e1e5eb3f9 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -41,6 +41,10 @@ theorem idxOf?_toList [BEq α] {a : α} {l : Array α} :
     (a.eraseIdxIfInBounds i).size = if i < a.size then a.size-1 else a.size := by
   grind
 
+theorem toList_drop {as: Array α} {n : Nat}
+  : (as.drop n).toList = as.toList.drop n
+  := by simp only [drop, toList_extract, size_eq_length_toList, List.drop_eq_extract]
+
 /-! ### set -/
 
 theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by simp
diff --git a/Batteries/Data/Array/Scan.lean b/Batteries/Data/Array/Scan.lean
new file mode 100644
index 0000000000..176d5d13e1
--- /dev/null
+++ b/Batteries/Data/Array/Scan.lean
@@ -0,0 +1,374 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chad Sharp
+-/
+module
+
+public import Batteries.Data.Array.Basic
+public import Batteries.Data.Array.Lemmas
+import Batteries.Data.List.Scan
+
+public section
+
+/-!
+# Array
+
+Prove basic results about `Array.scanl`, `Array.scanr`, `Array.scanlM` and `Array.scanrM`.
+-/
+
+
+namespace Array
+
+theorem scanlM_loop_toList [Monad m] [LawfulMonad m]
+    {f : β → α → m β} {stop : Nat} (h : stop ≤ as.size)
+    : scanlM.loop f init as start stop h acc
+      = return acc.toList
+               ++ (← as.toList.drop start
+                  |>.take (stop - start)
+                  |>.scanlM f init)
+               |>.toArray := by
+  induction h_ind : stop - start generalizing start acc init with
+    | zero =>
+      unfold scanlM.loop
+      simp [show ¬(start < stop) by omega, ← Array.toList_push]
+    | succ n ih =>
+      unfold scanlM.loop
+      rw [List.drop_eq_getElem_cons (by simp; omega)]
+      simp [ show start < stop by omega
+           , show stop - (start + 1) = n by omega
+           , ih
+           ]
+
+theorem scanlM_toList [Monad m] [LawfulMonad m] {f : β → α → m β} {as : Array α} :
+    List.toArray <$> as.toList.scanlM f init = as.scanlM f init := by
+  unfold scanlM
+  simp [Array.scanlM_loop_toList, ←Array.length_toList]
+
+
+@[simp, grind =]
+theorem toList_scanlM [Monad m] [LawfulMonad m] {f : β → α → m β} {as : Array α} :
+    toList <$> as.scanlM f init = as.toList.scanlM f init := by
+  rw [← scanlM_toList]
+  simp
+
+
+-- TODO: come back and simplify this proof? And/or simplify the structure of Arrat.scacnrM to make
+-- it more amenable
+theorem scanrM_loop_toList [Monad m] [LawfulMonad m] {f : α → β → m β}
+    {start : Nat} {h : start ≤ as.size}
+    : scanrM.loop f init as start stop h acc
+      = return (← as.toList.drop stop
+                  |>.take (start - stop)
+                  |>.scanrM f init)
+                ++ acc.toList.reverse
+                |>.toArray := by
+  induction h_ind : start - stop generalizing stop acc init start with
+    | zero =>
+      grind [scanrM.loop, append_eq_toArray_iff, toList_reverse]
+    | succ n ih =>
+      unfold scanrM.loop
+      simp_all only [bind_pure_comp, show stop < start by omega, ↓reduceDIte]
+
+      conv =>
+        lhs
+        arg 2
+        ext a
+        rw [ih (start := start - 1) (stop := stop) (acc := acc.push init) (by omega)]
+
+
+      have h_list : List.take (n + 1) (List.drop stop as.toList)
+        = as[stop] :: List.take n (List.drop (stop + 1) as.toList)
+        := by
+          rw [List.drop_eq_getElem_cons (by simp; omega)]
+          simp
+
+      have h_rev_list : (List.take (n + 1) (List.drop stop as.toList)).reverse
+        = as[start - 1] :: (List.take n (List.drop stop as.toList)).reverse
+        := by
+          have h_eq : start - 1 = stop + n := by omega
+          rw [← List.take_append_getElem
+            (by simp; omega : n < (List.drop stop as.toList).length)]
+          simp [List.reverse_append, List.getElem_drop, h_eq]
+
+      simp_all only [Array.toList_push, List.reverse_append, List.reverse_cons,
+        Functor.map_map , List.scanrM_eq_scanlM_reverse]
+      simp_all [flip]
+
+
+theorem scanrM_toList [Monad m] [LawfulMonad m] {f : α → β → m β} {as : Array α} :
+    List.toArray <$> as.toList.scanrM f init = as.scanrM f init := by
+  unfold scanrM
+  simp [Array.scanrM_loop_toList, ← Array.length_toList]
+
+
+@[simp, grind =]
+theorem toList_scanrM [Monad m] [LawfulMonad m] {f : α → β → m β} {as : Array α} :
+    toList <$> as.scanrM f init = as.toList.scanrM f init := by
+  rw [← scanrM_toList]
+  simp
+
+-- In principle this likely could be rewritten without LawfulMonad, it's just that
+-- it is easiest to prove using scanlM_loop_toList
+theorem scanlM_extract [Monad m] [LawfulMonad m] {f : β → α → m β} {as : Array α} :
+    as.scanlM f init start stop = (as.extract start stop).scanlM f init := by
+  rw (occs := [1]) [scanlM]
+  rw [scanlM_loop_toList, ← scanlM_toList, bind_pure_comp]
+  simp_all [← length_toList]
+  grind [List.take_eq_take_iff, List.drop_eq_drop_iff]
+
+
+-- TODO: rewrite without requiring LawfulMonad?
+-- In principle it probably shouldn't require it its just that scanlM_loop_toList does
+theorem scanrM_extract [Monad m] [LawfulMonad m] {f : α → β → m β} {as : Array α} :
+    as.scanrM f init start stop = (as.extract stop start).scanrM f init := by
+  rw (occs := [1]) [scanrM]
+  rw [scanrM_loop_toList, ← scanrM_toList, bind_pure_comp]
+  grind [List.take_eq_take_iff, toList_extract]
+
+@[simp, grind =]
+theorem scanlM_empty [Monad m] {f : β → α → m β} {start stop : Nat} :
+    #[].scanlM f init start stop = pure #[init] := by
+  simp [scanlM, scanlM.loop]
+
+@[grind =]
+theorem scanrM_empty [Monad m] {f : α → β → m β} {start stop : Nat} :
+    #[].scanrM f init start stop = pure #[init] := by
+  simp [scanrM, scanrM.loop]
+
+theorem scanlM_reverse [Monad m] [LawfulMonad m] {f : β → α → m β} {as : Array α} :
+    as.reverse.scanlM f init = Array.reverse <$> (as.scanrM (flip f) init) := by
+  rw [← scanlM_toList, ← scanrM_toList]
+  simp
+
+@[simp]
+theorem scanlM_pure [Monad m] [LawfulMonad m] {f : β → α → β} {as : Array α} :
+    as.scanlM (m := m) (pure <| f · ·) init = pure (as.scanl f init) := by
+  unfold scanl
+  rw [← scanlM_toList, ← scanlM_toList, List.scanlM_pure]
+  simp only [map_pure, Id.run_map]
+  rfl
+
+@[simp]
+theorem scanrM_pure [Monad m] [LawfulMonad m] {f : α → β → β} {as : Array α} :
+    as.scanrM (m := m) (pure <| f · ·) init = pure (as.scanr f init) := by
+  unfold scanr
+  rw [← scanrM_toList, ← scanrM_toList, List.scanrM_pure]
+  simp only [map_pure, Id.run_map]
+  rfl
+
+theorem idRun_scanlM {f : β → α → Id β} {as : Array α} :
+    (as.scanlM f init).run = as.scanl (f · · |>.run) init :=
+  scanlM_pure
+
+theorem idRun_scanrM {f : α → β → Id β} {as : Array α} :
+    (as.scanrM f init).run = as.scanr (f · · |>.run) init :=
+  scanrM_pure
+
+@[grind =]
+theorem scanlM_map [Monad m] [LawfulMonad m] {f : α₁ → α₂ } {g: β → α₂ → m β} {as : Array α₁} :
+    (as.map f).scanlM g init = as.scanlM (g · <| f ·) init := by
+  repeat rw [← scanlM_toList]
+  simp
+
+@[grind =]
+theorem scanrM_map [Monad m] [LawfulMonad m] {f : α₁ → α₂ } {g: α₂ → β → m β} {as : Array α₁} :
+    (as.map f).scanrM g init = as.scanrM (fun a b => g (f a) b) init := by
+  repeat rw [← scanrM_toList]
+  simp
+
+
+/-- ### Array.scanl -/
+
+theorem scanl_eq_scanlM {f : β → α → β} {as: Array α} :
+    as.scanl f init = (as.scanlM (m := Id) (pure <| f · ·) init).run := by
+  simp
+
+theorem scanl_toList {f: β → α → β} {as : Array α} :
+    (as.toList.scanl f init).toArray = as.scanl f init := by
+  rw [scanl_eq_scanlM, ← scanlM_toList]
+  simp [Id.run_map, pure, List.scanl]
+
+
+@[simp, grind =]
+theorem toList_scanl {f : β → α → β} {as: Array α} :
+    (as.scanl f init).toList = as.toList.scanl f init := by
+  rw [← scanl_toList]
+
+@[simp]
+theorem size_scanl {f : β → α → β} (init : β) (as : Array α) :
+    size (scanl f init as) = as.size + 1 := by
+  grind [size_eq_length_toList]
+
+grind_pattern size_scanl => scanl f init as
+
+@[grind =]
+theorem scanl_empty {f : β → α → β} (init : β) :
+    scanl f init #[] = #[init] := by
+  apply toList_inj.mp
+  grind
+
+@[grind =]
+theorem scanl_singleton {f : β → α → β} :
+    scanl f init #[a] = #[init, f init a] := by
+  apply toList_inj.mp
+  grind
+
+@[simp]
+theorem scanl_ne_empty {f : β → α → β} : scanl f init as ≠ #[] := by grind
+
+-- This pattern can be removed after moving to a lean version containing
+-- https://github.com/leanprover/lean4/pull/11760
+local grind_pattern Array.eq_empty_of_size_eq_zero => xs.size where
+  guard xs.size = 0
+
+@[simp]
+theorem scanl_iff_empty {f : β → α → β} (c : β) :
+    scanl f init as = #[c] ↔ c = init ∧ as = #[] := by
+  grind
+
+@[simp, grind =]
+theorem getElem_scanl {f : β → α → β} {as: Array α} (h : i < (as.scanl f init).size) :
+    (as.scanl f init)[i]'h = foldl f init (as.take i) := by
+  simp only [←foldl_toList, ←scanl_toList]
+  simp
+
+@[grind =]
+theorem getElem?_scanl {f : β → α → β} :
+    (scanl f a l)[i]? = if i ≤ l.size then some (foldl f a (l.take i)) else none := by
+  grind
+
+
+@[grind _=_]
+theorem take_scanl {f : β → α → β} (init : β) (as : Array α) :
+    (scanl f init as).take (i + 1) = scanl f init (as.take i) := by
+  grind
+
+theorem getElem?_scanl_zero {f : β → α → β} : (scanl f init as)[0]? = some init := by simp
+
+theorem getElem_scanl_zero {f : β → α → β} : (scanl f init as)[0] = init := by simp
+
+theorem getElem?_succ_scanl {f : β → α → β} :
+    (scanl f init as)[i + 1]? = (scanl f init as)[i]?.bind fun x => as[i]?.map fun y => f x y := by
+  simp [← scanl_toList, List.getElem?_succ_scanl]
+
+theorem getElem_succ_scanl {f : β → α → β} (h : i + 1 < (scanl f b as).size) :
+    (as.scanl f b)[i + 1] = f (as.scanl f b)[i] (as[i]'(by grind)) := by
+  simp only [← scanl_toList, List.getElem_toArray, List.getElem_succ_scanl]
+  simp
+
+@[grind =]
+theorem scanl_push {f : β → α → β} {init: β} {a : α} {as : Array α} :
+    (as.push a).scanl f init = (as.scanl f init).push (f (as.foldl f init) a) := by
+  repeat rw [← scanl_toList]
+  simp [List.scanl_append]
+
+@[grind =]
+theorem scanl_map {f : γ → β → γ} {g : α → β} (init : γ) (as : Array α) :
+    scanl f init (as.map g) = scanl (f · <| g ·) init as := by
+  repeat rw [← scanl_toList]
+  simp [List.scanl_map]
+
+@[simp, grind =]
+theorem back_scanl {f : β → α → β} {as : Array α} :
+    (as.scanl f init).back = as.foldl f init := by
+  simp [Array.back_eq_getElem]
+
+theorem back_scanl? {f : β → α → β} {as : Array α} :
+    (as.scanl f init).back? = some (as.foldl f init) := by
+  simp [Array.back?_eq_getElem?]
+
+/-! ### Array.scanr -/
+
+theorem scanr_eq_scanrM {f : α → β → β} {as : Array α} :
+    as.scanr f init = (as.scanrM (m := Id) (pure <| f · ·) init).run := by
+  simp
+
+theorem scanr_toList {f : α → β → β} {as : Array α} :
+    (as.toList.scanr f init).toArray = as.scanr f init := by
+  rw [scanr_eq_scanrM, ← scanrM_toList]
+  simp [Id.run_map, pure, List.scanr]
+
+@[simp, grind =]
+theorem toList_scanr {f : α → β → β} {as : Array α} :
+    (as.scanr f init).toList = as.toList.scanr f init := by
+  rw [← scanr_toList]
+
+@[simp]
+theorem size_scanr {f : α → β → β} (init : β) (as : Array α) :
+    size (as.scanr f init) = as.size + 1 := by
+  grind [size_eq_length_toList]
+
+grind_pattern size_scanr => scanr f init as
+
+@[grind =]
+theorem scanr_empty {f : α → β → β} {init: β} :
+    #[].scanr f init = #[init] := by
+  apply toList_inj.mp
+  grind
+
+@[simp]
+theorem scanr_ne_empty {f : α → β → β} {as : Array α} :
+    as.scanr f init ≠ #[] := by
+  grind
+
+@[grind =]
+theorem scanr_push {f : α → β → β} {as : Array α} :
+    (as.push a).scanr f init = (as.scanr f (f a init)).push init := by
+  apply toList_inj.mp
+  grind
+
+@[simp, grind =]
+theorem back_scanr {f : α → β → β} {as : Array α} : (as.scanr f init).back = init := by
+  simp [←getLast_toList, List.getLast_scanr]
+
+theorem back?_scanr {f : α → β → β} {as : Array α} :
+    (as.scanr f init).back? = some init := by
+  simp [←getLast?_toList, List.getLast?_scanr]
+
+@[simp, grind =]
+theorem getElem_scanr {f : α → β → β} (h : i < (scanr f b l).size) :
+    (scanr f b l)[i] = foldr f b (l.drop i) := by
+  simp only [← foldr_toList, ← scanr_toList, ←getElem_toList, List.getElem_scanr, toList_drop]
+
+@[grind =]
+theorem getElem?_scanr {f : α → β → β} :
+    (scanr f b as)[i]? = if i < as.size + 1 then some (foldr f b (as.drop i)) else none := by
+  simp only [← foldr_toList, ← scanr_toList, List.getElem?_toArray, toList_drop]
+  simp only [← length_toList, List.getElem?_scanr]
+
+theorem getElem_scanr_zero {f : α → β → β} :
+    (scanr f init as)[0] = as.foldr f init := by
+  simp
+
+theorem getElem?_scanr_zero {f : α → β → β} :
+    (scanr f init as)[0]? = some (as.foldr f init ) := by
+  simp
+
+@[grind =]
+theorem scanr_map {f : β → γ → γ} {g : α → β} (init : γ) (as : Array α) :
+    scanr f init (as.map g) = scanr (fun x acc => f (g x) acc) init as := by
+  repeat rw [← scanr_toList]
+  simp [List.scanr_map]
+
+@[grind =]
+theorem scanl_reverse {f : β → α → β} {as : Array α} :
+    scanl f init as.reverse = reverse (scanr (flip f) init as) := by
+  apply toList_inj.mp
+  simp only [← scanl_toList, ← scanr_toList]
+  simp
+
+ end Array
+
+namespace Subarray
+theorem scanlM_extract [Monad m] [LawfulMonad m] {f : β → α → m β} {as : Subarray α} :
+    as.scanlM f init = (as.array.extract as.start as.stop).scanlM f init := by
+  unfold scanlM
+  apply Array.scanlM_extract
+
+theorem scanrM_extract [Monad m] [LawfulMonad m] {f : α → β → m β} {as : Subarray α} :
+    as.scanrM f init = (as.array.extract as.stop as.start).scanrM f init := by
+  unfold scanrM
+  apply Array.scanrM_extract
+end Subarray
+
diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index 9bb24219af..052239ad75 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 
 module
 public import Batteries.Tactic.Alias
-
+public import Batteries.Tactic.Lint.Misc
 @[expose] public section
 
 namespace List
diff --git a/Batteries/Data/List/Scan.lean b/Batteries/Data/List/Scan.lean
index 0f4eb57e3f..35cf7bc493 100644
--- a/Batteries/Data/List/Scan.lean
+++ b/Batteries/Data/List/Scan.lean
@@ -10,6 +10,7 @@ public import Batteries.Data.List.Lemmas
 
 @[expose] public section
 
+
 /-!
 # List scan