feat: add BEq to DTreeMap/TreeMap/TreeSet and their extensional variants (#11404)

This PR adds BEq instance for `DTreeMap`/`TreeMap`/`TreeSet` and their
extensional variants and proves lemmas relating it to the equivalence of
hashmaps/equality of extensional variants.

Stacked on top of #11266

src/Std/Data/DTreeMap/Basic.lean

@@ -870,17 +870,11 @@ end Const
 
 /-- Check if any element satisfies the predicate, short-circuiting if a predicate fails. -/
 @[inline]
-def any (t : DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool := Id.run $ do
-  for ⟨a, b⟩ in t do
-    if p a b then return true
-  return false
+def any (t : DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool := t.inner.any p
 
 /-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails. -/
 @[inline]
-def all (t : DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool := Id.run $ do
-  for ⟨a, b⟩ in t do
-    if p a b = false then return false
-  return true
+def all (t : DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool := t.inner.all p
 
 /-- Returns a list of all keys present in the tree map in ascending  order. -/
 @[inline]
@@ -1054,6 +1048,19 @@ def inter (t₁ t₂ : DTreeMap α β cmp) : DTreeMap α β cmp :=
 
 instance : Inter (DTreeMap α β cmp) := ⟨inter⟩
 
+/--
+Compares two tree maps using Boolean equality on keys and values.
+
+Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
+-/
+def beq [LawfulEqCmp cmp] [∀ k, BEq (β k)] (t₁ t₂ : DTreeMap α β cmp) : Bool :=
+  letI : Ord α := ⟨cmp⟩; t₁.inner.beq t₂.inner
+
+instance [LawfulEqCmp cmp] [∀ k, BEq (β k)] : BEq (DTreeMap α β cmp) := ⟨beq⟩
+
+@[inherit_doc DTreeMap.beq] def Const.beq {β : Type v} [BEq β] (t₁ t₂ : DTreeMap α (fun _ => β) cmp) : Bool :=
+  letI : Ord α := ⟨cmp⟩; Internal.Impl.Const.beq t₁.inner t₂.inner
+
 /--
 Computes the difference of the given tree maps.
 This function always iterates through the smaller map.

src/Std/Data/DTreeMap/Internal/Lemmas.lean

@@ -101,6 +101,8 @@ private meta def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (T
      ⟨`getKeyD, (``getKeyD_eq_getKeyD, #[``(getKeyD_of_perm _)])⟩,
      ⟨`getKey!, (``getKey!_eq_getKey!, #[``(getKey!_of_perm _)])⟩,
      ⟨`toList, (``toList_eq_toListModel, #[])⟩,
+     ⟨`beq, (``beq_eq_beqModel, #[])⟩,
+     ⟨`Const.beq, (``Internal.Impl.Const.beq_eq_beqModel, #[])⟩,
      ⟨`keys, (``keys_eq_keys, #[])⟩,
      ⟨`Const.toList, (``Const.toList_eq_toListModel_map, #[])⟩,
      ⟨`foldlM, (``foldlM_eq_foldlM_toListModel, #[])⟩,
@@ -4888,6 +4890,37 @@ theorem get!_inter!_of_contains_eq_false_left [TransOrd α] [Inhabited β] (h₁
 
 end Const
 
+section BEq
+variable {m₁ m₂ : Impl α β} [TransOrd α] [LawfulEqOrd α] [∀ k, BEq (β k)]
+
+theorem Equiv.beq [∀ k, ReflBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁.Equiv m₂ → beq m₁ m₂ := by
+  simp_to_model using List.beqModel_eq_true_of_perm
+
+theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) : beq m₁ m₂ = true → m₁.Equiv m₂ := by
+  simp_to_model using List.perm_of_beqModel
+
+theorem Equiv.beq_congr {m₃ m₄ : Impl α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) :
+    m₁.Equiv m₃ → m₂.Equiv m₄ → (Impl.beq m₁ m₂) = (Impl.beq m₃ m₄) := by
+  simp_to_model using List.beqModel_congr
+
+end BEq
+
+section
+
+variable {β : Type v} [BEq β] {m₁ m₂ : Impl α (fun _ => β)}
+
+theorem Const.Equiv.beq [TransOrd α] [ReflBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁.Equiv m₂ → Const.beq m₁ m₂ := by
+  simp_to_model using List.Const.beqModel_eq_true_of_perm
+
+theorem Const.equiv_of_beq [TransOrd α] [LawfulEqOrd α] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : Const.beq m₁ m₂ = true → m₁.Equiv m₂ := by
+  simp_to_model using List.Const.perm_of_beqModel
+
+theorem Const.Equiv.beq_congr [TransOrd α] {m₃ m₄ : Impl α (fun _ => β)} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) :
+    m₁.Equiv m₃ → m₂.Equiv m₄ → Const.beq m₁ m₂ = Const.beq m₃ m₄ := by
+  simp_to_model using List.Const.beqModel_congr
+
+end
+
 section Diff
 
 variable {m₁ m₂ : Impl α β}

src/Std/Data/DTreeMap/Internal/Operations.lean

@@ -822,6 +822,10 @@ information but still assumes the preconditions of `filter`, otherwise might pan
 def inter! [Ord α] (m₁ m₂ : Impl α β): Impl α β :=
   if m₁.size ≤ m₂.size then m₁.filter! (fun k _ => m₂.contains k) else interSmaller m₁ m₂
 
+/-- Internal implementation detail of the tree map -/
+def beq [Ord α] [LawfulEqOrd α] [∀ k, BEq (β k)] (t₁ t₂ : Impl α β) : Bool :=
+  if t₁.size ≠ t₂.size then false else t₁.all (fun k v => t₂.get? k == some v)
+
 /--
 Computes the difference of the given tree maps.
 This function always iterates through the smaller map.
@@ -950,6 +954,11 @@ def mergeWith! [Ord α] [LawfulEqOrd α] (mergeFn : (a : α) → β a → β a
 namespace Const
 
 variable {β : Type v}
+
+/-- Internal implementation detail of the hash map -/
+def beq [Ord α] [BEq β] (t₁ t₂ : Impl α fun _ => β) : Bool :=
+  if t₁.size ≠ t₂.size then false else t₁.all (fun k v => Const.get? t₂ k == some v)
+
 local instance : Coe (Type v) (α → Type v) where coe γ := fun _ => γ
 
 /--

src/Std/Data/DTreeMap/Internal/Queries.lean

@@ -293,6 +293,20 @@ def forIn {m} [Monad m] (f : (a : α) → β a → δ → m (ForInStep δ)) (ini
 instance [Monad m] : ForIn m (Impl α β) ((a : α) × β a) where
   forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
+/-- Implementation detail. -/
+@[inline]
+def any (t : Impl α β) (p : (a : α) → β a → Bool) : Bool := Id.run $ do
+  for ⟨a, b⟩ in t do
+    if p a b then return true
+  return false
+
+/-- Implementation detail. -/
+@[inline]
+def all (t : Impl α β) (p : (a : α) → β a → Bool) : Bool := Id.run $ do
+  for ⟨a, b⟩ in t do
+    if p a b = false then return false
+  return true
+
 /-- Returns a `List` of the keys in order. -/
 @[inline] def keys (t : Impl α β) : List α :=
   t.foldr (init := []) fun k _ l => k :: l

src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean

@@ -1900,6 +1900,29 @@ theorem WF.union! {_ : Ord α} [TransOrd α]
   . exact WF.insertManyIfNew! h₂
   . exact WF.insertMany! h₁
 
+theorem all_eq_all_toListModel {p : (a : α) → β a → Bool} {m : Impl α β} :
+    m.all p = m.toListModel.all (fun x => p x.1 x.2) := by
+  simp [all, ForIn.forIn, bind_pure_comp, map_pure, Id.run_bind]
+  rw [forIn_eq_forIn_toListModel, ← toList_eq_toListModel, forIn_eq_forIn']
+  induction m.toList with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [forIn'_eq_forIn, List.all_cons]
+    by_cases h : p hd.fst hd.snd = false
+    · simp [h]
+    · simp only [forIn'_eq_forIn] at ih
+      simp [h, ih]
+
+theorem beq_eq_beqModel {_ : Ord α} [BEq α] [TransOrd α] [LawfulBEq α] [LawfulBEqOrd α] [∀ k, BEq (β k)] {m₁ m₂ : Impl α β} (h₁ : m₁.WF) (h₂ : m₂.WF) :
+    Impl.beq m₁ m₂ = beqModel m₁.toListModel m₂.toListModel := by
+  simp [beq, beqModel, size_eq_length _ h₁.balanced, size_eq_length _ h₂.balanced, all_eq_all_toListModel,
+    get?_eq_getValueCast? h₂.ordered]
+
+theorem Const.beq_eq_beqModel {β : Type v} {_ : Ord α} [BEq α] [TransOrd α] [LawfulBEqOrd α] [BEq β] {m₁ m₂ : Impl α (fun _ => β)}  (h₁ : m₁.WF) (h₂ : m₂.WF) :
+    beq m₁ m₂ = Const.beqModel m₁.toListModel m₂.toListModel := by
+  simp [beq, Const.beqModel, size_eq_length _ h₁.balanced, size_eq_length _ h₂.balanced, all_eq_all_toListModel,
+    get?_eq_getValue? h₂.ordered]
+
 theorem WF.constInsertMany! {β : Type v} {_ : Ord α} [TransOrd α] {ρ} [ForIn Id ρ (α × β)] {l : ρ}
     {t : Impl α β} (h : t.WF) : (Const.insertMany! t l).1.WF :=
   (Const.insertMany! t l).2 h (fun _ _ _ h' => h'.insert!)

src/Std/Data/DTreeMap/Lemmas.lean

@@ -2890,6 +2890,36 @@ theorem get!_inter_of_not_mem_left [TransCmp cmp] [Inhabited β]
 
 end Const
 
+section BEq
+
+variable {m₁ m₂ : DTreeMap α β cmp} [∀ k, BEq (β k)] [LawfulEqCmp cmp] [TransCmp cmp]
+
+theorem Equiv.beq [∀ k, ReflBEq (β k)] (h : m₁ ~m m₂) : m₁ == m₂ :=
+  Impl.Equiv.beq m₁.2 m₂.2 h.1
+
+theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h : m₁ == m₂) : m₁ ~m m₂ :=
+  ⟨Impl.equiv_of_beq m₁.2 m₂.2 h⟩
+
+theorem Equiv.beq_congr {m₃ m₄ : DTreeMap α β cmp} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) :=
+  Impl.Equiv.beq_congr m₁.2 m₂.2 m₃.2 m₄.2 w₁.1 w₂.1
+
+end BEq
+
+section
+
+variable {β : Type v} {m₁ m₂ : DTreeMap α (fun _ => β) cmp} [BEq β]
+
+theorem Const.Equiv.beq [TransCmp cmp] [ReflBEq β] (h : m₁ ~m m₂) : DTreeMap.Const.beq m₁ m₂ :=
+  Impl.Const.Equiv.beq m₁.2 m₂.2 h.1
+
+theorem Const.equiv_of_beq [TransCmp cmp] [LawfulEqCmp cmp] [LawfulBEq β] (h : Const.beq m₁ m₂) : m₁ ~m m₂ :=
+  ⟨Impl.Const.equiv_of_beq m₁.2 m₂.2 h⟩
+
+theorem Const.Equiv.beq_congr [TransCmp cmp] {m₃ m₄ : DTreeMap α (fun _ => β) cmp} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : Const.beq m₁ m₂ = Const.beq m₃ m₄ :=
+  Impl.Const.Equiv.beq_congr m₁.2 m₂.2 m₃.2 m₄.2 w₁.1 w₂.1
+
+end
+
 section Diff
 
 variable {t₁ t₂ : DTreeMap α β cmp}
@@ -5372,10 +5402,10 @@ theorem forM_eq [TransCmp cmp] [Monad m] [LawfulMonad m] {f : (a : α) × β a
   h.1.forM_eq t₁.2 t₂.2
 
 theorem any_eq [TransCmp cmp] {p : (a : α) → β a → Bool} (h : t₁ ~m t₂) : t₁.any p = t₂.any p := by
-  simp only [any, h.forIn_eq]
+  simp only [any, Impl.any, ForIn.forIn, h.1.forIn_eq t₁.2 t₂.2]
 
 theorem all_eq [TransCmp cmp] {p : (a : α) → β a → Bool} (h : t₁ ~m t₂) : t₁.all p = t₂.all p := by
-  simp only [all, h.forIn_eq]
+  simp only [all, Impl.all, ForIn.forIn, h.1.forIn_eq t₁.2 t₂.2]
 
 theorem minKey?_eq [TransCmp cmp] (h : t₁ ~m t₂) : t₁.minKey? = t₂.minKey? :=
   h.1.minKey?_eq t₁.2 t₂.2

src/Std/Data/DTreeMap/Raw/Basic.lean

@@ -604,16 +604,12 @@ def forInUncurried (f : α × β → δ → m (ForInStep δ)) (init : δ) (t : R
 end Const
 
 @[inline, inherit_doc DTreeMap.any]
-def any (t : Raw α β cmp) (p : (a : α) → β a → Bool) : Bool := Id.run $ do
-  for ⟨a, b⟩ in t do
-    if p a b then return true
-  return false
+def any (t : Raw α β cmp) (p : (a : α) → β a → Bool) : Bool :=
+  t.inner.any p
 
 @[inline, inherit_doc DTreeMap.all]
 def all (t : Raw α β cmp) (p : (a : α) → β a → Bool) : Bool := Id.run $ do
-  for ⟨a, b⟩ in t do
-    if p a b = false then return false
-  return true
+  t.inner.all p
 
 @[inline, inherit_doc DTreeMap.keys]
 def keys (t : Raw α β cmp) : List α :=
@@ -732,6 +728,15 @@ def inter (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
 
 instance : Inter (Raw α β cmp) := ⟨inter⟩
 
+
+@[inherit_doc DTreeMap.beq] def beq [LawfulEqCmp cmp] [∀ k, BEq (β k)] (t₁ t₂ : Raw α β cmp) : Bool :=
+  letI : Ord α := ⟨cmp⟩; t₁.inner.beq t₂.inner
+
+instance [LawfulEqCmp cmp] [∀ k, BEq (β k)] : BEq (Raw α β cmp) := ⟨beq⟩
+
+@[inherit_doc DTreeMap.beq] def Const.beq {β : Type v} [BEq β] (t₁ t₂ : Raw α (fun _ => β) cmp) : Bool :=
+  letI : Ord α := ⟨cmp⟩; Internal.Impl.Const.beq t₁.inner t₂.inner
+
 /--
 Computes the difference of the given tree maps.
 This function always iterates through the smaller map.

src/Std/Data/DTreeMap/Raw/Lemmas.lean

@@ -3056,6 +3056,36 @@ theorem get!_inter_of_not_mem_left [TransCmp cmp] [Inhabited β] (h₁ : m₁.WF
 
 end Const
 
+section BEq
+variable {m₁ m₂ : Raw α β cmp} [∀ k, BEq (β k)] [LawfulEqCmp cmp] [TransCmp cmp]
+
+theorem Equiv.beq [∀ k, ReflBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : beq m₁ m₂ :=
+  Impl.Equiv.beq h₁ h₂ h.1
+
+theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) : beq m₁ m₂ = true → m₁ ~m m₂ := fun hyp =>
+  let : Ord α := ⟨cmp⟩; ⟨Impl.equiv_of_beq h₁.1 h₂.1 hyp⟩
+
+theorem Equiv.beq_congr {m₃ m₄ : Raw α β cmp} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) :
+    m₁ ~m m₃ → m₂ ~m m₄ → Raw.beq m₁ m₂ = Raw.beq m₃ m₄ :=
+  fun w1 w2 => Impl.Equiv.beq_congr h₁ h₂ h₃ h₄ w1.1 w2.1
+
+end BEq
+
+section
+variable {β : Type v} {m₁ m₂ : Raw α (fun _ => β) cmp}
+
+theorem Const.Equiv.beq [TransCmp cmp] [BEq β] [ReflBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁ ~m m₂ → beq m₁ m₂ :=
+  fun h => Impl.Const.Equiv.beq h₁ h₂ h.1
+
+theorem Const.equiv_of_beq [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : beq m₁ m₂ = true → m₁ ~m m₂ :=
+  fun hyp => let : Ord α := ⟨cmp⟩; ⟨Impl.Const.equiv_of_beq h₁.1 h₂.1 hyp⟩
+
+theorem Const.Equiv.beq_congr [TransCmp cmp] [BEq β] {m₃ m₄ : Raw α (fun _ => β) cmp} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) :
+    m₁ ~m m₃ → m₂ ~m m₄ → Raw.Const.beq m₁ m₂ = Raw.Const.beq m₃ m₄ :=
+  fun w1 w2 => Impl.Const.Equiv.beq_congr h₁ h₂ h₃ h₄ w1.1 w2.1
+
+end
+
 section Diff
 
 variable {t₁ t₂ : Raw α β cmp}
@@ -5295,11 +5325,13 @@ theorem forM_eq [TransCmp cmp] [Monad m] [LawfulMonad m] {f : (a : α) × β a
 
 theorem any_eq [TransCmp cmp] {p : (a : α) → β a → Bool} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁ ~m t₂) :
     t₁.any p = t₂.any p := by
-  simp only [any, h.forIn_eq h₁ h₂]
+  simp only [any, Impl.any, ForIn.forIn, bind_pure_comp, map_pure, h.1.forIn_eq h₁.1 h₂.1,
+    Id.run_bind]
 
 theorem all_eq [TransCmp cmp] {p : (a : α) → β a → Bool} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁ ~m t₂) :
     t₁.all p = t₂.all p := by
-  simp only [all, h.forIn_eq h₁ h₂]
+  simp only [all, Impl.all, ForIn.forIn, bind_pure_comp, map_pure, h.1.forIn_eq h₁.1 h₂.1,
+    Id.run_bind]
 
 theorem minKey?_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁ ~m t₂) :
     t₁.minKey? = t₂.minKey? :=

src/Std/Data/ExtDTreeMap/Basic.lean

@@ -924,6 +924,30 @@ def inter [TransCmp cmp] (m₁ m₂ : ExtDTreeMap α β cmp) : ExtDTreeMap α β
 
 instance [TransCmp cmp] : Inter (ExtDTreeMap α β cmp) := ⟨inter⟩
 
+instance [LawfulEqCmp cmp] [TransCmp cmp] [∀ k, BEq (β k)] : BEq (ExtDTreeMap α β cmp) where
+  beq := lift₂ (fun x y : DTreeMap α β cmp => x.beq y) fun _ _ _ _ => DTreeMap.Equiv.beq_congr
+
+instance [LawfulEqCmp cmp] [TransCmp cmp] [∀ k, BEq (β k)] [∀ k, ReflBEq (β k)] : ReflBEq (ExtDTreeMap α β cmp) where
+  rfl {a} := a.inductionOn fun _ => DTreeMap.Equiv.beq <| DTreeMap.Equiv.rfl
+
+instance [LawfulEqCmp cmp] [TransCmp cmp] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] : LawfulBEq (ExtDTreeMap α β cmp) where
+  eq_of_beq {a} {b} := a.inductionOn₂ b fun _ _ h => sound <| DTreeMap.equiv_of_beq h
+
+namespace Const
+
+variable {β : Type v}
+
+@[inline, inherit_doc DTreeMap.beq]
+def beq [TransCmp cmp] [BEq β] (m₁ m₂ : ExtDTreeMap α (fun _ => β) cmp) : Bool := lift₂ (fun x y : DTreeMap α (fun _ => β) cmp => DTreeMap.Const.beq x y)
+  (fun _ _ _ _ => DTreeMap.Const.Equiv.beq_congr) m₁ m₂
+
+theorem beq_of_eq [TransCmp cmp] [BEq β] [ReflBEq β] (m₁ m₂ : ExtDTreeMap α (fun _ => β) cmp) : m₁ = m₂ → Const.beq m₁ m₂ :=
+  m₁.inductionOn₂ m₂ fun _ _ h => DTreeMap.Const.Equiv.beq <| exact h
+
+theorem eq_of_beq [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] (m₁ m₂ : ExtDTreeMap α (fun _ => β) cmp) : Const.beq m₁ m₂ → m₁ = m₂ :=
+  m₁.inductionOn₂ m₂ fun _ _ h => sound <| DTreeMap.Const.equiv_of_beq h
+
+end Const
 @[inline, inherit_doc DTreeMap.diff]
 def diff [TransCmp cmp] (m₁ m₂ : ExtDTreeMap α β cmp) : ExtDTreeMap α β cmp := lift₂ (fun x y : DTreeMap α β cmp => mk (x.diff y))
   (fun a b c d equiv₁ equiv₂ => by

src/Std/Data/ExtTreeMap/Basic.lean

@@ -535,6 +535,19 @@ def inter [TransCmp cmp] (t₁ t₂ : ExtTreeMap α β cmp) : ExtTreeMap α β c
 
 instance [TransCmp cmp] : Inter (ExtTreeMap α β cmp) := ⟨inter⟩
 
+instance [TransCmp cmp] [BEq β] : BEq (ExtTreeMap α β cmp) where
+  beq m₁ m₂ := ExtDTreeMap.Const.beq m₁.inner m₂.inner
+
+instance [TransCmp cmp] [BEq β] [ReflBEq β] : ReflBEq (ExtTreeMap α β cmp) where
+  rfl := ExtDTreeMap.Const.beq_of_eq _ _ rfl
+
+instance [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] : LawfulBEq (ExtTreeMap α β cmp) where
+  eq_of_beq {a} {b} hyp := by
+    have ⟨_⟩ := a
+    have ⟨_⟩ := b
+    simp only [mk.injEq]
+    exact ExtDTreeMap.Const.eq_of_beq _ _ hyp
+    
 @[inline, inherit_doc ExtDTreeMap.diff]
 def diff [TransCmp cmp] (t₁ t₂ : ExtTreeMap α β cmp) : ExtTreeMap α β cmp := ⟨ExtDTreeMap.diff t₁.inner t₂.inner⟩
 

src/Std/Data/ExtTreeSet/Basic.lean

@@ -529,6 +529,19 @@ def inter [TransCmp cmp] (t₁ t₂ : ExtTreeSet α cmp) : ExtTreeSet α cmp :=
 
 instance [TransCmp cmp] : Inter (ExtTreeSet α cmp) := ⟨inter⟩
 
+instance [TransCmp cmp] : BEq (ExtTreeSet α cmp) where
+  beq m₁ m₂ := ExtDTreeMap.Const.beq m₁.inner.inner m₂.inner.inner
+
+instance [TransCmp cmp] : ReflBEq (ExtTreeSet α cmp) where
+  rfl := ExtDTreeMap.Const.beq_of_eq _ _ rfl
+
+instance [TransCmp cmp] [LawfulEqCmp cmp] : LawfulBEq (ExtTreeSet α cmp) where
+  eq_of_beq {a} {b} hyp := by
+    have ⟨⟨_⟩⟩ := a
+    have ⟨⟨_⟩⟩ := b
+    simp only [mk.injEq, ExtTreeMap.mk.injEq] at |- hyp
+    exact ExtDTreeMap.Const.eq_of_beq _ _ hyp
+    
 /--
 Computes the difference of the given tree sets.
 

src/Std/Data/TreeMap/Basic.lean

@@ -501,6 +501,11 @@ def inter (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp :=
 
 instance : Inter (TreeMap α β cmp) := ⟨inter⟩
 
+@[inherit_doc DTreeMap.beq] def beq [BEq β] (t₁ t₂ : TreeMap α β cmp) : Bool :=
+  letI : Ord α := ⟨cmp⟩; DTreeMap.Const.beq t₁.inner t₂.inner
+
+instance [BEq β] : BEq (TreeMap α β cmp) := ⟨beq⟩
+
 @[inline, inherit_doc DTreeMap.diff]
 def diff (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp :=
   letI : Ord α := ⟨cmp⟩; ⟨DTreeMap.diff t₁.inner t₂.inner⟩

src/Std/Data/TreeMap/Lemmas.lean

@@ -2077,6 +2077,21 @@ theorem isEmpty_inter_iff [TransCmp cmp] :
 
 end Inter
 
+section
+
+variable {β : Type v} {m₁ m₂ : TreeMap α β cmp} [BEq β]
+
+theorem Equiv.beq [TransCmp cmp] [ReflBEq β] (h : m₁ ~m m₂) : m₁ == m₂ :=
+  DTreeMap.Const.Equiv.beq h.1
+
+theorem equiv_of_beq [TransCmp cmp] [LawfulEqCmp cmp] [LawfulBEq β] (h : m₁ == m₂) : m₁ ~m m₂ :=
+  ⟨DTreeMap.Const.equiv_of_beq h⟩
+
+theorem Equiv.beq_congr [TransCmp cmp] {m₃ m₄ : TreeMap α β cmp} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) :=
+  DTreeMap.Const.Equiv.beq_congr w₁.1 w₂.1
+
+end
+
 section Diff
 
 variable {t₁ t₂ : TreeMap α β cmp}

src/Std/Data/TreeMap/Raw/Basic.lean

@@ -503,6 +503,11 @@ def inter (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
 
 instance : Inter (Raw α β cmp) := ⟨inter⟩
 
+@[inherit_doc DTreeMap.beq] def beq [BEq β] (t₁ t₂ : Raw α β cmp) : Bool :=
+  letI : Ord α := ⟨cmp⟩; DTreeMap.Raw.Const.beq t₁.inner t₂.inner
+
+instance [BEq β] : BEq (Raw α β cmp) := ⟨beq⟩
+
 @[inline, inherit_doc DTreeMap.Raw.diff]
 def diff (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
   ⟨DTreeMap.Raw.diff t₁.inner t₂.inner⟩

src/Std/Data/TreeMap/Raw/Lemmas.lean

@@ -2129,6 +2129,20 @@ theorem isEmpty_inter_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
 
 end Inter
 
+section
+variable {β : Type v} {m₁ m₂ : Raw α β cmp}
+
+theorem Const.Equiv.beq [TransCmp cmp] [BEq β] [ReflBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : m₁ == m₂ :=
+  DTreeMap.Raw.Const.Equiv.beq h₁ h₂ h.1
+
+theorem Const.equiv_of_beq [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (k : m₁ == m₂) : m₁ ~m m₂ :=
+  ⟨DTreeMap.Raw.Const.equiv_of_beq h₁.1 h₂.1 k⟩
+
+theorem Const.Equiv.beq_congr [TransCmp cmp] [BEq β] {m₃ m₄ : Raw α β cmp} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) :=
+  DTreeMap.Raw.Const.Equiv.beq_congr h₁ h₂ h₃ h₄ w₁.1 w₂.1
+
+end
+
 section Diff
 
 variable {t₁ t₂ : Raw α β cmp}

src/Std/Data/TreeSet/Basic.lean

@@ -503,6 +503,16 @@ def inter (t₁ t₂ : TreeSet α cmp) : TreeSet α cmp :=
 
 instance : Inter (TreeSet α cmp) := ⟨inter⟩
 
+/--
+Compares two tree sets using Boolean equality on keys.
+
+Returns `true` if the sets contain the same keys, `false` otherwise.
+-/
+def beq (t₁ t₂ : TreeSet α cmp) : Bool :=
+  letI : Ord α := ⟨cmp⟩; TreeMap.beq t₁.inner t₂.inner
+
+instance : BEq (TreeSet α cmp) := ⟨beq⟩
+
 /--
 Computes the difference of the given tree sets.
 

src/Std/Data/TreeSet/Lemmas.lean

@@ -778,6 +778,20 @@ theorem isEmpty_inter_iff [TransCmp cmp] :
 
 end Inter
 
+section
+variable {m₁ m₂ : TreeSet α cmp}
+
+theorem Equiv.beq [TransCmp cmp] (h : m₁ ~m m₂) : m₁ == m₂ :=
+  TreeMap.Equiv.beq h.1
+
+theorem equiv_of_beq [TransCmp cmp] [LawfulEqCmp cmp] (h : m₁ == m₂) : m₁ ~m m₂ :=
+  ⟨TreeMap.equiv_of_beq h⟩
+
+theorem Equiv.beq_congr [TransCmp cmp] {m₃ m₄ : TreeSet α cmp} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) :=
+  TreeMap.Equiv.beq_congr w₁.1 w₂.1
+
+end
+
 section Diff
 
 variable {t₁ t₂ : TreeSet α cmp}

src/Std/Data/TreeSet/Raw/Basic.lean

@@ -353,6 +353,11 @@ def inter (t₁ t₂ : Raw α cmp) : Raw α cmp :=
 
 instance : Inter (Raw α cmp) := ⟨inter⟩
 
+@[inherit_doc TreeSet.beq] def beq (t₁ t₂ : Raw α cmp) : Bool :=
+  letI : Ord α := ⟨cmp⟩; TreeMap.Raw.beq t₁.inner t₂.inner
+
+instance : BEq (Raw α cmp) := ⟨beq⟩
+
 /--
 Computes the difference of the given tree sets.
 

src/Std/Data/TreeSet/Raw/Lemmas.lean

@@ -818,6 +818,20 @@ theorem isEmpty_inter_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
 
 end Inter
 
+section
+variable {m₁ m₂ : Raw α cmp}
+
+theorem Equiv.beq [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : beq m₁ m₂ :=
+  TreeMap.Raw.Const.Equiv.beq h₁ h₂ h.1
+
+theorem equiv_of_beq [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ == m₂): m₁ ~m m₂ :=
+  ⟨TreeMap.Raw.Const.equiv_of_beq h₁.1 h₂.1 h⟩
+
+theorem Equiv.beq_congr [TransCmp cmp] {m₃ m₄ : Raw α cmp} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) :=
+  TreeMap.Raw.Const.Equiv.beq_congr h₁.1 h₂.1 h₃.1 h₄.1 w₁.1 w₂.1
+
+end
+
 section Diff
 
 variable {t₁ t₂ : Raw α cmp}