From e99ccf641ad056e1a7b6abe5a90f8ab6574177c5 Mon Sep 17 00:00:00 2001
From: Rob Simmons <robsimmons@gmail.com>
Date: Mon, 24 Aug 2026 08:47:43 -0400
Subject: [PATCH 1/3] feat: create asNode/mkNode abstraction for DiscrTree

---
 src/Lean/Meta/DiscrTree/Basic.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/Lean/Meta/DiscrTree/Basic.lean b/src/Lean/Meta/DiscrTree/Basic.lean
index 745033421224..635ff5415fc4 100644
--- a/src/Lean/Meta/DiscrTree/Basic.lean
+++ b/src/Lean/Meta/DiscrTree/Basic.lean
@@ -122,6 +122,20 @@ where
       r := r.push (← go)
     return r
 
+/--
+Generate a trie node from values and an array of children.
+-/
+@[inline]
+def Trie.mkNode (vs : Array α) (cs : Array (Key × Trie α)) : Trie α :=
+  .node vs cs
+
+/--
+Inspect a trie node as an array of values and an array of children.
+-/
+@[inline]
+def Trie.asNode : Trie α → Array α × Array (Key × Trie α)
+  | .node vs cs => ⟨vs, cs⟩
+
 private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α :=
   if h : i < keys.size then
     let k := keys[i]

From 764775e726453c08833c10166eaa4d3587715035 Mon Sep 17 00:00:00 2001
From: Rob Simmons <robsimmons@gmail.com>
Date: Mon, 24 Aug 2026 12:34:48 -0400
Subject: [PATCH 2/3] add `Trie.nodeValues` and `Trie.nodeChildren` utility
 functions

---
 src/Lean/Meta/DiscrTree/Util.lean | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/DiscrTree/Util.lean b/src/Lean/Meta/DiscrTree/Util.lean
index 8b56d1360c40..42f8eb328134 100644
--- a/src/Lean/Meta/DiscrTree/Util.lean
+++ b/src/Lean/Meta/DiscrTree/Util.lean
@@ -51,7 +51,21 @@ partial def size : Trie α → Nat
     children.foldl (init := vs.size) fun n (_, c) => n + size c
 
 /--
-Checks that a trie node has no values and no children.
+Returns the values stored at the current trie node.
+Equivalent to `t.asNode.1`.
+-/
+def nodeValues : Trie α → Array α
+  | .node vs _ => vs
+
+/--
+Returns the child nodes of the current trie node.
+Equivalent to `t.asNode.2`.
+-/
+def nodeChildren : Trie α → Array (Key × Trie α)
+  | .node _ cs => cs
+
+/--
+Checks whether a trie node is empty (no values and no children).
 
 This is only a check for actual trie emptiness (`t.size = 0`) if all operations maintain the
 invariant that no trie node has an empty child node.

From c2e122e0047db6a922334a8434c88dbe069debdd Mon Sep 17 00:00:00 2001
From: Rob Simmons <robsimmons@gmail.com>
Date: Tue, 25 Aug 2026 09:08:34 -0400
Subject: [PATCH 3/3] consolidate in Util.lean

---
 src/Lean/Meta/DiscrTree/Basic.lean | 14 --------------
 src/Lean/Meta/DiscrTree/Util.lean  | 16 ++++++++++++++++
 2 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/src/Lean/Meta/DiscrTree/Basic.lean b/src/Lean/Meta/DiscrTree/Basic.lean
index 635ff5415fc4..745033421224 100644
--- a/src/Lean/Meta/DiscrTree/Basic.lean
+++ b/src/Lean/Meta/DiscrTree/Basic.lean
@@ -122,20 +122,6 @@ where
       r := r.push (← go)
     return r
 
-/--
-Generate a trie node from values and an array of children.
--/
-@[inline]
-def Trie.mkNode (vs : Array α) (cs : Array (Key × Trie α)) : Trie α :=
-  .node vs cs
-
-/--
-Inspect a trie node as an array of values and an array of children.
--/
-@[inline]
-def Trie.asNode : Trie α → Array α × Array (Key × Trie α)
-  | .node vs cs => ⟨vs, cs⟩
-
 private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α :=
   if h : i < keys.size then
     let k := keys[i]
diff --git a/src/Lean/Meta/DiscrTree/Util.lean b/src/Lean/Meta/DiscrTree/Util.lean
index 42f8eb328134..bd95cbfc7162 100644
--- a/src/Lean/Meta/DiscrTree/Util.lean
+++ b/src/Lean/Meta/DiscrTree/Util.lean
@@ -50,10 +50,25 @@ partial def size : Trie α → Nat
   | Trie.node vs children =>
     children.foldl (init := vs.size) fun n (_, c) => n + size c
 
+/--
+Generate a trie node from values and an array of children.
+-/
+@[inline]
+def mkNode (vs : Array α) (cs : Array (Key × Trie α)) : Trie α :=
+  .node vs cs
+
+/--
+Inspect a trie node as an array of values and an array of children.
+-/
+@[inline]
+def asNode : Trie α → Array α × Array (Key × Trie α)
+  | .node vs cs => ⟨vs, cs⟩
+
 /--
 Returns the values stored at the current trie node.
 Equivalent to `t.asNode.1`.
 -/
+@[inline]
 def nodeValues : Trie α → Array α
   | .node vs _ => vs
 
@@ -61,6 +76,7 @@ def nodeValues : Trie α → Array α
 Returns the child nodes of the current trie node.
 Equivalent to `t.asNode.2`.
 -/
+@[inline]
 def nodeChildren : Trie α → Array (Key × Trie α)
   | .node _ cs => cs