chore: deprecate Lean.Meta.DiscrTree.elements (#1952)

Author: robsimmons

Batteries/Tactic/Lint/Simp.lean

@@ -5,6 +5,7 @@ Authors: Gabriel Ebner
 -/
 module
 
+public meta import Lean.Meta.DiscrTree.Util
 public meta import Lean.Meta.Tactic.Simp.Main
 public meta import Batteries.Tactic.Lint.Basic
 public meta import Batteries.Tactic.OpenPrivate
@@ -101,13 +102,9 @@ def isSimpTheorem (declName : Name) : MetaM Bool := do
 
 open Lean.Meta.DiscrTree in
 /-- Returns the list of elements in the discrimination tree. -/
+@[deprecated Lean.Meta.DiscrTree.values (since := "2026-08-25")]
 partial def _root_.Lean.Meta.DiscrTree.elements (d : DiscrTree α) : Array α :=
-  d.root.foldl (init := #[]) fun arr _ => trieElements arr
-where
-  /-- Returns the list of elements in the trie. -/
-  trieElements (arr)
-  | Trie.node vs children =>
-    children.foldl (init := arr ++ vs) fun arr (_, child) => trieElements arr child
+  d.values
 
 /-- Add message `msg` to any errors thrown inside `k`. -/
 def decorateError (msg : MessageData) (k : MetaM α) : MetaM α := do