diff --git a/RELEASES.md b/RELEASES.md
index b1e5936d15..851028fbd8 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -99,6 +99,10 @@ v4.8.0 (development in progress)
   and `#guard_msgs (ordering := sorted) in cmd` sorts the messages in lexicographic order before checking.
   PR [#3883](https://github.com/leanprover/lean4/pull/3883).
 
+* The `#guard_msgs` command now supports showing a diff between the expected and actual outputs. This feature is currently
+  disabled by default, but can be enabled with `set_option guard_msgs.diff true`. Depending on user feedback, this option
+  may default to `true` in a future version of Lean.
+
 Breaking changes:
 
 * Automatically generated equational theorems are now named using suffix `.eq_<idx>` instead of `._eq_<idx>`, and `.def` instead of `._unfold`. Example:
diff --git a/src/Init/Data.lean b/src/Init/Data.lean
index f6befdfc50..f6da558757 100644
--- a/src/Init/Data.lean
+++ b/src/Init/Data.lean
@@ -14,6 +14,7 @@ import Init.Data.String
 import Init.Data.List
 import Init.Data.Int
 import Init.Data.Array
+import Init.Data.Array.Subarray.Split
 import Init.Data.ByteArray
 import Init.Data.FloatArray
 import Init.Data.Fin
diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index b57d8eaace..682fbb204b 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -29,6 +29,12 @@ namespace Subarray
 def size (s : Subarray α) : Nat :=
   s.stop - s.start
 
+theorem size_le_array_size {s : Subarray α} : s.size ≤ s.array.size := by
+  let {array, start, stop, start_le_stop, stop_le_array_size} := s
+  simp [size]
+  apply Nat.le_trans (Nat.sub_le stop start)
+  assumption
+
 def get (s : Subarray α) (i : Fin s.size) : α :=
   have : s.start + i.val < s.array.size := by
    apply Nat.lt_of_lt_of_le _ s.stop_le_array_size
diff --git a/src/Init/Data/Array/Subarray/Split.lean b/src/Init/Data/Array/Subarray/Split.lean
new file mode 100644
index 0000000000..a3c7a2aac1
--- /dev/null
+++ b/src/Init/Data/Array/Subarray/Split.lean
@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+
+prelude
+import Init.Data.Array.Basic
+import Init.Data.Array.Subarray
+import Init.Omega
+
+/-
+This module contains splitting operations on subarrays that crucially rely on `omega` for proof
+automation. Placing them in another module breaks an import cycle, because `omega` itself uses the
+array library.
+-/
+
+namespace Subarray
+/--
+Splits a subarray into two parts.
+-/
+def split (s : Subarray α) (i : Fin s.size.succ) : (Subarray α × Subarray α) :=
+  let ⟨i', isLt⟩ := i
+  have := s.start_le_stop
+  have := s.stop_le_array_size
+  have : i' ≤ s.stop - s.start := Nat.lt_succ.mp isLt
+  have : s.start + i' ≤ s.stop := by omega
+  have : s.start + i' ≤ s.array.size := by omega
+  have : s.start + i' ≤ s.stop := by
+    simp only [size] at isLt
+    omega
+  let pre := {s with
+    stop := s.start + i',
+    start_le_stop := by omega,
+    stop_le_array_size := by assumption
+  }
+  let post := {s with
+    start := s.start + i'
+    start_le_stop := by assumption
+  }
+  (pre, post)
+
+/--
+Removes the first `i` elements of the subarray. If there are `i` or fewer elements, the resulting
+subarray is empty.
+-/
+def drop (arr : Subarray α) (i : Nat) : Subarray α where
+  array := arr.array
+  start := min (arr.start + i) arr.stop
+  stop := arr.stop
+  start_le_stop := by
+    rw [Nat.min_def]
+    split <;> simp only [Nat.le_refl, *]
+  stop_le_array_size := arr.stop_le_array_size
+
+/--
+Keeps only the first `i` elements of the subarray. If there are `i` or fewer elements, the resulting
+subarray is empty.
+-/
+def take (arr : Subarray α) (i : Nat) : Subarray α where
+  array := arr.array
+  start := arr.start
+  stop := min (arr.start + i) arr.stop
+  start_le_stop := by
+    have := arr.start_le_stop
+    rw [Nat.min_def]
+    split <;> omega
+  stop_le_array_size := by
+    have := arr.stop_le_array_size
+    rw [Nat.min_def]
+    split <;> omega
diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean
index ddb84a2921..9a0017f23c 100644
--- a/src/Lean/Elab/GuardMsgs.lean
+++ b/src/Lean/Elab/GuardMsgs.lean
@@ -5,6 +5,7 @@ Authors: Kyle Miller
 -/
 prelude
 import Lean.Elab.Notation
+import Lean.Util.Diff
 import Lean.Server.CodeActions.Attr
 
 /-! `#guard_msgs` command for testing commands
@@ -15,6 +16,12 @@ See the docstring on the `#guard_msgs` command.
 
 open Lean Parser.Tactic Elab Command
 
+register_builtin_option guard_msgs.diff : Bool := {
+  defValue := false
+  descr := "When true, show a diff between expected and actual messages if they don't match. "
+}
+
+
 namespace Lean.Elab.Tactic.GuardMsgs
 
 /-- Gives a string representation of a message without source position information.
@@ -151,7 +158,12 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
     else
       -- Failed. Put all the messages back on the message log and add an error
       modify fun st => { st with messages := initMsgs ++ msgs }
-      logErrorAt tk m!"❌ Docstring on `#guard_msgs` does not match generated message:\n\n{res}"
+      let feedback :=
+        if (← getOptions).getBool `guard_msgs.diff false then
+          let diff := Diff.diff (expected.split (· == '\n')).toArray (res.split (· == '\n')).toArray
+          Diff.linesToString diff
+        else res
+      logErrorAt tk m!"❌ Docstring on `#guard_msgs` does not match generated message:\n\n{feedback}"
       pushInfoLeaf (.ofCustomInfo { stx := ← getRef, value := Dynamic.mk (GuardMsgFailure.mk res) })
   | _ => throwUnsupportedSyntax
 
diff --git a/src/Lean/Util/Diff.lean b/src/Lean/Util/Diff.lean
new file mode 100644
index 0000000000..3e68cd0748
--- /dev/null
+++ b/src/Lean/Util/Diff.lean
@@ -0,0 +1,198 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+prelude
+import Init.Data
+import Lean.Data.HashMap
+import Init.Omega
+
+namespace Lean.Diff
+/--
+An action in an edit script to transform one source sequence into a target sequence.
+-/
+inductive Action where
+  /-- Insert the item into the source -/
+  | insert
+  /-- Delete the item from the source -/
+  | delete
+  /-- Leave the item in the source -/
+  | skip
+deriving Repr, BEq, Hashable, Repr
+
+instance : ToString Action where
+  toString
+    | .insert => "insert"
+    | .delete => "delete"
+    | .skip => "skip"
+
+/--
+Determines a prefix to show on a given line when printing diff results.
+
+For `delete`, the prefix is `"-"`, for `insert`, it is `"+"`, and for `skip` it is `" "`.
+-/
+def Action.linePrefix : (action : Action) → String
+  | .delete => "-"
+  | .insert => "+"
+  | .skip => " "
+
+/--
+A histogram entry consists of the number of times the element occurs in the left and right input
+arrays along with an index at which the element can be found, if applicable.
+-/
+structure Histogram.Entry (α : Type u) (lsize rsize : Nat) where
+  /-- How many times the element occurs in the left array -/
+  leftCount : Nat
+  /-- An index of the element in the left array, if applicable -/
+  leftIndex : Option (Fin lsize)
+  /-- Invariant: the count is non-zero iff there is a saved index -/
+  leftWF : leftCount = 0 ↔ leftIndex = none
+  /-- How many times the element occurs in the right array -/
+  rightCount : Nat
+  /-- An index of the element in the right array, if applicable -/
+  rightIndex : Option (Fin rsize)
+  /-- Invariant: the count is non-zero iff there is a saved index -/
+  rightWF : rightCount = 0 ↔ rightIndex = none
+
+/-- A histogram for arrays maps each element to a count and, if applicable, an index.-/
+def Histogram (α : Type u) (lsize rsize : Nat) [BEq α] [Hashable α] :=
+  Lean.HashMap α (Histogram.Entry α lsize rsize)
+
+
+section
+
+variable [BEq α] [Hashable α]
+
+/-- Add an element from the left array to a histogram -/
+def Histogram.addLeft (histogram : Histogram α lsize rsize) (index : Fin lsize) (val : α)
+    : Histogram α lsize rsize :=
+  match histogram.find? val with
+  | none => histogram.insert val {
+      leftCount := 1, leftIndex := some index,
+      leftWF := by simp,
+      rightCount := 0, rightIndex := none
+      rightWF := by simp
+    }
+  | some x => histogram.insert val {x with
+      leftCount := x.leftCount + 1, leftIndex := some index, leftWF := by simp
+    }
+
+/-- Add an element from the right array to a histogram -/
+def Histogram.addRight (histogram : Histogram α lsize rsize) (index : Fin rsize) (val : α)
+    : Histogram α lsize rsize :=
+  match histogram.find? val with
+  | none => histogram.insert val {
+      leftCount := 0, leftIndex := none,
+      leftWF := by simp,
+      rightCount := 1, rightIndex := some index,
+      rightWF := by simp
+    }
+  | some x => histogram.insert val {x with
+      rightCount := x.leftCount + 1, rightIndex := some index,
+      rightWF := by simp
+    }
+
+/-- Given two `Subarray`s, find their common prefix and return their differing suffixes -/
+def matchPrefix (left right : Subarray α) : Array α × Subarray α × Subarray α :=
+  let rec go (pref : Array α) : Array α × Subarray α × Subarray α :=
+    let i := pref.size
+    if _ : i < left.size ∧ i < right.size then
+      if left[i]'(by omega) == right[i]'(by omega) then
+        go <| pref.push <| left[i]'(by omega)
+      else (pref, left.drop pref.size, right.drop pref.size)
+    else (pref, left.drop pref.size, right.drop pref.size)
+  termination_by left.size - pref.size
+  go #[]
+
+
+/-- Given two `Subarray`s, find their common suffix and return their differing prefixes -/
+def matchSuffix (left right : Subarray α) : Subarray α × Subarray α × Array α :=
+  let rec go (i : Nat) : Subarray α × Subarray α × Array α :=
+    if _ : i < left.size ∧ i < right.size then
+      if left[left.size - i - 1]'(by omega) == right[right.size - i - 1]'(by omega) then
+        go i.succ
+      else
+        (left.take (left.size - i), right.take (right.size - i), (left.drop (left.size - i)).toArray)
+    else
+      (left.take (left.size - i), right.take (right.size - i), (left.drop (left.size - i)).toArray)
+    termination_by left.size - i
+  go 0
+
+/--
+Finds the least common subsequence of two arrays using a variant of jgit's histogram diff algorithm.
+
+Unlike jgit's implementation, this one does not perform a cutoff on histogram bucket sizes, nor does
+it fall back to the Myers diff algorithm. This means that it has quadratic worst-case complexity.
+Empirically, however, even quadratic cases of this implementation can handle hundreds of megabytes
+in a second or so, and it is intended to be used for short strings like error messages. Be
+cautious when applying it to larger workloads.
+-/
+partial def lcs (left right : Subarray α) : Array α := Id.run do
+  let (pref, left, right) := matchPrefix left right
+  let (left, right, suff) := matchSuffix left right
+  let mut hist : Histogram α left.size right.size := .empty
+  for h : i in [0:left.size] do
+    hist := hist.addLeft ⟨i, Membership.get_elem_helper h rfl⟩ left[i]
+  for h : i in [0:right.size] do
+    hist := hist.addRight ⟨i, Membership.get_elem_helper h rfl⟩ right[i]
+  let mut best := none
+  for (k, v) in hist.toList do
+    if let {leftCount := lc, leftIndex := some li, rightCount := rc, rightIndex := some ri, ..} := v then
+      match best with
+      | none =>
+        best := some ((lc + rc), k, li, ri)
+      | some (count, _) =>
+        if lc + rc < count then
+          best := some ((lc + rc), k, li, ri)
+  let some (_, v, li, ri) := best
+    | return pref ++ suff
+
+  let lefts := left.split ⟨li.val, by cases li; simp_arith; omega⟩
+  let rights := right.split ⟨ri.val, by cases ri; simp_arith; omega⟩
+
+  pref ++ lcs lefts.1 rights.1 ++ #[v] ++ lcs (lefts.2.drop 1) (rights.2.drop 1) ++ suff
+
+/--
+Computes an edit script to transform `left` into `right`.
+-/
+def diff [Inhabited α] (original edited : Array α) : Array (Action × α) :=
+  if h : ¬(0 < original.size) then
+    edited.map (.insert, ·)
+  else if h' : ¬(0 < edited.size) then
+    original.map (.delete, ·)
+  else Id.run do
+    have : original.size > 0 := by omega
+    have : edited.size > 0 := by omega
+    let mut out := #[]
+    let ds := lcs original.toSubarray edited.toSubarray
+    let mut i := 0
+    let mut j := 0
+    for d in ds do
+      while i < original.size && original[i]! != d do
+        out := out.push <| (.delete, original[i]!)
+        i := i.succ
+      while j < edited.size && edited[j]! != d do
+        out := out.push <| (.insert, edited[j]!)
+        j := j.succ
+      out := out.push <| (.skip, d)
+      i := i.succ
+      j := j.succ
+    while h : i < original.size do
+      out := out.push <| (.delete, original[i])
+      i := i.succ
+    while h : j < edited.size do
+      out := out.push <| (.insert, edited[j])
+      j := j.succ
+    out
+
+/-- Shows a line-by-line edit script with markers for added and removed lines. -/
+def linesToString [ToString α] (lines : Array (Action × α)) : String := Id.run do
+  let mut out : String := ""
+  for (act, line) in lines do
+    let lineStr := toString line
+    if lineStr == "" then
+      out := out ++ s!"{act.linePrefix}\n"
+    else
+      out := out ++ s!"{act.linePrefix} {lineStr}\n"
+  out
diff --git a/tests/lean/run/diff.lean b/tests/lean/run/diff.lean
new file mode 100644
index 0000000000..0b2a2398ae
--- /dev/null
+++ b/tests/lean/run/diff.lean
@@ -0,0 +1,97 @@
+import Lean.Util.Diff
+
+open Lean.Diff
+
+/-!
+# Tests for diff
+
+Tests for various parts of the diffing system
+-/
+
+
+/-!
+## Prefix and Suffix Matching
+
+These tests check that the prefix and suffix matching operations on subarrays used by diff perform
+as expected.
+-/
+
+def Ex.abc' := #['a', 'b', 'c']
+def Ex.abc := abc'.toSubarray
+
+def Ex.abcde : Subarray Char := #['a','b','c','d','e'].toSubarray
+def Ex.bcde : Subarray Char := #['b','c','d','e'].toSubarray
+
+/-- info: (#['a', 'b', 'c'], #[].toSubarray, #['d', 'e'].toSubarray) -/
+#guard_msgs in
+#eval matchPrefix Ex.abc Ex.abcde
+
+/-- info: (#['a', 'b', 'c'], #['d', 'e'].toSubarray, #[].toSubarray) -/
+#guard_msgs in
+#eval matchPrefix Ex.abcde Ex.abc
+
+/-- info: (#[], #['a', 'b', 'c'].toSubarray, #['b', 'c', 'd', 'e'].toSubarray) -/
+#guard_msgs in
+#eval matchPrefix Ex.abc Ex.bcde
+
+/-- info: (#[], #["A"].toSubarray, #["B"].toSubarray) -/
+#guard_msgs in
+#eval matchPrefix #["A"].toSubarray #["B"].toSubarray
+
+/-- info: (#["D", "E", "F"], #["G"].toSubarray, #[].toSubarray) -/
+#guard_msgs in
+#eval matchPrefix #["D", "E", "F", "G"].toSubarray #["D", "E", "F"].toSubarray
+
+/-- info: (#["A", "A"], #["B"].toSubarray, #["X"].toSubarray) -/
+#guard_msgs in
+#eval matchPrefix #["A", "A", "B"].toSubarray #["A", "A", "X"].toSubarray
+
+
+def Ex.xyzabc : Subarray Char := #['x', 'y', 'z', 'a', 'b', 'c'].toSubarray
+def Ex.xyzab : Subarray Char := #['x', 'y', 'z', 'a', 'b'].toSubarray
+
+/-- info: (#[].toSubarray, #['x', 'y', 'z'].toSubarray, #['a', 'b', 'c']) -/
+#guard_msgs in
+#eval matchSuffix Ex.abc Ex.xyzabc
+
+/-- info: (#['a', 'b', 'c'].toSubarray, #['x', 'y', 'z', 'a', 'b'].toSubarray, #[]) -/
+#guard_msgs in
+#eval matchSuffix Ex.abc Ex.xyzab
+
+/-- info: (#['a'].toSubarray, #[].toSubarray, #['b']) -/
+#guard_msgs in
+#eval matchSuffix #['a', 'b'].toSubarray #['b'].toSubarray
+
+/-!
+## Least Common Subsequence
+
+These tests find least common subsequences.
+-/
+
+/-- info: #[] -/
+#guard_msgs in
+#eval lcs (α := Nat) (#[].toSubarray) (#[].toSubarray)
+
+/-- info: #[] -/
+#guard_msgs in
+#eval lcs  (#[1].toSubarray) (#[].toSubarray)
+
+/-- info: #[1] -/
+#guard_msgs in
+#eval lcs  (#[1].toSubarray) (#[1].toSubarray)
+
+/-- info: #[1, 3] -/
+#guard_msgs in
+#eval lcs  (#[1,3].toSubarray) (#[1,2,3].toSubarray)
+
+/-- info: #["A", "A"] -/
+#guard_msgs in
+#eval lcs ("A,A,B".split (·==',') |>.toArray).toSubarray ("A,A,X".split (·==',') |>.toArray).toSubarray
+
+/-- info: #["A", "D", "E", "F"] -/
+#guard_msgs in
+#eval lcs ("A,C,D,E,F,G".split (·==',') |>.toArray).toSubarray ("A,Y,Z,D,E,F".split (·==',') |>.toArray).toSubarray
+
+/-- info: #["A", "A", "D", "E", "F"] -/
+#guard_msgs in
+#eval lcs ("A,A,B,C,D,E,F,G".split (·==',') |>.toArray).toSubarray ("A,A,X,Y,Z,D,E,F".split (·==',') |>.toArray).toSubarray
diff --git a/tests/lean/run/diff.lean.expected.out b/tests/lean/run/diff.lean.expected.out
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean
index 28d2d95505..e85f273f63 100644
--- a/tests/lean/run/guard_msgs.lean
+++ b/tests/lean/run/guard_msgs.lean
@@ -150,3 +150,148 @@ note: this linter can be disabled with `set_option linter.unusedVariables false`
 #guard_msgs in
 #guard_msgs (info) in
 example (n : Nat) : True := trivial
+
+/-!
+Test diffs
+-/
+
+/--
+info: ABCDEFG
+HIJKLMNOP
+QRSTUVWXYZ
+---
+error: ❌ Docstring on `#guard_msgs` does not match generated message:
+
+-
++ info: ABCDEFG
++ HIJKLMNOP
++ QRSTUVWXYZ
+-/
+#guard_msgs in
+set_option guard_msgs.diff true in
+#guard_msgs in
+#eval IO.println "ABCDEFG\nHIJKLMNOP\nQRSTUVWXYZ"
+
+/--
+info: ABCDEFG
+HIJKLMNOP
+QRSTUVWXYZ
+---
+error: ❌ Docstring on `#guard_msgs` does not match generated message:
+
+  info: ABCDEFG
++ HIJKLMNOP
+  QRSTUVWXYZ
+-/
+#guard_msgs in
+set_option guard_msgs.diff true in
+/--
+info: ABCDEFG
+QRSTUVWXYZ
+-/
+#guard_msgs in
+#eval IO.println "ABCDEFG\nHIJKLMNOP\nQRSTUVWXYZ"
+
+inductive Tree where
+  | leaf (x : Nat)
+  | branch (left : Tree) (x : Nat) (right : Tree)
+deriving Repr
+
+def Tree.build (n k : Nat) : Tree :=
+  if n = 0 then leaf k else branch (Tree.build (n - 1) k) n (Tree.build (n - k - 1) (k / 2))
+
+/--
+info: Tree.branch
+  (Tree.branch
+    (Tree.branch
+      (Tree.branch
+        (Tree.branch
+          (Tree.branch (Tree.branch (Tree.branch (Tree.leaf 3) 1 (Tree.leaf 1)) 2 (Tree.leaf 1)) 3 (Tree.leaf 1))
+          4
+          (Tree.leaf 1))
+        5
+        (Tree.branch (Tree.leaf 1) 1 (Tree.leaf 0)))
+      6
+      (Tree.branch (Tree.branch (Tree.leaf 1) 1 (Tree.leaf 0)) 2 (Tree.leaf 0)))
+    7
+    (Tree.branch
+      (Tree.branch (Tree.branch (Tree.leaf 1) 1 (Tree.leaf 0)) 2 (Tree.leaf 0))
+      3
+      (Tree.branch (Tree.leaf 0) 1 (Tree.leaf 0))))
+  8
+  (Tree.branch
+    (Tree.branch
+      (Tree.branch (Tree.branch (Tree.leaf 1) 1 (Tree.leaf 0)) 2 (Tree.leaf 0))
+      3
+      (Tree.branch (Tree.leaf 0) 1 (Tree.leaf 0)))
+    4
+    (Tree.branch (Tree.branch (Tree.leaf 0) 1 (Tree.leaf 0)) 2 (Tree.branch (Tree.leaf 0) 1 (Tree.leaf 0))))
+---
+error: ❌ Docstring on `#guard_msgs` does not match generated message:
+
+  info: Tree.branch
+    (Tree.branch
+      (Tree.branch
+        (Tree.branch
+          (Tree.branch
+-           (Tree.branch (Tree.branch (Tree.branch (Tree.leaf) 1 (Tree.leaf)) 2 (Tree.leaf)) 3 (Tree.leaf))
++           (Tree.branch (Tree.branch (Tree.branch (Tree.leaf 3) 1 (Tree.leaf 1)) 2 (Tree.leaf 1)) 3 (Tree.leaf 1))
+            4
+-           (Tree.leaf))
++           (Tree.leaf 1))
+          5
+-         (Tree.branch (Tree.leaf) 1 (Tree.leaf)))
++         (Tree.branch (Tree.leaf 1) 1 (Tree.leaf 0)))
+        6
+-       (Tree.branch (Tree.branch (Tree.leaf) 1 (Tree.leaf)) 2 (Tree.leaf)))
++       (Tree.branch (Tree.branch (Tree.leaf 1) 1 (Tree.leaf 0)) 2 (Tree.leaf 0)))
+      7
+      (Tree.branch
+-       (Tree.branch (Tree.branch (Tree.leaf) 1 (Tree.leaf)) 2 (Tree.leaf))
++       (Tree.branch (Tree.branch (Tree.leaf 1) 1 (Tree.leaf 0)) 2 (Tree.leaf 0))
+        3
+-       (Tree.branch (Tree.leaf) 1 (Tree.leaf))))
++       (Tree.branch (Tree.leaf 0) 1 (Tree.leaf 0))))
+    8
+    (Tree.branch
+      (Tree.branch
+-       (Tree.branch (Tree.branch (Tree.leaf) 1 (Tree.leaf)) 2 (Tree.leaf))
++       (Tree.branch (Tree.branch (Tree.leaf 1) 1 (Tree.leaf 0)) 2 (Tree.leaf 0))
+        3
+-       (Tree.branch (Tree.leaf) 1 (Tree.leaf)))
++       (Tree.branch (Tree.leaf 0) 1 (Tree.leaf 0)))
+      4
+-     (Tree.branch (Tree.branch (Tree.leaf) 1 (Tree.leaf)) 2 (Tree.branch (Tree.leaf) 1 (Tree.leaf))))
++     (Tree.branch (Tree.branch (Tree.leaf 0) 1 (Tree.leaf 0)) 2 (Tree.branch (Tree.leaf 0) 1 (Tree.leaf 0))))
+-/
+#guard_msgs in
+set_option guard_msgs.diff true in
+/--
+info: Tree.branch
+  (Tree.branch
+    (Tree.branch
+      (Tree.branch
+        (Tree.branch
+          (Tree.branch (Tree.branch (Tree.branch (Tree.leaf) 1 (Tree.leaf)) 2 (Tree.leaf)) 3 (Tree.leaf))
+          4
+          (Tree.leaf))
+        5
+        (Tree.branch (Tree.leaf) 1 (Tree.leaf)))
+      6
+      (Tree.branch (Tree.branch (Tree.leaf) 1 (Tree.leaf)) 2 (Tree.leaf)))
+    7
+    (Tree.branch
+      (Tree.branch (Tree.branch (Tree.leaf) 1 (Tree.leaf)) 2 (Tree.leaf))
+      3
+      (Tree.branch (Tree.leaf) 1 (Tree.leaf))))
+  8
+  (Tree.branch
+    (Tree.branch
+      (Tree.branch (Tree.branch (Tree.leaf) 1 (Tree.leaf)) 2 (Tree.leaf))
+      3
+      (Tree.branch (Tree.leaf) 1 (Tree.leaf)))
+    4
+    (Tree.branch (Tree.branch (Tree.leaf) 1 (Tree.leaf)) 2 (Tree.branch (Tree.leaf) 1 (Tree.leaf))))
+-/
+#guard_msgs in
+#eval Tree.build 8 3
diff --git a/tests/lean/run/subarray_split.lean b/tests/lean/run/subarray_split.lean
new file mode 100644
index 0000000000..14bcfdd5c8
--- /dev/null
+++ b/tests/lean/run/subarray_split.lean
@@ -0,0 +1,91 @@
+/-!
+# Tests for Subarray Splitting
+
+The tests in this file check the basic splitting operations on subarrays.
+-/
+
+def abc' := #['a', 'b', 'c']
+def abc := abc'.toSubarray
+
+
+/-!
+
+## Split
+
+Splitting at various indices yields all the input elements the right number of times.
+
+-/
+/-- info: (#[].toSubarray, #[1, 2, 3, 4].toSubarray) -/
+#guard_msgs in
+#eval (#[1,2,3,4].toSubarray.split 0)
+
+/-- info: (#[1].toSubarray, #[2, 3, 4].toSubarray) -/
+#guard_msgs in
+#eval (#[1,2,3,4].toSubarray.split 1)
+
+/-- info: (#[1, 2].toSubarray, #[3, 4].toSubarray) -/
+#guard_msgs in
+#eval (#[1,2,3,4].toSubarray.split 2)
+
+/-- info: (#[1, 2, 3].toSubarray, #[4].toSubarray) -/
+#guard_msgs in
+#eval (#[1,2,3,4].toSubarray.split 3)
+
+/-- info: (#[1, 2, 3, 4].toSubarray, #[].toSubarray) -/
+#guard_msgs in
+#eval (#[1,2,3,4].toSubarray.split ⟨4, by decide⟩)
+
+/-- info: (#[2, 3].toSubarray, #[4].toSubarray) -/
+#guard_msgs in
+#eval (#[1,2,3,4].toSubarray (start := 1) |>.split ⟨2, by decide⟩)
+
+
+/-- info: (#[].toSubarray, #['a', 'b', 'c'].toSubarray) -/
+#guard_msgs in
+#eval abc.split 0
+
+/-- info: (#['a'].toSubarray, #['b', 'c'].toSubarray) -/
+#guard_msgs in
+#eval abc.split 1
+
+/-- info: (#['a', 'b'].toSubarray, #['c'].toSubarray) -/
+#guard_msgs in
+#eval abc.split 2
+
+/-- info: (#['a', 'b', 'c'].toSubarray, #[].toSubarray) -/
+#guard_msgs in
+#eval abc.split 3
+
+/-!
+## Take and Drop
+-/
+
+/-- info: #[].toSubarray -/
+#guard_msgs in
+#eval #[1,2,3].toSubarray.take 0
+
+/-- info: #[1].toSubarray -/
+#guard_msgs in
+#eval #[1,2,3].toSubarray.take 1
+/-- info: #[1, 2].toSubarray -/
+#guard_msgs in
+#eval #[1,2,3].toSubarray.take 2
+/-- info: #[1, 2, 3].toSubarray -/
+#guard_msgs in
+#eval #[1,2,3].toSubarray.take 100
+
+/-- info: #[1, 2, 3].toSubarray -/
+#guard_msgs in
+#eval #[1,2,3].toSubarray.drop 0
+
+/-- info: #[2, 3].toSubarray -/
+#guard_msgs in
+#eval #[1,2,3].toSubarray.drop 1
+
+/-- info: #[3].toSubarray -/
+#guard_msgs in
+#eval #[1,2,3].toSubarray.drop 2
+
+/-- info: #[].toSubarray -/
+#guard_msgs in
+#eval #[1,2,3].toSubarray.drop 100
diff --git a/tests/lean/run/subarray_split.lean.expected.out b/tests/lean/run/subarray_split.lean.expected.out
new file mode 100644
index 0000000000..e69de29bb2