From a629abfa7fb5ae4abc9086b30a2d43b6067f796a Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 14:27:10 +0200
Subject: [PATCH 01/37] rename tree; define memberaship instance; decidable;
 traversal

---
 .../Enumerative/Catalan/Tree.lean             |  16 +-
 .../Combinatorics/Enumerative/DyckWord.lean   |  20 +-
 Mathlib/Data/Tree/Basic.lean                  | 197 ++++++++++++++----
 Mathlib/Data/Tree/Get.lean                    |  10 +-
 Mathlib/Data/Tree/Traversable.lean            |  14 +-
 Mathlib/Tactic/CancelDenoms/Core.lean         |   4 +-
 6 files changed, 189 insertions(+), 72 deletions(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean b/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean
index 6822befbff552e..6985c392913baa 100644
--- a/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean
+++ b/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean
@@ -28,15 +28,15 @@ open Finset
 
 open Finset.antidiagonal (fst_le snd_le)
 
-namespace Tree
+namespace BinaryTree
 
 /-- Given two finsets, find all trees that can be formed with
   left child in `a` and right child in `b` -/
-abbrev pairwiseNode (a b : Finset (Tree Unit)) : Finset (Tree Unit) :=
+abbrev pairwiseNode (a b : Finset (BinaryTree Unit)) : Finset (BinaryTree Unit) :=
   (a ×ˢ b).map ⟨fun x => x.1 △ x.2, fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ => fun h => by simpa using h⟩
 
 /-- A Finset of all trees with `n` nodes. See `mem_treesOfNodesEq` -/
-def treesOfNumNodesEq : ℕ → Finset (Tree Unit)
+def treesOfNumNodesEq : ℕ → Finset (BinaryTree Unit)
   | 0 => {nil}
   | n + 1 =>
     (antidiagonal n).attach.biUnion fun ijh =>
@@ -57,17 +57,17 @@ theorem treesOfNumNodesEq_succ (n : ℕ) :
   simp
 
 @[simp]
-theorem mem_treesOfNumNodesEq {x : Tree Unit} {n : ℕ} :
+theorem mem_treesOfNumNodesEq {x : BinaryTree Unit} {n : ℕ} :
     x ∈ treesOfNumNodesEq n ↔ x.numNodes = n := by
-  induction x using Tree.unitRecOn generalizing n <;> cases n <;>
+  induction x using BinaryTree.unitRecOn generalizing n <;> cases n <;>
     simp [treesOfNumNodesEq_succ, *]
 
-theorem mem_treesOfNumNodesEq_numNodes (x : Tree Unit) : x ∈ treesOfNumNodesEq x.numNodes :=
+theorem mem_treesOfNumNodesEq_numNodes (x : BinaryTree Unit) : x ∈ treesOfNumNodesEq x.numNodes :=
   mem_treesOfNumNodesEq.mpr rfl
 
 @[simp, norm_cast]
 theorem coe_treesOfNumNodesEq (n : ℕ) :
-    ↑(treesOfNumNodesEq n) = { x : Tree Unit | x.numNodes = n } :=
+    ↑(treesOfNumNodesEq n) = { x : BinaryTree Unit | x.numNodes = n } :=
   Set.ext (by simp)
 
 theorem treesOfNumNodesEq_card_eq_catalan (n : ℕ) : #(treesOfNumNodesEq n) = catalan n := by
@@ -81,4 +81,4 @@ theorem treesOfNumNodesEq_card_eq_catalan (n : ℕ) : #(treesOfNumNodesEq n) = c
     · simp_rw [Set.PairwiseDisjoint, Set.Pairwise, disjoint_left]
       aesop
 
-end Tree
+end BinaryTree
diff --git a/Mathlib/Combinatorics/Enumerative/DyckWord.lean b/Mathlib/Combinatorics/Enumerative/DyckWord.lean
index fa5d2d4584f561..ea09972e79c192 100644
--- a/Mathlib/Combinatorics/Enumerative/DyckWord.lean
+++ b/Mathlib/Combinatorics/Enumerative/DyckWord.lean
@@ -474,9 +474,9 @@ lemma strictMono_semilength : StrictMono semilength := fun p q pq ↦ by
 
 end Order
 
-section Tree
+section BinaryTree
 
-open Tree
+open BinaryTree
 
 /-- Convert a Dyck word to a binary rooted tree.
 
@@ -485,7 +485,7 @@ which has index `p.firstReturn`, then let `x` be everything strictly between sai
 and `y` be everything strictly after said `D`. `p = x.nest + y` with `x, y` (possibly empty)
 Dyck words. `f(p) = f(x) △ f(y)`, where △ (defined in `Mathlib/Data/Tree/Basic.lean`) joins two
 subtrees to a new root node. -/
-def toTree (p : DyckWord) : Tree Unit :=
+def toTree (p : DyckWord) : BinaryTree Unit :=
   if p = 0 then nil else p.insidePart.toTree △ p.outsidePart.toTree
 termination_by p.semilength
 decreasing_by exacts [semilength_insidePart_lt ‹_›, semilength_outsidePart_lt ‹_›]
@@ -494,9 +494,9 @@ decreasing_by exacts [semilength_insidePart_lt ‹_›, semilength_outsidePart_l
 
 `g(nil) = 0`. A nonempty tree with left subtree `l` and right subtree `r`
 is sent to `g(l).nest + g(r)`. -/
-def ofTree : Tree Unit → DyckWord
-  | Tree.nil => 0
-  | Tree.node _ l r => (ofTree l).nest + ofTree r
+def ofTree : BinaryTree Unit → DyckWord
+  | BinaryTree.nil => 0
+  | BinaryTree.node _ l r => (ofTree l).nest + ofTree r
 
 lemma ofTree_toTree (p) : ofTree p.toTree = p := by
   by_cases h : p = 0
@@ -509,11 +509,11 @@ termination_by p.semilength
 decreasing_by exacts [semilength_insidePart_lt h, semilength_outsidePart_lt h]
 
 lemma toTree_ofTree : ∀ t, (ofTree t).toTree = t
-  | Tree.nil => by simp [ofTree, toTree]
-  | Tree.node _ _ _ => by simp [ofTree, toTree, toTree_ofTree]
+  | BinaryTree.nil => by simp [ofTree, toTree]
+  | BinaryTree.node _ _ _ => by simp [ofTree, toTree, toTree_ofTree]
 
 /-- Equivalence between Dyck words and rooted binary trees. -/
-@[simps] def equivTree : DyckWord ≃ Tree Unit where
+@[simps] def equivTree : DyckWord ≃ BinaryTree Unit where
   toFun := toTree
   invFun := ofTree
   left_inv := ofTree_toTree
@@ -547,7 +547,7 @@ theorem card_dyckWord_semilength_eq_catalan (n : ℕ) :
   rw [← Fintype.ofEquiv_card (equivTreesOfNumNodesEq n), ← treesOfNumNodesEq_card_eq_catalan]
   convert Fintype.card_coe _
 
-end Tree
+end BinaryTree
 
 end DyckWord
 
diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 8862dbdc4e6583..45c70c96c6b7e9 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -9,14 +9,14 @@ public import Mathlib.Data.Nat.Notation
 public import Mathlib.Util.CompileInductive
 
 /-!
-# Binary tree
+# BinaryTree
 
-Provides binary tree storage for values of any type, with O(lg n) retrieval.
-See also `Lean.Data.RBTree` for red-black trees - this version allows more operations
+Provides binary BinaryTree storage for values of any type, with O(lg n) retrieval.
+See also `Lean.Data.RBBinaryTree` for red-black BinaryTrees - this version allows more operations
 to be defined and is better suited for in-kernel computation.
 
-We also specialize for `Tree Unit`, which is a binary tree without any
-additional data. We provide the notation `a △ b` for making a `Tree Unit` with children
+We also specialize for `BinaryTree Unit`, which is a binary BinaryTree without any
+additional data. We provide the notation `a △ b` for making a `BinaryTree Unit` with children
 `a` and `b`.
 
 ## References
@@ -27,109 +27,226 @@ additional data. We provide the notation `a △ b` for making a `Tree Unit` with
 @[expose] public section
 
 
-/-- A binary tree with values stored in non-leaf nodes. -/
-inductive Tree.{u} (α : Type u) : Type u
-  | nil : Tree α
-  | node (value : α) (left : Tree α) (right : Tree α) : Tree α
+/-- A binary BinaryTree with values stored in non-leaf nodes. -/
+inductive BinaryTree.{u} (α : Type u) : Type u
+  | nil : BinaryTree α
+  | node (value : α) (left : BinaryTree α) (right : BinaryTree α) : BinaryTree α
   deriving DecidableEq, Repr
-compile_inductive% Tree
+compile_inductive% BinaryTree
 
-namespace Tree
+namespace BinaryTree
 
 universe u
 
 variable {α : Type u}
 
-instance : Inhabited (Tree α) :=
+instance : Inhabited (BinaryTree α) :=
   ⟨nil⟩
 
+
 /--
-Do an action for every node of the tree.
-Actions are taken in node -> left subtree -> right subtree recursive order.
-This function is the `traverse` function for the `Traversable Tree` instance.
+Do an action for every node of the BinaryTree.
+Actions are taken in node -> left subBinaryTree -> right subBinaryTree recursive order.
+This function is the `traverse` function for the `Traversable BinaryTree` instance.
 -/
-def traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β) : Tree α → m (Tree β)
+def traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β)
+: BinaryTree α → m (BinaryTree β)
   | .nil => pure nil
   | .node a l r => .node <$> f a <*> traverse f l <*> traverse f r
 
-/-- Apply a function to each value in the tree.  This is the `map` function for the `Tree` functor.
+/-- Apply a function to each value in the BinaryTree.
+This is the `map` function for the `BinaryTree` functor.
 -/
-def map {β} (f : α → β) : Tree α → Tree β
+def map {β} (f : α → β) : BinaryTree α → BinaryTree β
   | nil => nil
   | node a l r => node (f a) (map f l) (map f r)
 
-theorem id_map (t : Tree α) : t.map id = t := by
+theorem id_map (t : BinaryTree α) : t.map id = t := by
   induction t with
   | nil => rw [map]
   | node v l r hl hr => rw [map, hl, hr, id_eq]
 
-theorem comp_map {β γ : Type*} (f : α → β) (g : β → γ) (t : Tree α) :
+theorem comp_map {β γ : Type*} (f : α → β) (g : β → γ) (t : BinaryTree α) :
     t.map (g ∘ f) = (t.map f).map g := by
   induction t with
   | nil => rw [map, map, map]
   | node v l r hl hr => rw [map, map, map, hl, hr, Function.comp_apply]
 
-theorem traverse_pure (t : Tree α) {m : Type u → Type*} [Applicative m] [LawfulApplicative m] :
-    t.traverse (pure : α → m α) = pure t := by
+theorem traverse_pure (t : BinaryTree α) {m : Type u → Type*} [Applicative m] [LawfulApplicative m]
+: t.traverse (pure : α → m α) = pure t := by
   induction t with
   | nil => rw [traverse]
   | node v l r hl hr =>
     rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]
 
-/-- The number of internal nodes (i.e. not including leaves) of a binary tree -/
+/-- The number of internal nodes (i.e. not including leaves) of a binary BinaryTree -/
 @[simp]
-def numNodes : Tree α → ℕ
+def numNodes : BinaryTree α → ℕ
   | nil => 0
   | node _ a b => a.numNodes + b.numNodes + 1
 
-/-- The number of leaves of a binary tree -/
+/-- The number of leaves of a binary BinaryTree -/
 @[simp]
-def numLeaves : Tree α → ℕ
+def numLeaves : BinaryTree α → ℕ
   | nil => 1
   | node _ a b => a.numLeaves + b.numLeaves
 
-/-- The height - length of the longest path from the root - of a binary tree -/
+/-- The height - length of the longest path from the root - of a binary BinaryTree -/
 @[simp]
-def height : Tree α → ℕ
+def height : BinaryTree α → ℕ
   | nil => 0
   | node _ a b => max a.height b.height + 1
 
-theorem numLeaves_eq_numNodes_succ (x : Tree α) : x.numLeaves = x.numNodes + 1 := by
+theorem numLeaves_eq_numNodes_succ (x : BinaryTree α) : x.numLeaves = x.numNodes + 1 := by
   induction x <;> simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]
 
-theorem numLeaves_pos (x : Tree α) : 0 < x.numLeaves := by
+theorem numLeaves_pos (x : BinaryTree α) : 0 < x.numLeaves := by
   rw [numLeaves_eq_numNodes_succ]
   exact x.numNodes.zero_lt_succ
 
-theorem height_le_numNodes : ∀ x : Tree α, x.height ≤ x.numNodes
+theorem height_le_numNodes : ∀ x : BinaryTree α, x.height ≤ x.numNodes
   | nil => Nat.le_refl _
   | node _ a b => Nat.succ_le_succ <|
     Nat.max_le.2 ⟨Nat.le_trans a.height_le_numNodes <| a.numNodes.le_add_right _,
       Nat.le_trans b.height_le_numNodes <| b.numNodes.le_add_left _⟩
 
-/-- The left child of the tree, or `nil` if the tree is `nil` -/
+/-- The left child of the BinaryTree, or `nil` if the BinaryTree is `nil` -/
 @[simp]
-def left : Tree α → Tree α
+def left : BinaryTree α → BinaryTree α
   | nil => nil
   | node _ l _r => l
 
-/-- The right child of the tree, or `nil` if the tree is `nil` -/
+/-- The right child of the BinaryTree, or `nil` if the BinaryTree is `nil` -/
 @[simp]
-def right : Tree α → Tree α
+def right : BinaryTree α → BinaryTree α
   | nil => nil
   | node _ _l r => r
 
 /-- A node with `Unit` data -/
-scoped infixr:65 " △ " => Tree.node ()
+scoped infixr:65 " △ " => BinaryTree.node ()
+
+/-- A tree node -/
+scoped notation:65 l:66 " △[" v "] " r:66 => BinaryTree.node v l r
+
+/--
+BinaryTree membership, typically accessed via the `∈` operator.
+
+`a ∈ T` means that `a` is an element of the binary tree `T`.
+Elements are compared according to Lean's logical equality.
 
-/-- Induction principle for `Tree Unit`s -/
+Examples:
+* `a ∈ ((nil △[x] nil) △[y] nil) ↔ a = x ∨ a = y`
+-/
+inductive Mem (a : α) : BinaryTree α → Prop
+| node  {l r}   : Mem a (l △[a] r)
+| left  (b : α) {l r} : Mem a l → Mem a (l △[b] r)
+| right (b : α) {l r} : Mem a r → Mem a (l △[b] r)
+
+/-- Defines the `∈` notation for `BinaryTree`.
+    `a ∈ t` unfolds to `Mem a t`, flipping argument order to match
+    Lean's `Membership` typeclass convention. -/
+instance : Membership α (BinaryTree α) where
+  mem l a := Mem a l
+
+/-- A singleton tree `nil △[x] nil` contains exactly `x`. -/
+theorem mem_singleton_iff (a x : ℕ) : a ∈ ((nil △[x] nil)) ↔ a = x := by
+  constructor
+  · intro h
+    cases h <;> trivial
+  · intro h
+    subst h
+    apply Mem.node
+
+def contains [BEq α] (t : BinaryTree α) (a : α) :  Bool := match t with
+  | .nil        => false
+  | l △[b] r => a == b || l.contains a  || r.contains a
+
+/-- `contains` is sound and complete with respect to `Mem`. -/
+theorem contains_iff {α : Type u} [inst : BEq α] [inst_1 : LawfulBEq α]
+  (a : α) (t : BinaryTree α) : t.contains a = true ↔ a ∈ t := by
+  fun_induction contains
+  · simp_all only [Bool.false_eq_true, false_iff]
+    false_or_by_contra
+    expose_names
+    cases h
+  · expose_names
+    simp only [Bool.or_eq_true, beq_iff_eq, ih2, ih1]
+    constructor
+    · rintro ( ⟨h | h⟩ | h)
+      · subst h; exact .node
+      · exact .left a_1 h
+      · exact .right a_1 h
+    · intro h
+      cases h
+      · grind
+      · left
+        right
+        assumption
+      · right; assumption
+
+/-- Lifts `contains` to a `Decidable` instance for `a ∈ t`.
+    Enables `if a ∈ t then ...` and `decide (a ∈ t)` without any extra proof work.
+    Requires `LawfulBEq` to connect `BEq` to propositional equality. -/
+instance [BEq α] [LawfulBEq α] (a : α) (t : BinaryTree α) : Decidable (a ∈ t)  :=
+  decidable_of_iff (t.contains a = true) (t.contains_iff a)
+
+/-- Checks whether a boolean predicate holds for every node in the tree.
+    Traversal order: current node, then left subtree, then right subtree. -/
+def all (p : α → Bool) : BinaryTree α → Bool
+  | nil        => true
+  | l △[b] r => p b && all p l && all p r
+
+/-- `all` is sound and complete with respect to `∀ x ∈ t, p x`. -/
+theorem all_iff (p : α → Prop) [inst : DecidablePred p]
+  (t : BinaryTree α) : t.all (fun x ↦ p x) = true ↔ ∀ x ∈ t, p x := by
+  fun_induction all
+  · simp only [true_iff]; intros; contradiction
+  · expose_names
+    simp only [Bool.and_eq_true, decide_eq_true_eq, ih2, ih1]
+    constructor
+    · rintro ⟨⟨h1,h3⟩,h2⟩ x hx
+      cases hx
+      · assumption
+      · expose_names
+        apply h3
+        exact h
+      · expose_names
+        apply h2
+        exact h
+    · intro h
+      exact ⟨⟨h a .node,
+        fun x m => h x (.left a m)⟩,
+        fun x m => h x (.right a m)⟩
+
+/-- `Decidable` instance for bounded universal quantification over a `BinaryTree`. -/
+instance decidableBAll (p : α → Prop) [DecidablePred p] (t : BinaryTree α) :
+    Decidable (∀ x ∈ t, p x) :=
+      decidable_of_iff (t.all (fun x => p x)) (all_iff p t)
+
+/-- Induction principle for `BinaryTree Unit`s -/
 @[elab_as_elim]
-def unitRecOn {motive : Tree Unit → Sort*} (t : Tree Unit) (base : motive nil)
+def unitRecOn {motive : BinaryTree Unit → Sort*} (t : BinaryTree Unit) (base : motive nil)
     (ind : ∀ x y, motive x → motive y → motive (x △ y)) : motive t :=
   t.recOn base fun _u ↦ ind
 
-theorem left_node_right_eq_self : ∀ {x : Tree Unit} (_hx : x ≠ nil), x.left △ x.right = x
+theorem left_node_right_eq_self : ∀ {x : BinaryTree Unit} (_hx : x ≠ nil), x.left △ x.right = x
   | nil, h => by trivial
   | node _ _ _, _ => rfl  -- Porting note: `a △ b` no longer works in pattern matching
 
-end Tree
+
+/-- Inorder traversal into a list: left → node → right. -/
+def toListInOrder : BinaryTree α → List α
+  | .nil          => []
+  | .node v l r   => l.toListInOrder ++ [v] ++ r.toListInOrder
+
+/-- Preorder traversal  into a list: node → left → right. -/
+def toListPreOrder : BinaryTree α → List α
+  | .nil          => []
+  | .node v l r   => [v] ++ l.toListPreOrder ++ r.toListPreOrder
+
+/-- Postorder traversal  into a list: left → right → node. -/
+def toListPostOrder : BinaryTree α → List α
+  | .nil          => []
+  | .node v l r   => l.toListPostOrder ++ r.toListPostOrder ++ [v]
+
+end BinaryTree
diff --git a/Mathlib/Data/Tree/Get.lean b/Mathlib/Data/Tree/Get.lean
index c18cc3823ff6b2..694cced303f163 100644
--- a/Mathlib/Data/Tree/Get.lean
+++ b/Mathlib/Data/Tree/Get.lean
@@ -22,7 +22,7 @@ These definitions were moved from the main file to avoid a dependency on `Num`.
 
 @[expose] public section
 
-namespace Tree
+namespace BinaryTree
 
 variable {α : Type*}
 
@@ -30,7 +30,7 @@ variable {α : Type*}
 constructed according to the provided decidable order on its elements.
 If it hasn't, the result will be incorrect. If it has, but the element
 is not in the tree, returns none. -/
-def indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : Tree α → Option PosNum
+def indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : BinaryTree α → Option PosNum
   | nil => none
   | node a t₁ t₂ =>
     match cmpUsing lt x a with
@@ -43,7 +43,7 @@ taking the following path to get to the element:
 - `bit0` - go to left child
 - `bit1` - go to right child
 - `PosNum.one` - retrieve from here -/
-def get : PosNum → Tree α → Option α
+def get : PosNum → BinaryTree α → Option α
   | _, nil => none
   | PosNum.one, node a _t₁ _t₂ => some a
   | PosNum.bit0 n, node _a t₁ _t₂ => t₁.get n
@@ -51,7 +51,7 @@ def get : PosNum → Tree α → Option α
 
 /-- Retrieves an element from the tree, or the provided default value
 if the index is invalid. See `Tree.get`. -/
-def getOrElse (n : PosNum) (t : Tree α) (v : α) : α :=
+def getOrElse (n : PosNum) (t : BinaryTree α) (v : α) : α :=
   (t.get n).getD v
 
-end Tree
+end BinaryTree
diff --git a/Mathlib/Data/Tree/Traversable.lean b/Mathlib/Data/Tree/Traversable.lean
index e68c34ad960288..485db8ea3eadb5 100644
--- a/Mathlib/Data/Tree/Traversable.lean
+++ b/Mathlib/Data/Tree/Traversable.lean
@@ -19,18 +19,18 @@ public section
 
 universe u v w
 
-namespace Tree
+namespace BinaryTree
 section Traverse
 variable {α β : Type*}
 
-instance : Traversable Tree where
+instance : Traversable BinaryTree where
   map := map
   traverse := traverse
 
 lemma comp_traverse
     {F : Type u → Type v} {G : Type v → Type w} [Applicative F] [Applicative G]
     [LawfulApplicative G] {β : Type v} {γ : Type u} (f : β → F γ) (g : α → G β)
-    (t : Tree α) : t.traverse (Functor.Comp.mk ∘ (f <$> ·) ∘ g) =
+    (t : BinaryTree α) : t.traverse (Functor.Comp.mk ∘ (f <$> ·) ∘ g) =
       Functor.Comp.mk ((·.traverse f) <$> (t.traverse g)) := by
   induction t with
   | nil => rw [traverse, traverse, map_pure, traverse]; rfl
@@ -40,7 +40,7 @@ lemma comp_traverse
       Comp.seq_mk, seq_map_assoc, map_seq]
     rfl
 
-lemma traverse_eq_map_id (f : α → β) (t : Tree α) :
+lemma traverse_eq_map_id (f : α → β) (t : BinaryTree α) :
     t.traverse ((pure : β → Id β) ∘ f) = pure (t.map f) := by
   induction t with
   | nil => rw [traverse, map]
@@ -50,14 +50,14 @@ lemma traverse_eq_map_id (f : α → β) (t : Tree α) :
 
 lemma naturality {F G : Type u → Type*} [Applicative F] [Applicative G] [LawfulApplicative F]
     [LawfulApplicative G] (η : ApplicativeTransformation F G) {β : Type u} (f : α → F β)
-    (t : Tree α) : η (t.traverse f) = t.traverse (η.app β ∘ f : α → G β) := by
+    (t : BinaryTree α) : η (t.traverse f) = t.traverse (η.app β ∘ f : α → G β) := by
   induction t with
   | nil => rw [traverse, traverse, η.preserves_pure]
   | node v l r hl hr =>
     rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
       Function.comp_apply]
 
-instance : LawfulTraversable Tree where
+instance : LawfulTraversable BinaryTree where
   map_const := rfl
   id_map := id_map
   comp_map := comp_map
@@ -68,4 +68,4 @@ instance : LawfulTraversable Tree where
 
 end Traverse
 
-end Tree
+end BinaryTree
diff --git a/Mathlib/Tactic/CancelDenoms/Core.lean b/Mathlib/Tactic/CancelDenoms/Core.lean
index e7d44daab09426..af4068c577306c 100644
--- a/Mathlib/Tactic/CancelDenoms/Core.lean
+++ b/Mathlib/Tactic/CancelDenoms/Core.lean
@@ -105,7 +105,7 @@ theorem cancel_factors_ne {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad *
 be able to cancel all the numeric denominators in `e`. The returned `Tree` describes how to
 distribute the value `n` over products inside `e`.
 -/
-partial def findCancelFactor (e : Expr) : ℕ × Tree ℕ :=
+partial def findCancelFactor (e : Expr) : ℕ × BinaryTree ℕ :=
   match e.getAppFnArgs with
   | (``HAdd.hAdd, #[_, _, _, _, e1, e2]) | (``HSub.hSub, #[_, _, _, _, e1, e2]) =>
     let (v1, t1) := findCancelFactor e1
@@ -162,7 +162,7 @@ The `v'` argument is a numeral expression corresponding to `v`, which we need in
 the return type accurately.
 -/
 partial def mkProdPrf {u : Level} (α : Q(Type u)) (sα : Q(Field $α)) (v : ℕ) (v' : Q($α))
-    (t : Tree ℕ) (e : Q($α)) : MetaM (CancelResult q(inferInstance) e v') := do
+    (t : BinaryTree ℕ) (e : Q($α)) : MetaM (CancelResult q(inferInstance) e v') := do
   let amwo : Q(AddMonoidWithOne $α) := q(inferInstance)
   trace[CancelDenoms] "mkProdPrf {e} {v}"
   match t, e with

From 9c3719f2170d672a6f37b8b547801427759e27b3 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 14:28:30 +0200
Subject: [PATCH 02/37] author

---
 Mathlib/Data/Tree/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 45c70c96c6b7e9..7830f3cfce9ac7 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 mathlib community. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Wojciech Nawrocki
+Authors: Mario Carneiro, Wojciech Nawrocki, Sorrachai Yingchareonthawornchai
 -/
 module
 

From 952d13f74399f830bfabfc7c0c2347c0f68ee5d9 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 14:31:51 +0200
Subject: [PATCH 03/37] update

---
 Mathlib/Data/Tree/Basic.lean | 21 +++++++--------------
 1 file changed, 7 insertions(+), 14 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 7830f3cfce9ac7..f8eba6aad43be2 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -142,13 +142,10 @@ inductive Mem (a : α) : BinaryTree α → Prop
 | left  (b : α) {l r} : Mem a l → Mem a (l △[b] r)
 | right (b : α) {l r} : Mem a r → Mem a (l △[b] r)
 
-/-- Defines the `∈` notation for `BinaryTree`.
-    `a ∈ t` unfolds to `Mem a t`, flipping argument order to match
-    Lean's `Membership` typeclass convention. -/
+/-- Defines the `∈` notation for `BinaryTree`. -/
 instance : Membership α (BinaryTree α) where
   mem l a := Mem a l
 
-/-- A singleton tree `nil △[x] nil` contains exactly `x`. -/
 theorem mem_singleton_iff (a x : ℕ) : a ∈ ((nil △[x] nil)) ↔ a = x := by
   constructor
   · intro h
@@ -184,9 +181,6 @@ theorem contains_iff {α : Type u} [inst : BEq α] [inst_1 : LawfulBEq α]
         assumption
       · right; assumption
 
-/-- Lifts `contains` to a `Decidable` instance for `a ∈ t`.
-    Enables `if a ∈ t then ...` and `decide (a ∈ t)` without any extra proof work.
-    Requires `LawfulBEq` to connect `BEq` to propositional equality. -/
 instance [BEq α] [LawfulBEq α] (a : α) (t : BinaryTree α) : Decidable (a ∈ t)  :=
   decidable_of_iff (t.contains a = true) (t.contains_iff a)
 
@@ -196,7 +190,6 @@ def all (p : α → Bool) : BinaryTree α → Bool
   | nil        => true
   | l △[b] r => p b && all p l && all p r
 
-/-- `all` is sound and complete with respect to `∀ x ∈ t, p x`. -/
 theorem all_iff (p : α → Prop) [inst : DecidablePred p]
   (t : BinaryTree α) : t.all (fun x ↦ p x) = true ↔ ∀ x ∈ t, p x := by
   fun_induction all
@@ -236,17 +229,17 @@ theorem left_node_right_eq_self : ∀ {x : BinaryTree Unit} (_hx : x ≠ nil), x
 
 /-- Inorder traversal into a list: left → node → right. -/
 def toListInOrder : BinaryTree α → List α
-  | .nil          => []
-  | .node v l r   => l.toListInOrder ++ [v] ++ r.toListInOrder
+  | nil          => []
+  | l △[v] r  => l.toListInOrder ++ [v] ++ r.toListInOrder
 
 /-- Preorder traversal  into a list: node → left → right. -/
 def toListPreOrder : BinaryTree α → List α
-  | .nil          => []
-  | .node v l r   => [v] ++ l.toListPreOrder ++ r.toListPreOrder
+  | nil          => []
+  | l △[v] r  => [v] ++ l.toListPreOrder ++ r.toListPreOrder
 
 /-- Postorder traversal  into a list: left → right → node. -/
 def toListPostOrder : BinaryTree α → List α
-  | .nil          => []
-  | .node v l r   => l.toListPostOrder ++ r.toListPostOrder ++ [v]
+  | nil          => []
+  | l △[v] r  => l.toListPostOrder ++ r.toListPostOrder ++ [v]
 
 end BinaryTree

From 3df2975b8cd17450a2b850bf0640b3166e7cded7 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 14:34:31 +0200
Subject: [PATCH 04/37] update

---
 Mathlib/Data/Tree/Basic.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index f8eba6aad43be2..24f7cd6bb49841 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -159,7 +159,7 @@ def contains [BEq α] (t : BinaryTree α) (a : α) :  Bool := match t with
   | l △[b] r => a == b || l.contains a  || r.contains a
 
 /-- `contains` is sound and complete with respect to `Mem`. -/
-theorem contains_iff {α : Type u} [inst : BEq α] [inst_1 : LawfulBEq α]
+theorem contains_iff [BEq α] [LawfulBEq α]
   (a : α) (t : BinaryTree α) : t.contains a = true ↔ a ∈ t := by
   fun_induction contains
   · simp_all only [Bool.false_eq_true, false_iff]
@@ -184,13 +184,13 @@ theorem contains_iff {α : Type u} [inst : BEq α] [inst_1 : LawfulBEq α]
 instance [BEq α] [LawfulBEq α] (a : α) (t : BinaryTree α) : Decidable (a ∈ t)  :=
   decidable_of_iff (t.contains a = true) (t.contains_iff a)
 
-/-- Checks whether a boolean predicate holds for every node in the tree.
+/-- An implementation of checking whether a boolean predicate holds for every node in the tree.
     Traversal order: current node, then left subtree, then right subtree. -/
 def all (p : α → Bool) : BinaryTree α → Bool
   | nil        => true
   | l △[b] r => p b && all p l && all p r
 
-theorem all_iff (p : α → Prop) [inst : DecidablePred p]
+theorem all_iff (p : α → Prop) [DecidablePred p]
   (t : BinaryTree α) : t.all (fun x ↦ p x) = true ↔ ∀ x ∈ t, p x := by
   fun_induction all
   · simp only [true_iff]; intros; contradiction

From 89256ddadb966cf92b629ef2321b99221735b689 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 14:41:04 +0200
Subject: [PATCH 05/37] minor

---
 Mathlib/Data/Tree/Basic.lean | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 24f7cd6bb49841..46b915cd399b8f 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -11,13 +11,14 @@ public import Mathlib.Util.CompileInductive
 /-!
 # BinaryTree
 
-Provides binary BinaryTree storage for values of any type, with O(lg n) retrieval.
+Provides binary tree storage for values of any type.
 See also `Lean.Data.RBBinaryTree` for red-black BinaryTrees - this version allows more operations
 to be defined and is better suited for in-kernel computation.
 
 We also specialize for `BinaryTree Unit`, which is a binary BinaryTree without any
 additional data. We provide the notation `a △ b` for making a `BinaryTree Unit` with children
-`a` and `b`.
+`a` and `b`, and the notation `l △[a] r` for a binary tree with root node
+containing value `a` and two children `l` and `r`.
 
 ## References
 
@@ -125,13 +126,13 @@ def right : BinaryTree α → BinaryTree α
 /-- A node with `Unit` data -/
 scoped infixr:65 " △ " => BinaryTree.node ()
 
-/-- A tree node -/
+/-- A notation for a tree node -/
 scoped notation:65 l:66 " △[" v "] " r:66 => BinaryTree.node v l r
 
 /--
 BinaryTree membership, typically accessed via the `∈` operator.
 
-`a ∈ T` means that `a` is an element of the binary tree `T`.
+`a ∈ t` means that `a` is an element of the binary tree `t`.
 Elements are compared according to Lean's logical equality.
 
 Examples:
@@ -154,6 +155,7 @@ theorem mem_singleton_iff (a x : ℕ) : a ∈ ((nil △[x] nil)) ↔ a = x := by
     subst h
     apply Mem.node
 
+/-- In a binary tree, `contains` operation traverses over the tree and make equality check. -/
 def contains [BEq α] (t : BinaryTree α) (a : α) :  Bool := match t with
   | .nil        => false
   | l △[b] r => a == b || l.contains a  || r.contains a

From 7d8e49d8cedb9105360da91e00c3d2536de880f9 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 15:58:31 +0200
Subject: [PATCH 06/37] change Tree to BinaryTree

---
 docs/overview.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/overview.yaml b/docs/overview.yaml
index 7bce34eccd4bcb..54506859354537 100644
--- a/docs/overview.yaml
+++ b/docs/overview.yaml
@@ -589,7 +589,7 @@ Data structures:
     finite map: 'Finmap'
 
   Trees:
-    tree: 'Tree'
+    tree: 'BinaryTree'
     red-black tree: 'Batteries.RBSet'
     size-balanced binary search tree: 'Ordnode'
     W type: 'WType'

From a8a24c138124febae4120255cb44045eda2f06d2 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 16:23:53 +0200
Subject: [PATCH 07/37] rename branch

---
 Mathlib/Data/Tree/Basic.lean | 108 -----------------------------------
 1 file changed, 108 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 46b915cd399b8f..5863efd31bb5f0 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -126,98 +126,6 @@ def right : BinaryTree α → BinaryTree α
 /-- A node with `Unit` data -/
 scoped infixr:65 " △ " => BinaryTree.node ()
 
-/-- A notation for a tree node -/
-scoped notation:65 l:66 " △[" v "] " r:66 => BinaryTree.node v l r
-
-/--
-BinaryTree membership, typically accessed via the `∈` operator.
-
-`a ∈ t` means that `a` is an element of the binary tree `t`.
-Elements are compared according to Lean's logical equality.
-
-Examples:
-* `a ∈ ((nil △[x] nil) △[y] nil) ↔ a = x ∨ a = y`
--/
-inductive Mem (a : α) : BinaryTree α → Prop
-| node  {l r}   : Mem a (l △[a] r)
-| left  (b : α) {l r} : Mem a l → Mem a (l △[b] r)
-| right (b : α) {l r} : Mem a r → Mem a (l △[b] r)
-
-/-- Defines the `∈` notation for `BinaryTree`. -/
-instance : Membership α (BinaryTree α) where
-  mem l a := Mem a l
-
-theorem mem_singleton_iff (a x : ℕ) : a ∈ ((nil △[x] nil)) ↔ a = x := by
-  constructor
-  · intro h
-    cases h <;> trivial
-  · intro h
-    subst h
-    apply Mem.node
-
-/-- In a binary tree, `contains` operation traverses over the tree and make equality check. -/
-def contains [BEq α] (t : BinaryTree α) (a : α) :  Bool := match t with
-  | .nil        => false
-  | l △[b] r => a == b || l.contains a  || r.contains a
-
-/-- `contains` is sound and complete with respect to `Mem`. -/
-theorem contains_iff [BEq α] [LawfulBEq α]
-  (a : α) (t : BinaryTree α) : t.contains a = true ↔ a ∈ t := by
-  fun_induction contains
-  · simp_all only [Bool.false_eq_true, false_iff]
-    false_or_by_contra
-    expose_names
-    cases h
-  · expose_names
-    simp only [Bool.or_eq_true, beq_iff_eq, ih2, ih1]
-    constructor
-    · rintro ( ⟨h | h⟩ | h)
-      · subst h; exact .node
-      · exact .left a_1 h
-      · exact .right a_1 h
-    · intro h
-      cases h
-      · grind
-      · left
-        right
-        assumption
-      · right; assumption
-
-instance [BEq α] [LawfulBEq α] (a : α) (t : BinaryTree α) : Decidable (a ∈ t)  :=
-  decidable_of_iff (t.contains a = true) (t.contains_iff a)
-
-/-- An implementation of checking whether a boolean predicate holds for every node in the tree.
-    Traversal order: current node, then left subtree, then right subtree. -/
-def all (p : α → Bool) : BinaryTree α → Bool
-  | nil        => true
-  | l △[b] r => p b && all p l && all p r
-
-theorem all_iff (p : α → Prop) [DecidablePred p]
-  (t : BinaryTree α) : t.all (fun x ↦ p x) = true ↔ ∀ x ∈ t, p x := by
-  fun_induction all
-  · simp only [true_iff]; intros; contradiction
-  · expose_names
-    simp only [Bool.and_eq_true, decide_eq_true_eq, ih2, ih1]
-    constructor
-    · rintro ⟨⟨h1,h3⟩,h2⟩ x hx
-      cases hx
-      · assumption
-      · expose_names
-        apply h3
-        exact h
-      · expose_names
-        apply h2
-        exact h
-    · intro h
-      exact ⟨⟨h a .node,
-        fun x m => h x (.left a m)⟩,
-        fun x m => h x (.right a m)⟩
-
-/-- `Decidable` instance for bounded universal quantification over a `BinaryTree`. -/
-instance decidableBAll (p : α → Prop) [DecidablePred p] (t : BinaryTree α) :
-    Decidable (∀ x ∈ t, p x) :=
-      decidable_of_iff (t.all (fun x => p x)) (all_iff p t)
-
 /-- Induction principle for `BinaryTree Unit`s -/
 @[elab_as_elim]
 def unitRecOn {motive : BinaryTree Unit → Sort*} (t : BinaryTree Unit) (base : motive nil)
@@ -228,20 +136,4 @@ theorem left_node_right_eq_self : ∀ {x : BinaryTree Unit} (_hx : x ≠ nil), x
   | nil, h => by trivial
   | node _ _ _, _ => rfl  -- Porting note: `a △ b` no longer works in pattern matching
 
-
-/-- Inorder traversal into a list: left → node → right. -/
-def toListInOrder : BinaryTree α → List α
-  | nil          => []
-  | l △[v] r  => l.toListInOrder ++ [v] ++ r.toListInOrder
-
-/-- Preorder traversal  into a list: node → left → right. -/
-def toListPreOrder : BinaryTree α → List α
-  | nil          => []
-  | l △[v] r  => [v] ++ l.toListPreOrder ++ r.toListPreOrder
-
-/-- Postorder traversal  into a list: left → right → node. -/
-def toListPostOrder : BinaryTree α → List α
-  | nil          => []
-  | l △[v] r  => l.toListPostOrder ++ r.toListPostOrder ++ [v]
-
 end BinaryTree

From 8e7291a87b54e24ccc0c1ab14e6e89a97823f87b Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 16:31:48 +0200
Subject: [PATCH 08/37] ensure only rename

---
 Mathlib/Data/Tree/Basic.lean | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 5863efd31bb5f0..478158a40f2167 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -12,13 +12,12 @@ public import Mathlib.Util.CompileInductive
 # BinaryTree
 
 Provides binary tree storage for values of any type.
-See also `Lean.Data.RBBinaryTree` for red-black BinaryTrees - this version allows more operations
+See also `Lean.Data.RBTree` for red-black trees - this version allows more operations
 to be defined and is better suited for in-kernel computation.
 
-We also specialize for `BinaryTree Unit`, which is a binary BinaryTree without any
+We also specialize for `BinaryTree Unit`, which is a binary tree without any
 additional data. We provide the notation `a △ b` for making a `BinaryTree Unit` with children
-`a` and `b`, and the notation `l △[a] r` for a binary tree with root node
-containing value `a` and two children `l` and `r`.
+`a` and `b`.
 
 ## References
 
@@ -28,7 +27,7 @@ containing value `a` and two children `l` and `r`.
 @[expose] public section
 
 
-/-- A binary BinaryTree with values stored in non-leaf nodes. -/
+/-- A binary tree with values stored in non-leaf nodes. -/
 inductive BinaryTree.{u} (α : Type u) : Type u
   | nil : BinaryTree α
   | node (value : α) (left : BinaryTree α) (right : BinaryTree α) : BinaryTree α
@@ -46,8 +45,8 @@ instance : Inhabited (BinaryTree α) :=
 
 
 /--
-Do an action for every node of the BinaryTree.
-Actions are taken in node -> left subBinaryTree -> right subBinaryTree recursive order.
+Do an action for every node of the tree.
+Actions are taken in node -> left subtree -> right subtree recursive order.
 This function is the `traverse` function for the `Traversable BinaryTree` instance.
 -/
 def traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β)
@@ -80,19 +79,19 @@ theorem traverse_pure (t : BinaryTree α) {m : Type u → Type*} [Applicative m]
   | node v l r hl hr =>
     rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]
 
-/-- The number of internal nodes (i.e. not including leaves) of a binary BinaryTree -/
+/-- The number of internal nodes (i.e. not including leaves) of a binary tree -/
 @[simp]
 def numNodes : BinaryTree α → ℕ
   | nil => 0
   | node _ a b => a.numNodes + b.numNodes + 1
 
-/-- The number of leaves of a binary BinaryTree -/
+/-- The number of leaves of a binary tree -/
 @[simp]
 def numLeaves : BinaryTree α → ℕ
   | nil => 1
   | node _ a b => a.numLeaves + b.numLeaves
 
-/-- The height - length of the longest path from the root - of a binary BinaryTree -/
+/-- The height - length of the longest path from the root - of a binary tree -/
 @[simp]
 def height : BinaryTree α → ℕ
   | nil => 0
@@ -111,13 +110,13 @@ theorem height_le_numNodes : ∀ x : BinaryTree α, x.height ≤ x.numNodes
     Nat.max_le.2 ⟨Nat.le_trans a.height_le_numNodes <| a.numNodes.le_add_right _,
       Nat.le_trans b.height_le_numNodes <| b.numNodes.le_add_left _⟩
 
-/-- The left child of the BinaryTree, or `nil` if the BinaryTree is `nil` -/
+/-- The left child of the tree, or `nil` if the tree is `nil` -/
 @[simp]
 def left : BinaryTree α → BinaryTree α
   | nil => nil
   | node _ l _r => l
 
-/-- The right child of the BinaryTree, or `nil` if the BinaryTree is `nil` -/
+/-- The right child of the tree, or `nil` if the tree is `nil` -/
 @[simp]
 def right : BinaryTree α → BinaryTree α
   | nil => nil

From 0fcd3b0e40ca2c23a8cb0f0fafcc684cfddbdd8e Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 16:34:21 +0200
Subject: [PATCH 09/37] minor

---
 Mathlib/Data/Tree/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 478158a40f2167..029359c3b51683 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 mathlib community. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Wojciech Nawrocki, Sorrachai Yingchareonthawornchai
+Authors: Mario Carneiro, Wojciech Nawrocki
 -/
 module
 

From c14add8a21c7764696d3ff4db475177f5b1f266c Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 17:17:01 +0200
Subject: [PATCH 10/37] add deprecated tags

---
 Mathlib/Data/Tree/Basic.lean | 40 ++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 029359c3b51683..a10e3af60022df 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -34,6 +34,17 @@ inductive BinaryTree.{u} (α : Type u) : Type u
   deriving DecidableEq, Repr
 compile_inductive% BinaryTree
 
+@[deprecated BinaryTree (since := "2026-05-22")]
+abbrev Tree.{u} (α : Type u) : Type u := BinaryTree α
+
+@[deprecated BinaryTree.nil (since := "2026-05-22")]
+abbrev Tree.leaf.{u} {α : Type u} : BinaryTree α := BinaryTree.nil
+
+@[deprecated BinaryTree.node (since := "2026-05-22")]
+abbrev Tree.node.{u} {α : Type u} (value : α) (left : BinaryTree α) (right : BinaryTree α)
+: BinaryTree α :=
+  BinaryTree.node value left right
+
 namespace BinaryTree
 
 universe u
@@ -54,6 +65,11 @@ def traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β)
   | .nil => pure nil
   | .node a l r => .node <$> f a <*> traverse f l <*> traverse f r
 
+@[deprecated BinaryTree.traverse (since := "2026-05-22")]
+abbrev Tree.traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β)
+(t : BinaryTree α) : m (BinaryTree β) :=
+  BinaryTree.traverse f t
+
 /-- Apply a function to each value in the BinaryTree.
 This is the `map` function for the `BinaryTree` functor.
 -/
@@ -61,6 +77,9 @@ def map {β} (f : α → β) : BinaryTree α → BinaryTree β
   | nil => nil
   | node a l r => node (f a) (map f l) (map f r)
 
+@[deprecated BinaryTree.map (since := "2026-05-22")]
+abbrev Tree.map {α β} (f : α → β) (t : BinaryTree α) : BinaryTree β := BinaryTree.map f t
+
 theorem id_map (t : BinaryTree α) : t.map id = t := by
   induction t with
   | nil => rw [map]
@@ -85,18 +104,28 @@ def numNodes : BinaryTree α → ℕ
   | nil => 0
   | node _ a b => a.numNodes + b.numNodes + 1
 
+@[deprecated BinaryTree.numNodes (since := "2026-05-22")]
+abbrev Tree.numNodes {α} (t : BinaryTree α) : ℕ := BinaryTree.numNodes t
+
 /-- The number of leaves of a binary tree -/
 @[simp]
 def numLeaves : BinaryTree α → ℕ
   | nil => 1
   | node _ a b => a.numLeaves + b.numLeaves
 
+@[deprecated BinaryTree.numLeaves (since := "2026-05-22")]
+abbrev Tree.numLeaves {α} (t : BinaryTree α) : ℕ := BinaryTree.numLeaves t
+
+
 /-- The height - length of the longest path from the root - of a binary tree -/
 @[simp]
 def height : BinaryTree α → ℕ
   | nil => 0
   | node _ a b => max a.height b.height + 1
 
+@[deprecated BinaryTree.height (since := "2026-05-22")]
+abbrev Tree.height {α} (t : BinaryTree α) : ℕ := BinaryTree.height t
+
 theorem numLeaves_eq_numNodes_succ (x : BinaryTree α) : x.numLeaves = x.numNodes + 1 := by
   induction x <;> simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]
 
@@ -116,12 +145,18 @@ def left : BinaryTree α → BinaryTree α
   | nil => nil
   | node _ l _r => l
 
+@[deprecated BinaryTree.left (since := "2026-05-22")]
+abbrev Tree.left {α} (t : BinaryTree α) : BinaryTree α := BinaryTree.left t
+
 /-- The right child of the tree, or `nil` if the tree is `nil` -/
 @[simp]
 def right : BinaryTree α → BinaryTree α
   | nil => nil
   | node _ _l r => r
 
+@[deprecated BinaryTree.right (since := "2026-05-22")]
+abbrev Tree.right {α} (t : BinaryTree α) : BinaryTree α := BinaryTree.right t
+
 /-- A node with `Unit` data -/
 scoped infixr:65 " △ " => BinaryTree.node ()
 
@@ -131,6 +166,11 @@ def unitRecOn {motive : BinaryTree Unit → Sort*} (t : BinaryTree Unit) (base :
     (ind : ∀ x y, motive x → motive y → motive (x △ y)) : motive t :=
   t.recOn base fun _u ↦ ind
 
+@[deprecated BinaryTree.unitRecOn (since := "2026-05-22")]
+abbrev Tree.unitRecOn {motive : BinaryTree Unit → Sort*} (t : BinaryTree Unit) (base : motive nil)
+    (ind : ∀ x y, motive x → motive y → motive (x △ y)) : motive t :=
+  BinaryTree.unitRecOn t base ind
+
 theorem left_node_right_eq_self : ∀ {x : BinaryTree Unit} (_hx : x ≠ nil), x.left △ x.right = x
   | nil, h => by trivial
   | node _ _ _, _ => rfl  -- Porting note: `a △ b` no longer works in pattern matching

From 53b1d9b40ac2b75dbe0c5528c19fd00c53325484 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 17:32:55 +0200
Subject: [PATCH 11/37] Update Mathlib/Data/Tree/Basic.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Data/Tree/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index a10e3af60022df..3b8fd291ca3284 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -66,7 +66,7 @@ def traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β)
   | .node a l r => .node <$> f a <*> traverse f l <*> traverse f r
 
 @[deprecated BinaryTree.traverse (since := "2026-05-22")]
-abbrev Tree.traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β)
+abbrev _root_.Tree.traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β)
 (t : BinaryTree α) : m (BinaryTree β) :=
   BinaryTree.traverse f t
 

From 1e415ba0c326679283541128012d040a063a0b43 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 17:34:15 +0200
Subject: [PATCH 12/37] Update Mathlib/Data/Tree/Basic.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Data/Tree/Basic.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 3b8fd291ca3284..4d399a16e57bab 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -38,11 +38,11 @@ compile_inductive% BinaryTree
 abbrev Tree.{u} (α : Type u) : Type u := BinaryTree α
 
 @[deprecated BinaryTree.nil (since := "2026-05-22")]
-abbrev Tree.leaf.{u} {α : Type u} : BinaryTree α := BinaryTree.nil
+abbrev Tree.leaf.{u} {α : Type u} : Tree α := BinaryTree.nil
 
 @[deprecated BinaryTree.node (since := "2026-05-22")]
-abbrev Tree.node.{u} {α : Type u} (value : α) (left : BinaryTree α) (right : BinaryTree α)
-: BinaryTree α :=
+abbrev Tree.node.{u} {α : Type u} (value : α) (left : Tree α) (right : Tree α)
+: Tree α :=
   BinaryTree.node value left right
 
 namespace BinaryTree

From d585249a9474b1dc292b102ed82b7ff54d12065b Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 17:38:24 +0200
Subject: [PATCH 13/37] update

---
 Mathlib/Data/Tree/Basic.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 4d399a16e57bab..2d89b24a1177a0 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -38,7 +38,7 @@ compile_inductive% BinaryTree
 abbrev Tree.{u} (α : Type u) : Type u := BinaryTree α
 
 @[deprecated BinaryTree.nil (since := "2026-05-22")]
-abbrev Tree.leaf.{u} {α : Type u} : Tree α := BinaryTree.nil
+abbrev Tree.nil.{u} {α : Type u} : Tree α := BinaryTree.nil
 
 @[deprecated BinaryTree.node (since := "2026-05-22")]
 abbrev Tree.node.{u} {α : Type u} (value : α) (left : Tree α) (right : Tree α)
@@ -78,7 +78,7 @@ def map {β} (f : α → β) : BinaryTree α → BinaryTree β
   | node a l r => node (f a) (map f l) (map f r)
 
 @[deprecated BinaryTree.map (since := "2026-05-22")]
-abbrev Tree.map {α β} (f : α → β) (t : BinaryTree α) : BinaryTree β := BinaryTree.map f t
+abbrev Tree.map {α β} (f : α → β) (t : Tree α) : Tree β := BinaryTree.map f t
 
 theorem id_map (t : BinaryTree α) : t.map id = t := by
   induction t with
@@ -105,7 +105,7 @@ def numNodes : BinaryTree α → ℕ
   | node _ a b => a.numNodes + b.numNodes + 1
 
 @[deprecated BinaryTree.numNodes (since := "2026-05-22")]
-abbrev Tree.numNodes {α} (t : BinaryTree α) : ℕ := BinaryTree.numNodes t
+abbrev Tree.numNodes {α} (t : Tree α) : ℕ := BinaryTree.numNodes t
 
 /-- The number of leaves of a binary tree -/
 @[simp]
@@ -114,7 +114,7 @@ def numLeaves : BinaryTree α → ℕ
   | node _ a b => a.numLeaves + b.numLeaves
 
 @[deprecated BinaryTree.numLeaves (since := "2026-05-22")]
-abbrev Tree.numLeaves {α} (t : BinaryTree α) : ℕ := BinaryTree.numLeaves t
+abbrev Tree.numLeaves {α} (t : Tree α) : ℕ := BinaryTree.numLeaves t
 
 
 /-- The height - length of the longest path from the root - of a binary tree -/
@@ -124,7 +124,7 @@ def height : BinaryTree α → ℕ
   | node _ a b => max a.height b.height + 1
 
 @[deprecated BinaryTree.height (since := "2026-05-22")]
-abbrev Tree.height {α} (t : BinaryTree α) : ℕ := BinaryTree.height t
+abbrev Tree.height {α} (t : Tree α) : ℕ := BinaryTree.height t
 
 theorem numLeaves_eq_numNodes_succ (x : BinaryTree α) : x.numLeaves = x.numNodes + 1 := by
   induction x <;> simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]
@@ -146,7 +146,7 @@ def left : BinaryTree α → BinaryTree α
   | node _ l _r => l
 
 @[deprecated BinaryTree.left (since := "2026-05-22")]
-abbrev Tree.left {α} (t : BinaryTree α) : BinaryTree α := BinaryTree.left t
+abbrev Tree.left {α} (t : Tree α) : Tree α := BinaryTree.left t
 
 /-- The right child of the tree, or `nil` if the tree is `nil` -/
 @[simp]
@@ -155,7 +155,7 @@ def right : BinaryTree α → BinaryTree α
   | node _ _l r => r
 
 @[deprecated BinaryTree.right (since := "2026-05-22")]
-abbrev Tree.right {α} (t : BinaryTree α) : BinaryTree α := BinaryTree.right t
+abbrev Tree.right {α} (t : Tree α) : Tree α := BinaryTree.right t
 
 /-- A node with `Unit` data -/
 scoped infixr:65 " △ " => BinaryTree.node ()
@@ -167,7 +167,7 @@ def unitRecOn {motive : BinaryTree Unit → Sort*} (t : BinaryTree Unit) (base :
   t.recOn base fun _u ↦ ind
 
 @[deprecated BinaryTree.unitRecOn (since := "2026-05-22")]
-abbrev Tree.unitRecOn {motive : BinaryTree Unit → Sort*} (t : BinaryTree Unit) (base : motive nil)
+abbrev Tree.unitRecOn {motive : Tree Unit → Sort*} (t : Tree Unit) (base : motive nil)
     (ind : ∀ x y, motive x → motive y → motive (x △ y)) : motive t :=
   BinaryTree.unitRecOn t base ind
 

From 8cef6431da0119071268146cb8919209755ac132 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 18:10:26 +0200
Subject: [PATCH 14/37] depreciate Get.lean

---
 Mathlib/Data/Tree/Basic.lean |  2 +-
 Mathlib/Data/Tree/Get.lean   | 14 ++++++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 2d89b24a1177a0..bc6caea54135c9 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -9,7 +9,7 @@ public import Mathlib.Data.Nat.Notation
 public import Mathlib.Util.CompileInductive
 
 /-!
-# BinaryTree
+# Binary tree
 
 Provides binary tree storage for values of any type.
 See also `Lean.Data.RBTree` for red-black trees - this version allows more operations
diff --git a/Mathlib/Data/Tree/Get.lean b/Mathlib/Data/Tree/Get.lean
index 694cced303f163..3be150a6254862 100644
--- a/Mathlib/Data/Tree/Get.lean
+++ b/Mathlib/Data/Tree/Get.lean
@@ -38,6 +38,12 @@ def indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : BinaryTree α
     | Ordering.eq => some PosNum.one
     | Ordering.gt => PosNum.bit1 <$> indexOf lt x t₂
 
+
+@[deprecated BinaryTree.indexOf (since := "2026-05-22")]
+abbrev Tree.indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : Tree α →  Option PosNum :=
+  BinaryTree.indexOf lt x
+
+
 /-- Retrieves an element uniquely determined by a `PosNum` from the tree,
 taking the following path to get to the element:
 - `bit0` - go to left child
@@ -49,9 +55,17 @@ def get : PosNum → BinaryTree α → Option α
   | PosNum.bit0 n, node _a t₁ _t₂ => t₁.get n
   | PosNum.bit1 n, node _a _t₁ t₂ => t₂.get n
 
+@[deprecated BinaryTree.get (since := "2026-05-22")]
+abbrev Tree.get (n : PosNum) (t : Tree α) : Option α :=
+  BinaryTree.get n t
+
 /-- Retrieves an element from the tree, or the provided default value
 if the index is invalid. See `Tree.get`. -/
 def getOrElse (n : PosNum) (t : BinaryTree α) (v : α) : α :=
   (t.get n).getD v
 
+@[deprecated BinaryTree.getOrElse (since := "2026-05-22")]
+abbrev Tree.getOrElse (n : PosNum) (t : Tree α) (v : α) : α :=
+  BinaryTree.getOrElse n t v
+
 end BinaryTree

From b01599b86f32dbd9dfee6d06096ff0917e242470 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 18:23:08 +0200
Subject: [PATCH 15/37] minor

---
 Mathlib/Data/Tree/Get.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/Tree/Get.lean b/Mathlib/Data/Tree/Get.lean
index 3be150a6254862..4eaca1b717d403 100644
--- a/Mathlib/Data/Tree/Get.lean
+++ b/Mathlib/Data/Tree/Get.lean
@@ -40,7 +40,7 @@ def indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : BinaryTree α
 
 
 @[deprecated BinaryTree.indexOf (since := "2026-05-22")]
-abbrev Tree.indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : Tree α →  Option PosNum :=
+abbrev _root_.Tree.indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : Tree α →  Option PosNum :=
   BinaryTree.indexOf lt x
 
 
@@ -56,7 +56,7 @@ def get : PosNum → BinaryTree α → Option α
   | PosNum.bit1 n, node _a _t₁ t₂ => t₂.get n
 
 @[deprecated BinaryTree.get (since := "2026-05-22")]
-abbrev Tree.get (n : PosNum) (t : Tree α) : Option α :=
+abbrev _root_.Tree.get (n : PosNum) (t : Tree α) : Option α :=
   BinaryTree.get n t
 
 /-- Retrieves an element from the tree, or the provided default value
@@ -65,7 +65,7 @@ def getOrElse (n : PosNum) (t : BinaryTree α) (v : α) : α :=
   (t.get n).getD v
 
 @[deprecated BinaryTree.getOrElse (since := "2026-05-22")]
-abbrev Tree.getOrElse (n : PosNum) (t : Tree α) (v : α) : α :=
+abbrev _root_.Tree.getOrElse (n : PosNum) (t : Tree α) (v : α) : α :=
   BinaryTree.getOrElse n t v
 
 end BinaryTree

From c371e4f7bdb639f5f4319eb613c6398ee6ba5a46 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 20:51:13 +0200
Subject: [PATCH 16/37] Update Mathlib/Data/Tree/Basic.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Data/Tree/Basic.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index bc6caea54135c9..4c2db0a51b4b0d 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -54,7 +54,6 @@ variable {α : Type u}
 instance : Inhabited (BinaryTree α) :=
   ⟨nil⟩
 
-
 /--
 Do an action for every node of the tree.
 Actions are taken in node -> left subtree -> right subtree recursive order.

From 66042ed87599190a18bc169d9851d7f281b7450f Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 20:51:23 +0200
Subject: [PATCH 17/37] Update Mathlib/Data/Tree/Basic.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Data/Tree/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 4c2db0a51b4b0d..bf2c4aa1256b51 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -104,7 +104,7 @@ def numNodes : BinaryTree α → ℕ
   | node _ a b => a.numNodes + b.numNodes + 1
 
 @[deprecated BinaryTree.numNodes (since := "2026-05-22")]
-abbrev Tree.numNodes {α} (t : Tree α) : ℕ := BinaryTree.numNodes t
+abbrev _root_.Tree.numNodes {α} (t : Tree α) : ℕ := BinaryTree.numNodes t
 
 /-- The number of leaves of a binary tree -/
 @[simp]

From 2f12a7254057f69a48bc8832aa299d5f388c62ab Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 20:54:57 +0200
Subject: [PATCH 18/37] add _root_

---
 Mathlib/Data/Tree/Basic.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index bf2c4aa1256b51..4f92f281ccc657 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -113,7 +113,7 @@ def numLeaves : BinaryTree α → ℕ
   | node _ a b => a.numLeaves + b.numLeaves
 
 @[deprecated BinaryTree.numLeaves (since := "2026-05-22")]
-abbrev Tree.numLeaves {α} (t : Tree α) : ℕ := BinaryTree.numLeaves t
+abbrev _root_.Tree.numLeaves {α} (t : Tree α) : ℕ := BinaryTree.numLeaves t
 
 
 /-- The height - length of the longest path from the root - of a binary tree -/
@@ -123,7 +123,7 @@ def height : BinaryTree α → ℕ
   | node _ a b => max a.height b.height + 1
 
 @[deprecated BinaryTree.height (since := "2026-05-22")]
-abbrev Tree.height {α} (t : Tree α) : ℕ := BinaryTree.height t
+abbrev _root_.Tree.height {α} (t : Tree α) : ℕ := BinaryTree.height t
 
 theorem numLeaves_eq_numNodes_succ (x : BinaryTree α) : x.numLeaves = x.numNodes + 1 := by
   induction x <;> simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]
@@ -145,7 +145,7 @@ def left : BinaryTree α → BinaryTree α
   | node _ l _r => l
 
 @[deprecated BinaryTree.left (since := "2026-05-22")]
-abbrev Tree.left {α} (t : Tree α) : Tree α := BinaryTree.left t
+abbrev _root_.Tree.left {α} (t : Tree α) : Tree α := BinaryTree.left t
 
 /-- The right child of the tree, or `nil` if the tree is `nil` -/
 @[simp]
@@ -154,7 +154,7 @@ def right : BinaryTree α → BinaryTree α
   | node _ _l r => r
 
 @[deprecated BinaryTree.right (since := "2026-05-22")]
-abbrev Tree.right {α} (t : Tree α) : Tree α := BinaryTree.right t
+abbrev _root_.Tree.right {α} (t : Tree α) : Tree α := BinaryTree.right t
 
 /-- A node with `Unit` data -/
 scoped infixr:65 " △ " => BinaryTree.node ()
@@ -166,7 +166,7 @@ def unitRecOn {motive : BinaryTree Unit → Sort*} (t : BinaryTree Unit) (base :
   t.recOn base fun _u ↦ ind
 
 @[deprecated BinaryTree.unitRecOn (since := "2026-05-22")]
-abbrev Tree.unitRecOn {motive : Tree Unit → Sort*} (t : Tree Unit) (base : motive nil)
+abbrev _root_.Tree.unitRecOn {motive : Tree Unit → Sort*} (t : Tree Unit) (base : motive nil)
     (ind : ∀ x y, motive x → motive y → motive (x △ y)) : motive t :=
   BinaryTree.unitRecOn t base ind
 

From 80820ad4749b66f4f5fb252f8ebb19559cea6b81 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 20:56:08 +0200
Subject: [PATCH 19/37] restore docstring

---
 Mathlib/Data/Tree/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 4f92f281ccc657..04d092f5a9cd19 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -11,7 +11,7 @@ public import Mathlib.Util.CompileInductive
 /-!
 # Binary tree
 
-Provides binary tree storage for values of any type.
+Provides binary tree storage for values of any type, with O(lg n) retrieval.
 See also `Lean.Data.RBTree` for red-black trees - this version allows more operations
 to be defined and is better suited for in-kernel computation.
 

From 38279ef5be97f9a31c444d8c5a587f553af17891 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 20:57:18 +0200
Subject: [PATCH 20/37] minor

---
 Mathlib/Data/Tree/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 04d092f5a9cd19..deb50814917d02 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -77,7 +77,7 @@ def map {β} (f : α → β) : BinaryTree α → BinaryTree β
   | node a l r => node (f a) (map f l) (map f r)
 
 @[deprecated BinaryTree.map (since := "2026-05-22")]
-abbrev Tree.map {α β} (f : α → β) (t : Tree α) : Tree β := BinaryTree.map f t
+abbrev _root_.Tree.map {α β} (f : α → β) (t : Tree α) : Tree β := BinaryTree.map f t
 
 theorem id_map (t : BinaryTree α) : t.map id = t := by
   induction t with

From b4160afd28250f5d0558c23036da72ded0934984 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 21:29:49 +0200
Subject: [PATCH 21/37] add docstring

---
 Mathlib/Data/Tree/Basic.lean | 14 ++++++++++++++
 Mathlib/Data/Tree/Get.lean   | 16 +++++++++++++---
 2 files changed, 27 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index deb50814917d02..678e6646b6cff0 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -64,6 +64,11 @@ def traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β)
   | .nil => pure nil
   | .node a l r => .node <$> f a <*> traverse f l <*> traverse f r
 
+/--
+Do an action for every node of the tree.
+Actions are taken in node -> left subtree -> right subtree recursive order.
+This function is the `traverse` function for the `Traversable BinaryTree` instance.
+-/
 @[deprecated BinaryTree.traverse (since := "2026-05-22")]
 abbrev _root_.Tree.traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β)
 (t : BinaryTree α) : m (BinaryTree β) :=
@@ -76,6 +81,9 @@ def map {β} (f : α → β) : BinaryTree α → BinaryTree β
   | nil => nil
   | node a l r => node (f a) (map f l) (map f r)
 
+/-- Apply a function to each value in the BinaryTree.
+This is the `map` function for the `BinaryTree` functor.
+-/
 @[deprecated BinaryTree.map (since := "2026-05-22")]
 abbrev _root_.Tree.map {α β} (f : α → β) (t : Tree α) : Tree β := BinaryTree.map f t
 
@@ -103,6 +111,7 @@ def numNodes : BinaryTree α → ℕ
   | nil => 0
   | node _ a b => a.numNodes + b.numNodes + 1
 
+/-- The number of internal nodes (i.e. not including leaves) of a binary tree -/
 @[deprecated BinaryTree.numNodes (since := "2026-05-22")]
 abbrev _root_.Tree.numNodes {α} (t : Tree α) : ℕ := BinaryTree.numNodes t
 
@@ -112,6 +121,7 @@ def numLeaves : BinaryTree α → ℕ
   | nil => 1
   | node _ a b => a.numLeaves + b.numLeaves
 
+/-- The number of leaves of a binary tree -/
 @[deprecated BinaryTree.numLeaves (since := "2026-05-22")]
 abbrev _root_.Tree.numLeaves {α} (t : Tree α) : ℕ := BinaryTree.numLeaves t
 
@@ -122,6 +132,7 @@ def height : BinaryTree α → ℕ
   | nil => 0
   | node _ a b => max a.height b.height + 1
 
+/-- The height - length of the longest path from the root - of a binary tree -/
 @[deprecated BinaryTree.height (since := "2026-05-22")]
 abbrev _root_.Tree.height {α} (t : Tree α) : ℕ := BinaryTree.height t
 
@@ -144,6 +155,7 @@ def left : BinaryTree α → BinaryTree α
   | nil => nil
   | node _ l _r => l
 
+/-- The left child of the tree, or `nil` if the tree is `nil` -/
 @[deprecated BinaryTree.left (since := "2026-05-22")]
 abbrev _root_.Tree.left {α} (t : Tree α) : Tree α := BinaryTree.left t
 
@@ -153,6 +165,7 @@ def right : BinaryTree α → BinaryTree α
   | nil => nil
   | node _ _l r => r
 
+/-- The right child of the tree, or `nil` if the tree is `nil` -/
 @[deprecated BinaryTree.right (since := "2026-05-22")]
 abbrev _root_.Tree.right {α} (t : Tree α) : Tree α := BinaryTree.right t
 
@@ -165,6 +178,7 @@ def unitRecOn {motive : BinaryTree Unit → Sort*} (t : BinaryTree Unit) (base :
     (ind : ∀ x y, motive x → motive y → motive (x △ y)) : motive t :=
   t.recOn base fun _u ↦ ind
 
+/-- Induction principle for `Tree Unit`s -/
 @[deprecated BinaryTree.unitRecOn (since := "2026-05-22")]
 abbrev _root_.Tree.unitRecOn {motive : Tree Unit → Sort*} (t : Tree Unit) (base : motive nil)
     (ind : ∀ x y, motive x → motive y → motive (x △ y)) : motive t :=
diff --git a/Mathlib/Data/Tree/Get.lean b/Mathlib/Data/Tree/Get.lean
index 4eaca1b717d403..dbad9914b7b7ee 100644
--- a/Mathlib/Data/Tree/Get.lean
+++ b/Mathlib/Data/Tree/Get.lean
@@ -38,9 +38,12 @@ def indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : BinaryTree α
     | Ordering.eq => some PosNum.one
     | Ordering.gt => PosNum.bit1 <$> indexOf lt x t₂
 
-
+/-- Finds the index of an element in the tree assuming the tree has been
+constructed according to the provided decidable order on its elements.
+If it hasn't, the result will be incorrect. If it has, but the element
+is not in the tree, returns none. -/
 @[deprecated BinaryTree.indexOf (since := "2026-05-22")]
-abbrev _root_.Tree.indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : Tree α →  Option PosNum :=
+abbrev _root_.Tree.indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : Tree α → Option PosNum :=
   BinaryTree.indexOf lt x
 
 
@@ -55,15 +58,22 @@ def get : PosNum → BinaryTree α → Option α
   | PosNum.bit0 n, node _a t₁ _t₂ => t₁.get n
   | PosNum.bit1 n, node _a _t₁ t₂ => t₂.get n
 
+/-- Retrieves an element uniquely determined by a `PosNum` from the tree,
+taking the following path to get to the element:
+- `bit0` - go to left child
+- `bit1` - go to right child
+- `PosNum.one` - retrieve from here -/
 @[deprecated BinaryTree.get (since := "2026-05-22")]
 abbrev _root_.Tree.get (n : PosNum) (t : Tree α) : Option α :=
   BinaryTree.get n t
 
 /-- Retrieves an element from the tree, or the provided default value
-if the index is invalid. See `Tree.get`. -/
+if the index is invalid. See `BinaryTree.get`. -/
 def getOrElse (n : PosNum) (t : BinaryTree α) (v : α) : α :=
   (t.get n).getD v
 
+/-- Retrieves an element from the tree, or the provided default value
+if the index is invalid. See `Tree.get`. -/
 @[deprecated BinaryTree.getOrElse (since := "2026-05-22")]
 abbrev _root_.Tree.getOrElse (n : PosNum) (t : Tree α) (v : α) : α :=
   BinaryTree.getOrElse n t v

From 9716693acc74f29cd186bee8c98e965adbc4f4a1 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 21:31:25 +0200
Subject: [PATCH 22/37] docstring

---
 Mathlib/Data/Tree/Basic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 678e6646b6cff0..d729d9a279fb28 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -34,12 +34,15 @@ inductive BinaryTree.{u} (α : Type u) : Type u
   deriving DecidableEq, Repr
 compile_inductive% BinaryTree
 
+/-- A binary tree with values stored in non-leaf nodes. -/
 @[deprecated BinaryTree (since := "2026-05-22")]
 abbrev Tree.{u} (α : Type u) : Type u := BinaryTree α
 
+/-- Tree.nil -/
 @[deprecated BinaryTree.nil (since := "2026-05-22")]
 abbrev Tree.nil.{u} {α : Type u} : Tree α := BinaryTree.nil
 
+/-- Tree.node -/
 @[deprecated BinaryTree.node (since := "2026-05-22")]
 abbrev Tree.node.{u} {α : Type u} (value : α) (left : Tree α) (right : Tree α)
 : Tree α :=

From e49e9007e95f76ca883b63355e9d8d606fa5d488 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 22:15:36 +0200
Subject: [PATCH 23/37] remove expose

---
 Mathlib/Data/Tree/Basic.lean | 2 +-
 Mathlib/Data/Tree/Get.lean   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index d729d9a279fb28..cabaf05d9be93e 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -24,7 +24,7 @@ additional data. We provide the notation `a △ b` for making a `BinaryTree Unit
 <https://leanprover-community.github.io/archive/stream/113488-general/topic/tactic.20question.html>
 -/
 
-@[expose] public section
+public section
 
 
 /-- A binary tree with values stored in non-leaf nodes. -/
diff --git a/Mathlib/Data/Tree/Get.lean b/Mathlib/Data/Tree/Get.lean
index dbad9914b7b7ee..fe583c01e60ec1 100644
--- a/Mathlib/Data/Tree/Get.lean
+++ b/Mathlib/Data/Tree/Get.lean
@@ -20,7 +20,7 @@ These definitions were moved from the main file to avoid a dependency on `Num`.
 <https://leanprover-community.github.io/archive/stream/113488-general/topic/tactic.20question.html#170999997>
 -/
 
-@[expose] public section
+public section
 
 namespace BinaryTree
 

From 4cff09e282414547c8218e1cd492ee6f3e41ee44 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 22:16:13 +0200
Subject: [PATCH 24/37] Merge branch 'rename_tree_to_binary_tree' of
 https://github.com/sorrachai/mathlib4 into rename_tree_to_binary_tree


From c2ef00e4a52f06fe2064a8002dbb378252d80ea3 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 22:42:27 +0200
Subject: [PATCH 25/37] Update Mathlib/Data/Tree/Get.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Data/Tree/Get.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Get.lean b/Mathlib/Data/Tree/Get.lean
index fe583c01e60ec1..34ca58eadf0c13 100644
--- a/Mathlib/Data/Tree/Get.lean
+++ b/Mathlib/Data/Tree/Get.lean
@@ -46,7 +46,6 @@ is not in the tree, returns none. -/
 abbrev _root_.Tree.indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : Tree α → Option PosNum :=
   BinaryTree.indexOf lt x
 
-
 /-- Retrieves an element uniquely determined by a `PosNum` from the tree,
 taking the following path to get to the element:
 - `bit0` - go to left child

From b7c505c9f27ec57653d7e60bca17a71b6f1f35c2 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 22:44:16 +0200
Subject: [PATCH 26/37] Update Mathlib/Data/Tree/Basic.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Data/Tree/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index cabaf05d9be93e..d729d9a279fb28 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -24,7 +24,7 @@ additional data. We provide the notation `a △ b` for making a `BinaryTree Unit
 <https://leanprover-community.github.io/archive/stream/113488-general/topic/tactic.20question.html>
 -/
 
-public section
+@[expose] public section
 
 
 /-- A binary tree with values stored in non-leaf nodes. -/

From 4a450d5d1d7c4bda6cb03e874e6912f8e007f8e4 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 22 May 2026 22:45:24 +0200
Subject: [PATCH 27/37] expose

---
 Mathlib/Data/Tree/Get.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Get.lean b/Mathlib/Data/Tree/Get.lean
index 34ca58eadf0c13..d752354af37a90 100644
--- a/Mathlib/Data/Tree/Get.lean
+++ b/Mathlib/Data/Tree/Get.lean
@@ -20,7 +20,7 @@ These definitions were moved from the main file to avoid a dependency on `Num`.
 <https://leanprover-community.github.io/archive/stream/113488-general/topic/tactic.20question.html#170999997>
 -/
 
-public section
+@[expose] public section
 
 namespace BinaryTree
 

From 2b3a4d85ebde989f79265d93e1ab10b2a38c9a16 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Sun, 24 May 2026 16:49:31 +0200
Subject: [PATCH 28/37] locally disable liner

---
 Mathlib/Data/Tree/Basic.lean | 9 +++++++++
 Mathlib/Data/Tree/Get.lean   | 3 +++
 2 files changed, 12 insertions(+)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index d729d9a279fb28..fcda0a40e59d51 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -38,9 +38,11 @@ compile_inductive% BinaryTree
 @[deprecated BinaryTree (since := "2026-05-22")]
 abbrev Tree.{u} (α : Type u) : Type u := BinaryTree α
 
+set_option linter.deprecated false in
 /-- Tree.nil -/
 @[deprecated BinaryTree.nil (since := "2026-05-22")]
 abbrev Tree.nil.{u} {α : Type u} : Tree α := BinaryTree.nil
+set_option linter.deprecated false in
 
 /-- Tree.node -/
 @[deprecated BinaryTree.node (since := "2026-05-22")]
@@ -84,6 +86,7 @@ def map {β} (f : α → β) : BinaryTree α → BinaryTree β
   | nil => nil
   | node a l r => node (f a) (map f l) (map f r)
 
+set_option linter.deprecated false in
 /-- Apply a function to each value in the BinaryTree.
 This is the `map` function for the `BinaryTree` functor.
 -/
@@ -114,6 +117,7 @@ def numNodes : BinaryTree α → ℕ
   | nil => 0
   | node _ a b => a.numNodes + b.numNodes + 1
 
+set_option linter.deprecated false in
 /-- The number of internal nodes (i.e. not including leaves) of a binary tree -/
 @[deprecated BinaryTree.numNodes (since := "2026-05-22")]
 abbrev _root_.Tree.numNodes {α} (t : Tree α) : ℕ := BinaryTree.numNodes t
@@ -124,6 +128,7 @@ def numLeaves : BinaryTree α → ℕ
   | nil => 1
   | node _ a b => a.numLeaves + b.numLeaves
 
+set_option linter.deprecated false in
 /-- The number of leaves of a binary tree -/
 @[deprecated BinaryTree.numLeaves (since := "2026-05-22")]
 abbrev _root_.Tree.numLeaves {α} (t : Tree α) : ℕ := BinaryTree.numLeaves t
@@ -135,6 +140,7 @@ def height : BinaryTree α → ℕ
   | nil => 0
   | node _ a b => max a.height b.height + 1
 
+set_option linter.deprecated false in
 /-- The height - length of the longest path from the root - of a binary tree -/
 @[deprecated BinaryTree.height (since := "2026-05-22")]
 abbrev _root_.Tree.height {α} (t : Tree α) : ℕ := BinaryTree.height t
@@ -158,6 +164,7 @@ def left : BinaryTree α → BinaryTree α
   | nil => nil
   | node _ l _r => l
 
+set_option linter.deprecated false in
 /-- The left child of the tree, or `nil` if the tree is `nil` -/
 @[deprecated BinaryTree.left (since := "2026-05-22")]
 abbrev _root_.Tree.left {α} (t : Tree α) : Tree α := BinaryTree.left t
@@ -168,6 +175,7 @@ def right : BinaryTree α → BinaryTree α
   | nil => nil
   | node _ _l r => r
 
+set_option linter.deprecated false in
 /-- The right child of the tree, or `nil` if the tree is `nil` -/
 @[deprecated BinaryTree.right (since := "2026-05-22")]
 abbrev _root_.Tree.right {α} (t : Tree α) : Tree α := BinaryTree.right t
@@ -181,6 +189,7 @@ def unitRecOn {motive : BinaryTree Unit → Sort*} (t : BinaryTree Unit) (base :
     (ind : ∀ x y, motive x → motive y → motive (x △ y)) : motive t :=
   t.recOn base fun _u ↦ ind
 
+set_option linter.deprecated false in
 /-- Induction principle for `Tree Unit`s -/
 @[deprecated BinaryTree.unitRecOn (since := "2026-05-22")]
 abbrev _root_.Tree.unitRecOn {motive : Tree Unit → Sort*} (t : Tree Unit) (base : motive nil)
diff --git a/Mathlib/Data/Tree/Get.lean b/Mathlib/Data/Tree/Get.lean
index d752354af37a90..45d7f7f4988c80 100644
--- a/Mathlib/Data/Tree/Get.lean
+++ b/Mathlib/Data/Tree/Get.lean
@@ -38,6 +38,7 @@ def indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : BinaryTree α
     | Ordering.eq => some PosNum.one
     | Ordering.gt => PosNum.bit1 <$> indexOf lt x t₂
 
+set_option linter.deprecated false in
 /-- Finds the index of an element in the tree assuming the tree has been
 constructed according to the provided decidable order on its elements.
 If it hasn't, the result will be incorrect. If it has, but the element
@@ -57,6 +58,7 @@ def get : PosNum → BinaryTree α → Option α
   | PosNum.bit0 n, node _a t₁ _t₂ => t₁.get n
   | PosNum.bit1 n, node _a _t₁ t₂ => t₂.get n
 
+set_option linter.deprecated false in
 /-- Retrieves an element uniquely determined by a `PosNum` from the tree,
 taking the following path to get to the element:
 - `bit0` - go to left child
@@ -71,6 +73,7 @@ if the index is invalid. See `BinaryTree.get`. -/
 def getOrElse (n : PosNum) (t : BinaryTree α) (v : α) : α :=
   (t.get n).getD v
 
+set_option linter.deprecated false in
 /-- Retrieves an element from the tree, or the provided default value
 if the index is invalid. See `Tree.get`. -/
 @[deprecated BinaryTree.getOrElse (since := "2026-05-22")]

From 56168ce460ab877f286d247d4f91403fc0a82df5 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Thu, 28 May 2026 12:38:47 +0200
Subject: [PATCH 29/37] Update Mathlib/Data/Tree/Basic.lean

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
---
 Mathlib/Data/Tree/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index fcda0a40e59d51..97180295e222d5 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -42,8 +42,8 @@ set_option linter.deprecated false in
 /-- Tree.nil -/
 @[deprecated BinaryTree.nil (since := "2026-05-22")]
 abbrev Tree.nil.{u} {α : Type u} : Tree α := BinaryTree.nil
-set_option linter.deprecated false in
 
+set_option linter.deprecated false in
 /-- Tree.node -/
 @[deprecated BinaryTree.node (since := "2026-05-22")]
 abbrev Tree.node.{u} {α : Type u} (value : α) (left : Tree α) (right : Tree α)

From b5971803c9e51d5d29b144bbef25365e672852ee Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Thu, 28 May 2026 14:24:51 +0200
Subject: [PATCH 30/37] formatting

---
 Mathlib/Data/Tree/Basic.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 97180295e222d5..583a0306d92d7f 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -104,8 +104,9 @@ theorem comp_map {β γ : Type*} (f : α → β) (g : β → γ) (t : BinaryTree
   | nil => rw [map, map, map]
   | node v l r hl hr => rw [map, map, map, hl, hr, Function.comp_apply]
 
-theorem traverse_pure (t : BinaryTree α) {m : Type u → Type*} [Applicative m] [LawfulApplicative m]
-: t.traverse (pure : α → m α) = pure t := by
+theorem traverse_pure (t : BinaryTree α) {m : Type u → Type*}
+    [Applicative m] [LawfulApplicative m] :
+    t.traverse (pure : α → m α) = pure t := by
   induction t with
   | nil => rw [traverse]
   | node v l r hl hr =>

From bd8e8b0b8a51eee30164793fd6fe7f836ee4c91c Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Mon, 8 Jun 2026 02:14:28 +0000
Subject: [PATCH 31/37] alias docstrings

---
 Mathlib/Data/Tree/Basic.lean | 45 +++++++++++++++++-------------------
 Mathlib/Data/Tree/Get.lean   | 20 +++++-----------
 2 files changed, 27 insertions(+), 38 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 583a0306d92d7f..70205f543a9a02 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -34,18 +34,17 @@ inductive BinaryTree.{u} (α : Type u) : Type u
   deriving DecidableEq, Repr
 compile_inductive% BinaryTree
 
-/-- A binary tree with values stored in non-leaf nodes. -/
-@[deprecated BinaryTree (since := "2026-05-22")]
-abbrev Tree.{u} (α : Type u) : Type u := BinaryTree α
+@[deprecated BinaryTree (since := "2026-06-07"), reducible]
+alias Tree := BinaryTree
 
 set_option linter.deprecated false in
-/-- Tree.nil -/
-@[deprecated BinaryTree.nil (since := "2026-05-22")]
+/-- **Alias** of `BinaryTree.nil`. -/
+@[deprecated BinaryTree.nil (since := "2026-06-07")]
 abbrev Tree.nil.{u} {α : Type u} : Tree α := BinaryTree.nil
 
 set_option linter.deprecated false in
-/-- Tree.node -/
-@[deprecated BinaryTree.node (since := "2026-05-22")]
+/-- **Alias** of `BinaryTree.node`. -/
+@[deprecated BinaryTree.node (since := "2026-06-07")]
 abbrev Tree.node.{u} {α : Type u} (value : α) (left : Tree α) (right : Tree α)
 : Tree α :=
   BinaryTree.node value left right
@@ -74,7 +73,7 @@ Do an action for every node of the tree.
 Actions are taken in node -> left subtree -> right subtree recursive order.
 This function is the `traverse` function for the `Traversable BinaryTree` instance.
 -/
-@[deprecated BinaryTree.traverse (since := "2026-05-22")]
+@[deprecated BinaryTree.traverse (since := "2026-06-07")]
 abbrev _root_.Tree.traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β)
 (t : BinaryTree α) : m (BinaryTree β) :=
   BinaryTree.traverse f t
@@ -87,10 +86,8 @@ def map {β} (f : α → β) : BinaryTree α → BinaryTree β
   | node a l r => node (f a) (map f l) (map f r)
 
 set_option linter.deprecated false in
-/-- Apply a function to each value in the BinaryTree.
-This is the `map` function for the `BinaryTree` functor.
--/
-@[deprecated BinaryTree.map (since := "2026-05-22")]
+/-- **Alias** of `BinaryTree.map`. -/
+@[deprecated BinaryTree.map (since := "2026-06-07")]
 abbrev _root_.Tree.map {α β} (f : α → β) (t : Tree α) : Tree β := BinaryTree.map f t
 
 theorem id_map (t : BinaryTree α) : t.map id = t := by
@@ -119,8 +116,8 @@ def numNodes : BinaryTree α → ℕ
   | node _ a b => a.numNodes + b.numNodes + 1
 
 set_option linter.deprecated false in
-/-- The number of internal nodes (i.e. not including leaves) of a binary tree -/
-@[deprecated BinaryTree.numNodes (since := "2026-05-22")]
+/-- **Alias** of `BinaryTree.numNodes`. -/
+@[deprecated BinaryTree.numNodes (since := "2026-06-07")]
 abbrev _root_.Tree.numNodes {α} (t : Tree α) : ℕ := BinaryTree.numNodes t
 
 /-- The number of leaves of a binary tree -/
@@ -130,8 +127,8 @@ def numLeaves : BinaryTree α → ℕ
   | node _ a b => a.numLeaves + b.numLeaves
 
 set_option linter.deprecated false in
-/-- The number of leaves of a binary tree -/
-@[deprecated BinaryTree.numLeaves (since := "2026-05-22")]
+/-- **Alias** of `BinaryTree.numLeaves`. -/
+@[deprecated BinaryTree.numLeaves (since := "2026-06-07")]
 abbrev _root_.Tree.numLeaves {α} (t : Tree α) : ℕ := BinaryTree.numLeaves t
 
 
@@ -142,8 +139,8 @@ def height : BinaryTree α → ℕ
   | node _ a b => max a.height b.height + 1
 
 set_option linter.deprecated false in
-/-- The height - length of the longest path from the root - of a binary tree -/
-@[deprecated BinaryTree.height (since := "2026-05-22")]
+/-- **Alias** of `BinaryTree.height`. -/
+@[deprecated BinaryTree.height (since := "2026-06-07")]
 abbrev _root_.Tree.height {α} (t : Tree α) : ℕ := BinaryTree.height t
 
 theorem numLeaves_eq_numNodes_succ (x : BinaryTree α) : x.numLeaves = x.numNodes + 1 := by
@@ -166,8 +163,8 @@ def left : BinaryTree α → BinaryTree α
   | node _ l _r => l
 
 set_option linter.deprecated false in
-/-- The left child of the tree, or `nil` if the tree is `nil` -/
-@[deprecated BinaryTree.left (since := "2026-05-22")]
+/-- **Alias** of `BinaryTree.left`. -/
+@[deprecated BinaryTree.left (since := "2026-06-07")]
 abbrev _root_.Tree.left {α} (t : Tree α) : Tree α := BinaryTree.left t
 
 /-- The right child of the tree, or `nil` if the tree is `nil` -/
@@ -177,8 +174,8 @@ def right : BinaryTree α → BinaryTree α
   | node _ _l r => r
 
 set_option linter.deprecated false in
-/-- The right child of the tree, or `nil` if the tree is `nil` -/
-@[deprecated BinaryTree.right (since := "2026-05-22")]
+/-- **Alias** of `BinaryTree.right`. -/
+@[deprecated BinaryTree.right (since := "2026-06-07")]
 abbrev _root_.Tree.right {α} (t : Tree α) : Tree α := BinaryTree.right t
 
 /-- A node with `Unit` data -/
@@ -191,8 +188,8 @@ def unitRecOn {motive : BinaryTree Unit → Sort*} (t : BinaryTree Unit) (base :
   t.recOn base fun _u ↦ ind
 
 set_option linter.deprecated false in
-/-- Induction principle for `Tree Unit`s -/
-@[deprecated BinaryTree.unitRecOn (since := "2026-05-22")]
+/-- **Alias** of `BinaryTree.unitRecOn`. -/
+@[deprecated BinaryTree.unitRecOn (since := "2026-06-07")]
 abbrev _root_.Tree.unitRecOn {motive : Tree Unit → Sort*} (t : Tree Unit) (base : motive nil)
     (ind : ∀ x y, motive x → motive y → motive (x △ y)) : motive t :=
   BinaryTree.unitRecOn t base ind
diff --git a/Mathlib/Data/Tree/Get.lean b/Mathlib/Data/Tree/Get.lean
index 45d7f7f4988c80..9d4468c3c8c410 100644
--- a/Mathlib/Data/Tree/Get.lean
+++ b/Mathlib/Data/Tree/Get.lean
@@ -39,11 +39,8 @@ def indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : BinaryTree α
     | Ordering.gt => PosNum.bit1 <$> indexOf lt x t₂
 
 set_option linter.deprecated false in
-/-- Finds the index of an element in the tree assuming the tree has been
-constructed according to the provided decidable order on its elements.
-If it hasn't, the result will be incorrect. If it has, but the element
-is not in the tree, returns none. -/
-@[deprecated BinaryTree.indexOf (since := "2026-05-22")]
+/-- **Alias** of `BinaryTree.indexOf`. -/
+@[deprecated BinaryTree.indexOf (since := "2026-06-07")]
 abbrev _root_.Tree.indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : Tree α → Option PosNum :=
   BinaryTree.indexOf lt x
 
@@ -59,12 +56,8 @@ def get : PosNum → BinaryTree α → Option α
   | PosNum.bit1 n, node _a _t₁ t₂ => t₂.get n
 
 set_option linter.deprecated false in
-/-- Retrieves an element uniquely determined by a `PosNum` from the tree,
-taking the following path to get to the element:
-- `bit0` - go to left child
-- `bit1` - go to right child
-- `PosNum.one` - retrieve from here -/
-@[deprecated BinaryTree.get (since := "2026-05-22")]
+/-- **Alias** of `BinaryTree.get`. -/
+@[deprecated BinaryTree.get (since := "2026-06-07")]
 abbrev _root_.Tree.get (n : PosNum) (t : Tree α) : Option α :=
   BinaryTree.get n t
 
@@ -74,9 +67,8 @@ def getOrElse (n : PosNum) (t : BinaryTree α) (v : α) : α :=
   (t.get n).getD v
 
 set_option linter.deprecated false in
-/-- Retrieves an element from the tree, or the provided default value
-if the index is invalid. See `Tree.get`. -/
-@[deprecated BinaryTree.getOrElse (since := "2026-05-22")]
+/-- **Alias** of `BinaryTree.getOrElse`. -/
+@[deprecated BinaryTree.getOrElse (since := "2026-06-07")]
 abbrev _root_.Tree.getOrElse (n : PosNum) (t : Tree α) (v : α) : α :=
   BinaryTree.getOrElse n t v
 

From 51c6e76c7e1e1dfa1f4537ec77d70a9302cf57ce Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Mon, 8 Jun 2026 02:16:13 +0000
Subject: [PATCH 32/37] missing deprecation

---
 Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean b/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean
index 6985c392913baa..1b0f1c47b1c3ad 100644
--- a/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean
+++ b/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean
@@ -45,6 +45,12 @@ def treesOfNumNodesEq : ℕ → Finset (BinaryTree Unit)
     · simp_wf; have := fst_le ijh.2; lia
     · simp_wf; have := snd_le ijh.2; lia
 
+set_option linter.deprecated false in
+/-- **Alias** of `BinaryTree.treesOfNumNodesEq`. -/
+@[deprecated BinaryTree.getOrElse (since := "2026-06-07")]
+abbrev _root_.Tree.treesOfNumNodesEq : ℕ → Finset (Tree Unit) :=
+  BinaryTree.treesOfNumNodesEq
+
 @[simp]
 theorem treesOfNumNodesEq_zero : treesOfNumNodesEq 0 = {nil} := by rw [treesOfNumNodesEq]
 

From 44ee70e042b2e41bbc19a337dacabeffaefb90ec Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Mon, 8 Jun 2026 02:24:59 +0000
Subject: [PATCH 33/37] missing import

---
 Mathlib/Data/Tree/Basic.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 70205f543a9a02..12e8ec9fe0e92b 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Data.Nat.Notation
 public import Mathlib.Util.CompileInductive
+import Batteries.Tactic.Alias
 
 /-!
 # Binary tree
@@ -34,7 +35,7 @@ inductive BinaryTree.{u} (α : Type u) : Type u
   deriving DecidableEq, Repr
 compile_inductive% BinaryTree
 
-@[deprecated BinaryTree (since := "2026-06-07"), reducible]
+@[deprecated (since := "2026-06-07"), reducible]
 alias Tree := BinaryTree
 
 set_option linter.deprecated false in

From 16ffd5917e2f7f20a30b2243d0c5f56e0b4f677b Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 8 Jun 2026 07:38:25 -0700
Subject: [PATCH 34/37] Apply suggestion from @eric-wieser

---
 Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean b/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean
index 1b0f1c47b1c3ad..c29da1292184a8 100644
--- a/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean
+++ b/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean
@@ -47,7 +47,7 @@ def treesOfNumNodesEq : ℕ → Finset (BinaryTree Unit)
 
 set_option linter.deprecated false in
 /-- **Alias** of `BinaryTree.treesOfNumNodesEq`. -/
-@[deprecated BinaryTree.getOrElse (since := "2026-06-07")]
+@[deprecated BinaryTree.treesOfNumNodesEq (since := "2026-06-07")]
 abbrev _root_.Tree.treesOfNumNodesEq : ℕ → Finset (Tree Unit) :=
   BinaryTree.treesOfNumNodesEq
 

From fdb4514c9f7219072a21f7dc3c6bdd55de706d52 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 8 Jun 2026 08:36:46 -0700
Subject: [PATCH 35/37] Docstring and formatting

---
 Mathlib/Data/Tree/Basic.lean | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 12e8ec9fe0e92b..d88d222aa4be91 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -64,19 +64,17 @@ Do an action for every node of the tree.
 Actions are taken in node -> left subtree -> right subtree recursive order.
 This function is the `traverse` function for the `Traversable BinaryTree` instance.
 -/
-def traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β)
-: BinaryTree α → m (BinaryTree β)
+def traverse
+    {m : Type* → Type*} [Applicative m] {α β} (f : α → m β) :
+    BinaryTree α → m (BinaryTree β)
   | .nil => pure nil
   | .node a l r => .node <$> f a <*> traverse f l <*> traverse f r
 
-/--
-Do an action for every node of the tree.
-Actions are taken in node -> left subtree -> right subtree recursive order.
-This function is the `traverse` function for the `Traversable BinaryTree` instance.
--/
+set_option linter.deprecated false in
+/-- **Alias** of `BinaryTree.traverse`. -/
 @[deprecated BinaryTree.traverse (since := "2026-06-07")]
 abbrev _root_.Tree.traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β)
-(t : BinaryTree α) : m (BinaryTree β) :=
+(t : Tree α) : m (Tree β) :=
   BinaryTree.traverse f t
 
 /-- Apply a function to each value in the BinaryTree.

From 2f1f2ddff0b5cc5723a16f4fd2584738c3d6d76c Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 8 Jun 2026 08:38:37 -0700
Subject: [PATCH 36/37] Fix bad line wrapping

---
 Mathlib/Data/Tree/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index d88d222aa4be91..6d69ac804b04cc 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -46,8 +46,8 @@ abbrev Tree.nil.{u} {α : Type u} : Tree α := BinaryTree.nil
 set_option linter.deprecated false in
 /-- **Alias** of `BinaryTree.node`. -/
 @[deprecated BinaryTree.node (since := "2026-06-07")]
-abbrev Tree.node.{u} {α : Type u} (value : α) (left : Tree α) (right : Tree α)
-: Tree α :=
+abbrev Tree.node.{u} {α : Type u}
+    (value : α) (left : Tree α) (right : Tree α) : Tree α :=
   BinaryTree.node value left right
 
 namespace BinaryTree

From c5644255220bf9a6ac750620e29e4f94e8d9e5b5 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 8 Jun 2026 11:29:17 -0700
Subject: [PATCH 37/37] Remove blank line

---
 Mathlib/Data/Tree/Basic.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean
index 6d69ac804b04cc..993a21a4c1953e 100644
--- a/Mathlib/Data/Tree/Basic.lean
+++ b/Mathlib/Data/Tree/Basic.lean
@@ -130,7 +130,6 @@ set_option linter.deprecated false in
 @[deprecated BinaryTree.numLeaves (since := "2026-06-07")]
 abbrev _root_.Tree.numLeaves {α} (t : Tree α) : ℕ := BinaryTree.numLeaves t
 
-
 /-- The height - length of the longest path from the root - of a binary tree -/
 @[simp]
 def height : BinaryTree α → ℕ