diff --git a/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean b/Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean
index 6822befbff552e..c29da1292184a8 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 =>
@@ -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
diff --git a/Mathlib/Combinatorics/Enumerative/DyckWord.lean b/Mathlib/Combinatorics/Enumerative/DyckWord.lean
index 7a6a5447ff038a..972ca6dccd153a 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..993a21a4c1953e 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
@@ -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,30 +110,45 @@ 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 _,
@@ -109,27 +156,44 @@ theorem height_le_numNodes : ∀ x : Tree α, x.height ≤ x.numNodes
 
 /-- 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
diff --git a/Mathlib/Data/Tree/Get.lean b/Mathlib/Data/Tree/Get.lean
index c18cc3823ff6b2..9d4468c3c8c410 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
@@ -38,20 +38,38 @@ def indexOf (lt : α → α → Prop) [DecidableRel lt] (x : α) : Tree α → O
     | 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
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
diff --git a/docs/overview.yaml b/docs/overview.yaml
index b660bfec420082..ec76c6c11f4918 100644
--- a/docs/overview.yaml
+++ b/docs/overview.yaml
@@ -590,7 +590,7 @@ Data structures:
     finite map: 'Finmap'
 
   Trees:
-    tree: 'Tree'
+    tree: 'BinaryTree'
     # deprecated in https://github.com/leanprover-community/batteries/pull/1792
     # red-black tree: 'Batteries.RBSet'
     size-balanced binary search tree: 'Ordnode'