[#14805] feat: special case single-child nodes in DiscrTree

batteries/Batteries/Lean/Meta/DiscrTree.lean

@@ -38,9 +38,10 @@ namespace Trie
 /--
 Merge two `Trie`s. Duplicate values are preserved.
 -/
-partial def mergePreservingDuplicates : Trie α → Trie α → Trie α
-  | node vs₁ cs₁, node vs₂ cs₂ =>
-    node (vs₁ ++ vs₂) (mergeChildren cs₁ cs₂)
+partial def mergePreservingDuplicates (t₁ t₂ : Trie α) : Trie α :=
+  match (t₁.asNode, t₂.asNode) with
+  | ((vs₁, cs₁), (vs₂, cs₂)) =>
+    Trie.mkNode (vs₁ ++ vs₂) (mergeChildren cs₁ cs₂)
 where
   /-- Auxiliary definition for `mergePreservingDuplicates`. -/
   mergeChildren (cs₁ cs₂ : Array (Key × Trie α)) :

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-08-27
+leanprover/lean4-pr-releases:pr-release-14805-0ad131b

mathlib4/MathlibTest/Tactic/Push/Basic.lean

@@ -55,11 +55,11 @@ info: DiscrTree branch for Or:
   (node
    (* => (node
      (False => (node #[or_false:1000]))
-     (And => (node (* => (node (* => (node #[or_and_left:1000]))))))
+     (And => (chain * => (chain * => (node #[or_and_left:1000]))))
      (True => (node #[or_true:1000]))))
-   (False => (node (* => (node #[false_or:1000]))))
-   (And => (node (* => (node (* => (node (* => (node #[and_or_right:1000]))))))))
-   (True => (node (* => (node #[true_or:1000])))))
+   (False => (chain * => (node #[false_or:1000])))
+   (And => (chain * => (chain * => (chain * => (node #[and_or_right:1000])))))
+   (True => (chain * => (node #[true_or:1000]))))
 -/
 #guard_msgs in
 #push_discr_tree Or