more lemmas

Author: datokrat

src/Std/Data/DTreeMap/Lemmas.lean

@@ -6142,6 +6142,10 @@ theorem equiv_iff_toList_eq [TransCmp cmp] :
     t₁ ~m t₂ ↔ t₁.toList = t₂.toList :=
   equiv_iff_equiv.trans (Impl.equiv_iff_toList_eq t₁.2 t₂.2)
 
+theorem equiv_iff_toArray_eq [TransCmp cmp] :
+    t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray :=
+  equiv_iff_equiv.trans (Impl.equiv_iff_toArray_eq t₁.2 t₂.2)
+
 theorem insertMany_list_equiv_foldl {l : List ((a : α) × β a)} :
     t₁.insertMany l ~m l.foldl (init := t₁) fun acc p => acc.insert p.1 p.2 := by
   constructor
@@ -6175,6 +6179,9 @@ theorem Const.equiv_iff_toArray_perm : t₁ ~m t₂ ↔ (Const.toArray t₁).Per
 theorem Const.equiv_iff_toList_eq [TransCmp cmp] : t₁ ~m t₂ ↔ Const.toList t₁ = Const.toList t₂ :=
   equiv_iff_equiv.trans (Impl.Const.equiv_iff_toList_eq t₁.2 t₂.2)
 
+theorem Const.equiv_iff_toArray_eq [TransCmp cmp] : t₁ ~m t₂ ↔ Const.toArray t₁ = Const.toArray t₂ :=
+  equiv_iff_equiv.trans (Impl.Const.equiv_iff_toArray_eq t₁.2 t₂.2)
+
 theorem Const.equiv_iff_keys_unit_perm {t₁ t₂ : DTreeMap α Unit cmp} : t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys :=
   equiv_iff_equiv.trans Impl.Const.equiv_iff_keys_perm
 

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

@@ -6010,6 +6010,10 @@ theorem equiv_iff_toList_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
     t₁ ~m t₂ ↔ t₁.toList = t₂.toList :=
   equiv_iff.trans (Impl.equiv_iff_toList_eq h₁.1 h₂.1)
 
+theorem equiv_iff_toArray_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
+    t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray :=
+  equiv_iff.trans (Impl.equiv_iff_toArray_eq h₁.1 h₂.1)
+
 theorem insertMany_list_equiv_foldl {l : List ((a : α) × β a)} :
     t₁.insertMany l ~m l.foldl (init := t₁) fun acc p => acc.insert p.1 p.2 := by
   constructor
@@ -6036,6 +6040,10 @@ theorem Const.equiv_iff_toList_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.W
     t₁ ~m t₂ ↔ Const.toList t₁ = Const.toList t₂ :=
   equiv_iff.trans (Impl.Const.equiv_iff_toList_eq h₁.1 h₂.1)
 
+theorem Const.equiv_iff_toArray_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
+    t₁ ~m t₂ ↔ Const.toArray t₁ = Const.toArray t₂ :=
+  equiv_iff.trans (Impl.Const.equiv_iff_toArray_eq h₁.1 h₂.1)
+
 theorem Const.equiv_iff_keys_unit_perm {t₁ t₂ : Raw α Unit cmp} :
     t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys :=
   equiv_iff.trans Impl.Const.equiv_iff_keys_perm

src/Std/Data/TreeMap/Lemmas.lean

@@ -4508,6 +4508,10 @@ theorem equiv_iff_toList_eq [TransCmp cmp] :
     t₁ ~m t₂ ↔ t₁.toList = t₂.toList :=
   equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_toList_eq
 
+theorem equiv_iff_toArray_eq [TransCmp cmp] :
+    t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray :=
+  equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_toArray_eq
+
 theorem equiv_iff_keys_unit_perm {t₁ t₂ : TreeMap α Unit cmp} :
     t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys :=
   equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_keys_unit_perm

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

@@ -4235,13 +4235,23 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty :=
 theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList :=
   equiv_iff.trans DTreeMap.Raw.Const.equiv_iff_toList_perm
 
+theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray :=
+  equiv_iff.trans DTreeMap.Raw.Const.equiv_iff_toArray_perm
+
 theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ :=
   ⟨.of_constToList_perm h⟩
 
+theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ :=
+  ⟨.of_constToArray_perm h⟩
+
 theorem equiv_iff_toList_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
     t₁ ~m t₂ ↔ t₁.toList = t₂.toList :=
   equiv_iff.trans (DTreeMap.Raw.Const.equiv_iff_toList_eq h₁.1 h₂.1)
 
+theorem equiv_iff_toArray_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
+    t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray :=
+  equiv_iff.trans (DTreeMap.Raw.Const.equiv_iff_toArray_eq h₁.1 h₂.1)
+
 theorem equiv_iff_keys_unit_perm {t₁ t₂ : Raw α Unit cmp} :
     t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys :=
   equiv_iff.trans DTreeMap.Raw.Const.equiv_iff_keys_unit_perm

src/Std/Data/TreeSet/Lemmas.lean

@@ -8,6 +8,7 @@ module
 prelude
 import Std.Data.TreeMap.Lemmas
 import Std.Data.DTreeMap.Lemmas
+public import Init.Data.Array.Perm
 public import Std.Data.TreeSet.AdditionalOperations
 
 @[expose] public section
@@ -2386,17 +2387,27 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty :=
 theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList :=
   equiv_iff_equiv.trans TreeMap.equiv_iff_keys_unit_perm
 
+theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray :=
+  equiv_iff_equiv.trans TreeMap.equiv_iff_keysArray_unit_perm
+
 theorem equiv_iff_forall_mem_iff [TransCmp cmp] [LawfulEqCmp cmp] :
     t₁ ~m t₂ ↔ (∀ k, k ∈ t₁ ↔ k ∈ t₂) :=
   ⟨fun h _ => h.mem_iff, Equiv.of_forall_mem_iff⟩
 
 theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ :=
   ⟨.of_keys_unit_perm h⟩
 
+theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ :=
+  ⟨.of_keysArray_unit_perm h⟩
+
 theorem equiv_iff_toList_eq [TransCmp cmp] :
     t₁ ~m t₂ ↔ t₁.toList = t₂.toList :=
   equiv_iff_equiv.trans TreeMap.equiv_iff_keys_unit_eq
 
+theorem equiv_iff_toArray_eq [TransCmp cmp] :
+    t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray :=
+  equiv_iff_equiv.trans TreeMap.equiv_iff_keysArray_unit_eq
+
 theorem insertMany_list_equiv_foldl {l : List α} :
     insertMany t₁ l ~m l.foldl (init := t₁) fun acc a => acc.insert a := by
   constructor