chore(Data/Tree/Basic): Rename Tree to BinaryTree (#39707)

Rename `Tree` to `BinaryTree`.

This frees up the name `Tree` to cover n-ary trees in future.

We only deprecate the `def`s, and move the theorems without deprecation.

Co-authored-by: Eric Wieser <efw@google.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: sorrachai

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 =>
@@ -45,6 +45,12 @@ def treesOfNumNodesEq : ℕ → Finset (Tree 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.treesOfNumNodesEq (since := "2026-06-07")]
+abbrev _root_.Tree.treesOfNumNodesEq : ℕ → Finset (Tree Unit) :=
+  BinaryTree.treesOfNumNodesEq
+
 @[simp]
 theorem treesOfNumNodesEq_zero : treesOfNumNodesEq 0 = {nil} := by rw [treesOfNumNodesEq]
 
@@ -57,17 +63,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 +87,4 @@ theorem treesOfNumNodesEq_card_eq_catalan (n : ℕ) : #(treesOfNumNodesEq n) = c
     · simp_rw [Set.PairwiseDisjoint, Set.Pairwise, disjoint_left]
       aesop
 
-end Tree
+end BinaryTree

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
 

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
@@ -15,8 +16,8 @@ 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.
 
-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 tree without any
+additional data. We provide the notation `a △ b` for making a `BinaryTree Unit` with children
 `a` and `b`.
 
 ## References
@@ -28,48 +29,79 @@ additional data. We provide the notation `a △ b` for making a `Tree Unit` with
 
 
 /-- 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 α
+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
+@[deprecated (since := "2026-06-07"), reducible]
+alias Tree := BinaryTree
+
+set_option linter.deprecated false in
+/-- **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
+/-- **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
+
+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.
+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.
+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 : Tree α) : m (Tree β) :=
+  BinaryTree.traverse f t
+
+/-- 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
+set_option linter.deprecated false in
+/-- **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
   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] :
+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]
@@ -78,58 +110,90 @@ theorem traverse_pure (t : Tree α) {m : Type u → Type*} [Applicative m] [Lawf
 
 /-- The number of internal nodes (i.e. not including leaves) of a binary tree -/
 @[simp]
-def numNodes : Tree α → ℕ
+def numNodes : BinaryTree α → ℕ
   | nil => 0
   | node _ a b => a.numNodes + b.numNodes + 1
 
+set_option linter.deprecated false in
+/-- **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 -/
 @[simp]
-def numLeaves : Tree α → ℕ
+def numLeaves : BinaryTree α → ℕ
   | nil => 1
   | node _ a b => a.numLeaves + b.numLeaves
 
+set_option linter.deprecated false in
+/-- **Alias** of `BinaryTree.numLeaves`. -/
+@[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 : 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
+set_option linter.deprecated false in
+/-- **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
   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` -/
 @[simp]
-def left : Tree α → Tree α
+def left : BinaryTree α → BinaryTree α
   | nil => nil
   | node _ l _r => l
 
+set_option linter.deprecated false in
+/-- **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` -/
 @[simp]
-def right : Tree α → Tree α
+def right : BinaryTree α → BinaryTree α
   | nil => nil
   | node _ _l r => r
 
+set_option linter.deprecated false in
+/-- **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 -/
-scoped infixr:65 " △ " => Tree.node ()
+scoped infixr:65 " △ " => BinaryTree.node ()
 
-/-- Induction principle for `Tree Unit`s -/
+/-- 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
+set_option linter.deprecated false in
+/-- **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
+
+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
+end BinaryTree

Mathlib/Data/Tree/Get.lean

@@ -22,36 +22,54 @@ These definitions were moved from the main file to avoid a dependency on `Num`.
 
 @[expose] public section
 
-namespace Tree
+namespace BinaryTree
 
 variable {α : Type*}
 
 /-- 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. -/
-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
     | Ordering.lt => PosNum.bit0 <$> indexOf lt x t₁
     | Ordering.eq => some PosNum.one
     | Ordering.gt => PosNum.bit1 <$> indexOf lt x t₂
 
+set_option linter.deprecated false in
+/-- **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
+
 /-- 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 -/
-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
   | PosNum.bit1 n, node _a _t₁ t₂ => t₂.get n
 
+set_option linter.deprecated false in
+/-- **Alias** of `BinaryTree.get`. -/
+@[deprecated BinaryTree.get (since := "2026-06-07")]
+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`. -/
-def getOrElse (n : PosNum) (t : Tree α) (v : α) : α :=
+if the index is invalid. See `BinaryTree.get`. -/
+def getOrElse (n : PosNum) (t : BinaryTree α) (v : α) : α :=
   (t.get n).getD v
 
-end Tree
+set_option linter.deprecated false in
+/-- **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
+
+end BinaryTree