cleanups

Author: datokrat

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

@@ -10339,14 +10339,14 @@ theorem keys_filter [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bo
   rw [List.keys_filter h.ordered.distinctKeys]
   simp only [List.filter_map, Function.comp_def, List.unattach, List.map_map]
 
-private theorem _root_.List.unattach_filter_eq_if {p : α → Prop} {l : List { x // p x }}
+private theorem List.unattach_filter_eq_if {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → Bool} :
     open scoped Classical in
     (l.filter f).unattach = l.unattach.filter (fun x => if h : p x then f ⟨x, h⟩ else false) := by
   apply List.unattach_filter
   simp +contextual
 
-private theorem _root_.Array.unattach_filter_eq_if {p : α → Prop} {xs : Array { x // p x }}
+private theorem Array.unattach_filter_eq_if {p : α → Prop} {xs : Array { x // p x }}
     {f : { x // p x } → Bool} :
     open scoped Classical in
     (xs.filter f).unattach = xs.unattach.filter (fun x => if h : p x then f ⟨x, h⟩ else false) := by

src/Std/Data/DTreeMap/Lemmas.lean

@@ -1137,6 +1137,7 @@ theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
     k ∈ t.keys ↔ k ∈ t :=
   Impl.mem_keys t.wf
 
+@[simp, grind =]
 theorem mem_keysArray [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
     k ∈ t.keysArray ↔ k ∈ t :=
   Impl.mem_keysArray t.wf

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

@@ -1167,6 +1167,7 @@ theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
     k ∈ t.keys ↔ k ∈ t :=
   Impl.mem_keys h
 
+@[simp, grind =]
 theorem mem_keysArray [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
     k ∈ t.keysArray ↔ k ∈ t :=
   Impl.mem_keysArray h

src/Std/Data/TreeMap/Lemmas.lean

@@ -298,6 +298,9 @@ theorem getElem?_congr [TransCmp cmp] {a b : α} (hab : cmp a b = .eq) :
 theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β} :
     (t.insert k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) := DTreeMap.Const.toList_insert_perm
 
+theorem toArray_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β} :
+    (t.insert k v).toArray.Perm ((t.toArray.filter (¬k == ·.1)).push ⟨k, v⟩) := DTreeMap.Const.toArray_insert_perm
+
 theorem keys_insertIfNew_perm {t : TreeMap α Unit cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} :
     (t.insertIfNew k ()).keys.Perm (if k ∈ t then t.keys else k :: t.keys) :=
   DTreeMap.keys_insertIfNew_perm
@@ -839,6 +842,7 @@ theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
     k ∈ t.keys ↔ k ∈ t :=
   DTreeMap.mem_keys
 
+@[simp, grind =]
 theorem mem_keysArray [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
     k ∈ t.keysArray ↔ k ∈ t :=
   DTreeMap.mem_keysArray
@@ -4569,6 +4573,7 @@ theorem toList_filterMap {f : (a : α) → β → Option γ} :
       t.toList.filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) :=
   DTreeMap.Const.toList_filterMap
 
+@[simp, grind =]
 theorem toArray_filterMap {f : α → β → Option γ} :
     (t.filterMap f).toArray =
       t.toArray.filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) :=
@@ -4741,6 +4746,7 @@ theorem toList_filter {f : α → β → Bool} :
     (t.filter f).toList = t.toList.filter (fun p => f p.1 p.2) :=
   DTreeMap.Const.toList_filter
 
+@[simp, grind =]
 theorem toArray_filter {f : α → β → Bool} :
     (t.filter f).toArray = t.toArray.filter (fun p => f p.1 p.2) :=
   DTreeMap.Const.toArray_filter
@@ -4936,6 +4942,7 @@ theorem toList_map {f : α → β → γ} :
     (t.map f).toList = t.toList.map (fun p => (p.1, f p.1 p.2)) :=
   DTreeMap.Const.toList_map
 
+@[simp, grind =]
 theorem toArray_map {f : α → β → γ} :
     (t.map f).toArray = t.toArray.map (fun p => (p.1, f p.1 p.2)) :=
   DTreeMap.Const.toArray_map

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

@@ -294,6 +294,10 @@ theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF)
     (t.insert k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) :=
   DTreeMap.Raw.Const.toList_insert_perm h
 
+theorem toArray_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (t.insert k v).toArray.Perm ((t.toArray.filter (¬k == ·.1)).push ⟨k, v⟩) :=
+  DTreeMap.Raw.Const.toArray_insert_perm h
+
 theorem keys_insertIfNew_perm {t : Raw α Unit cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} :
     (t.insertIfNew k ()).keys.Perm (if k ∈ t then t.keys else k :: t.keys) :=
   DTreeMap.Raw.keys_insertIfNew_perm h
@@ -841,6 +845,7 @@ theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
     k ∈ t.keys ↔ k ∈ t :=
   DTreeMap.Raw.mem_keys h
 
+@[simp, grind =]
 theorem mem_keysArray [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
     k ∈ t.keysArray ↔ k ∈ t :=
   DTreeMap.Raw.mem_keysArray h

src/Std/Data/TreeSet/Lemmas.lean

@@ -293,6 +293,10 @@ theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} :
     (t.insert k).toList.Perm (if k ∈ t then t.toList else k :: t.toList) :=
   DTreeMap.keys_insertIfNew_perm
 
+theorem toArray_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} :
+    (t.insert k).toArray.Perm (if k ∈ t then t.toArray else t.toArray.push k) :=
+  DTreeMap.keysArray_insertIfNew_perm
+
 @[simp, grind =] theorem get_erase [TransCmp cmp] {k a : α} {h'} :
     (t.erase k).get a h' = t.get a (mem_of_mem_erase h') :=
   TreeMap.getKey_erase
@@ -485,12 +489,12 @@ theorem contains_toArray [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} :
     t.toArray.contains k = t.contains k := by
   simp [← toArray_toList, contains_toList]
 
-@[simp]
+@[simp, grind =]
 theorem mem_toList [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
     k ∈ t.toList ↔ k ∈ t :=
   TreeMap.mem_keys
 
-@[simp]
+@[simp, grind =]
 theorem mem_toArray [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
     k ∈ t.toArray ↔ k ∈ t :=
   TreeMap.mem_keysArray
@@ -1610,7 +1614,7 @@ theorem min!_eq_head!_toList [TransCmp cmp] [Inhabited α] :
     t.min! = t.toList.head! :=
   TreeMap.minKey!_eq_head!_keys
 
-theorem min!_eq_get!_toArray [TransCmp cmp] [Inhabited α] :
+theorem min!_eq_getElem!_toArray [TransCmp cmp] [Inhabited α] :
     t.min! = t.toArray[0]! :=
   TreeMap.minKey!_eq_getElem!_keysArray
 

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

@@ -1560,7 +1560,7 @@ theorem min!_eq_head!_toList [TransCmp cmp] [Inhabited α] (h : t.WF) :
   TreeMap.Raw.minKey!_eq_head!_keys h
 
 @[grind =_]
-theorem min!_eq_getElem!_toArray_zero [TransCmp cmp] [Inhabited α] (h : t.WF) :
+theorem min!_eq_getElem!_toArray [TransCmp cmp] [Inhabited α] (h : t.WF) :
     t.min! = t.toArray[0]! :=
   TreeMap.Raw.minKey!_eq_getElem!_keysArray h