chore: generalize a lemma about insertIfNew

Author: wkrozowski

src/Std/Data/DHashMap/Internal/RawLemmas.lean

@@ -404,7 +404,7 @@ theorem get_insert_self [LawfulBEq α] (h : m.1.WF) {k : α} {v : β k} :
 
 theorem toList_insert_perm [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
     (m.insert k v).1.toList.Perm (⟨k, v⟩ :: m.1.toList.filter (¬k == ·.1)) := by
-  simp_to_model using List.Perm.trans (toListModel_insert (by wf_trivial)) <| List.insertEntry_perm_filter _ _ _
+  simp_to_model using List.Perm.trans (toListModel_insert _) <| List.insertEntry_perm_filter _ _ _
 
 theorem Const.toList_insert_perm {β : Type v} (m : Raw₀ α (fun _ => β)) [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β} :
     (Raw.Const.toList (m.insert k v).1).Perm ((k, v) :: (Raw.Const.toList m.1).filter (¬k == ·.1)) := by
@@ -413,14 +413,14 @@ theorem Const.toList_insert_perm {β : Type v} (m : Raw₀ α (fun _ => β)) [Eq
   apply List.Perm.trans <| List.Const.map_insertEntry_perm_filter_map _ _ (by wf_trivial)
   simp
 
-theorem Const.keys_insertIfNew_perm (m : Raw₀ α (fun _ => Unit)) [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
-    (m.insertIfNew k ()).1.keys.Perm (if m.contains k then m.1.keys else k :: m.1.keys) := by
+theorem keys_insertIfNew_perm [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k}:
+    (m.insertIfNew k v).1.keys.Perm (if m.contains k then m.1.keys else k :: m.1.keys) := by
   simp_to_model
   apply List.Perm.trans
-  · simp only [keys_eq_map]
-    apply List.Perm.map _ <|  toListModel_insertIfNew (by wf_trivial)
+  simp only [keys_eq_map]
+  apply List.Perm.map _ <| toListModel_insertIfNew (by wf_trivial)
   simp only [← keys_eq_map]
-  apply List.Const.keys_insertEntryIfNew_perm
+  apply List.keys_insertEntryIfNew_perm
 
 @[simp]
 theorem get_erase [LawfulBEq α] (h : m.1.WF) {k a : α} {h'} :

src/Std/Data/DHashMap/Lemmas.lean

@@ -392,9 +392,9 @@ theorem Const.toList_insert_perm {β : Type v} {m : DHashMap α (fun _ => β)} [
     (Const.toList (m.insert k v)).Perm (⟨k, v⟩ :: (Const.toList m).filter (¬k == ·.1)) :=
   Raw₀.Const.toList_insert_perm ⟨m.1, _⟩ m.2
 
-theorem Const.keys_insertIfNew_perm {m : DHashMap α (fun _ => Unit)} [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m.insertIfNew k ()).keys.Perm (if k ∈ m then m.keys else k :: m.keys) :=
-  Raw₀.Const.keys_insertIfNew_perm ⟨m.1, _⟩ m.2
+theorem keys_insertIfNew_perm [EquivBEq α] [LawfulHashable α] {k : α} {v : β k}:
+    (m.insertIfNew k v).keys.Perm (if k ∈ m then m.keys else k :: m.keys) :=
+  Raw₀.keys_insertIfNew_perm ⟨m.1, _⟩ m.2
 
 @[simp, grind =]
 theorem get_erase [LawfulBEq α] {k a : α} {h'} :

src/Std/Data/DHashMap/RawLemmas.lean

@@ -451,10 +451,10 @@ theorem Const.toList_insert_perm {β : Type v} {m : Raw α (fun _ => β)} [Equiv
     (Const.toList (m.insert k v)).Perm ((k, v) :: (Const.toList m).filter (¬k == ·.1)) := by
   simp_to_raw using Raw₀.Const.toList_insert_perm ⟨m, _⟩
 
-theorem Const.keys_insertIfNew_perm {m : Raw α (fun _ => Unit)} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
-    (m.insertIfNew k ()).keys.Perm (if k ∈ m then m.keys else k :: m.keys) := by
+theorem keys_insertIfNew_perm [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
+    (m.insertIfNew k v).keys.Perm (if k ∈ m then m.keys else k :: m.keys) := by
   simp only [Membership.mem]
-  simp_to_raw using Raw₀.Const.keys_insertIfNew_perm ⟨m, _⟩
+  simp_to_raw using Raw₀.keys_insertIfNew_perm ⟨m, _⟩
 
 @[simp, grind =]
 theorem get_erase [LawfulBEq α] (h : m.WF) {k a : α} {h'} :

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

@@ -681,20 +681,20 @@ theorem Const.insert!_toList_perm {β : Type v} {t : Impl α (fun _ => β)} [BEq
     (Const.toList (t.insert! k v)).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) := by
   simpa only [insert_eq_insert!] using Const.toList_insert_perm h
 
-theorem Const.keys_insertIfNew_perm {t : Impl α (fun _ => Unit)} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} :
-    (t.insertIfNew k () h.balanced).1.keys.Perm (if t.contains k then t.keys else k :: t.keys) := by
+theorem keys_insertIfNew_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k}:
+    (t.insertIfNew k v h.balanced).1.keys.Perm (if t.contains k then t.keys else k :: t.keys) := by
   simp_to_model
   apply List.Perm.trans
   simp only [List.keys_eq_map]
   apply List.Perm.map _ <| toListModel_insertIfNew _ h.ordered
   simp only [← List.keys_eq_map]
   apply List.Perm.trans
-  apply List.Const.keys_insertEntryIfNew_perm
+  apply List.keys_insertEntryIfNew_perm
   simp
 
-theorem Const.keys_insertIfNew!_perm {t : Impl α (fun _ => Unit)} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} :
-    (t.insertIfNew! k ()).keys.Perm (if t.contains k then t.keys else k :: t.keys) := by
-    simpa only [insertIfNew_eq_insertIfNew!] using Const.keys_insertIfNew_perm h
+theorem keys_insertIfNew!_perm {t : Impl α β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew! k v).keys.Perm (if t.contains k then t.keys else k :: t.keys) := by
+    simpa only [insertIfNew_eq_insertIfNew!] using keys_insertIfNew_perm h
 
 theorem get_insert_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} :
     (t.insert k v h.balanced).impl.get k (contains_insert_self h) = v := by

src/Std/Data/DTreeMap/Lemmas.lean

@@ -364,9 +364,9 @@ theorem Const.toList_insert_perm {β : Type v} {t : DTreeMap α (fun _ => β) cm
     (Const.toList (t.insert k v)).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) :=
   Impl.Const.toList_insert_perm t.2
 
-theorem Const.keys_insertIfNew_perm {t : DTreeMap α (fun _ => Unit) cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} :
-    (t.insertIfNew k ()).keys.Perm (if k ∈ t then t.keys else k :: t.keys) :=
-  Impl.Const.keys_insertIfNew_perm t.2
+theorem keys_insertIfNew_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β k} :
+    (t.insertIfNew k v).keys.Perm (if k ∈ t then t.keys else k :: t.keys) :=
+  Impl.keys_insertIfNew_perm t.2
 
 @[simp]
 theorem get_insert_self [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :

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

@@ -358,9 +358,9 @@ theorem Const.toList_insert_perm {β : Type v} {t : Raw α (fun _ => β) cmp} [B
     (Const.toList (t.insert k v)).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) :=
   Impl.Const.insert!_toList_perm h
 
-theorem Const.keys_insertIfNew_perm {t : Raw α (fun _ => 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) :=
-  Impl.Const.keys_insertIfNew!_perm h
+theorem keys_insertIfNew_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v).keys.Perm (if k ∈ t then t.keys else k :: t.keys) :=
+  Impl.keys_insertIfNew!_perm h
 
 @[grind =] theorem get_insert [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {v : β k} {h₁} :
     (t.insert k v).get a h₁ =

src/Std/Data/HashMap/Lemmas.lean

@@ -318,9 +318,9 @@ theorem toList_insert_perm [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     (m.insert k v).toList.Perm (⟨k, v⟩ :: m.toList.filter (¬k == ·.1)) :=
   DHashMap.Const.toList_insert_perm
 
-theorem keys_insertIfNew_perm {m : DHashMap α (fun _ => Unit)} [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m.insertIfNew k ()).keys.Perm (if k ∈ m then m.keys else k :: m.keys) :=
-  DHashMap.Const.keys_insertIfNew_perm
+theorem keys_insertIfNew_perm [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+    (m.insertIfNew k v).keys.Perm (if k ∈ m then m.keys else k :: m.keys) :=
+  DHashMap.keys_insertIfNew_perm
 
 @[simp]
 theorem getElem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :

src/Std/Data/HashMap/RawLemmas.lean

@@ -327,9 +327,9 @@ theorem toList_insert_perm [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
     (m.insert k v).toList.Perm (⟨k, v⟩ :: m.toList.filter (¬k == ·.1)) :=
   DHashMap.Raw.Const.toList_insert_perm h.out
 
-theorem keys_insertIfNew_perm {m : Raw α Unit} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
-    (m.insertIfNew k ()).keys.Perm (if k ∈ m then m.keys else k :: m.keys) :=
-  DHashMap.Raw.Const.keys_insertIfNew_perm h.out
+theorem keys_insertIfNew_perm [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
+    (m.insertIfNew k v).keys.Perm (if k ∈ m then m.keys else k :: m.keys) :=
+  DHashMap.Raw.keys_insertIfNew_perm h.out
 
 @[simp]
 theorem getElem_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :

src/Std/Data/HashSet/RawLemmas.lean

@@ -302,7 +302,7 @@ theorem get?_eq_some [LawfulBEq α] (h : m.WF) {k : α} (h' : k ∈ m) :
 
 theorem toList_insert_perm [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     (m.insert k).toList.Perm (if k ∈ m then m.toList else k :: m.toList) :=
-  HashMap.Raw.keys_insertIfNew_perm h.out
+  HashMap.Raw.keys_insertIfNew_perm (v := ()) h.out
 
 @[simp, grind =]
 theorem get_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} :

src/Std/Data/Internal/List/Associative.lean

@@ -6964,9 +6964,9 @@ theorem Const.map_insertEntry_perm_filter_map {β : Type v} [BEq α] [EquivBEq 
       simp [heq]
       apply ih hl.1
 
-theorem Const.keys_insertEntryIfNew_perm [BEq α] [EquivBEq α]
-    (k : α) {l : List ((_ : α) × Unit)} :
-    (keys <| insertEntryIfNew k () l).Perm <| if (containsKey k l) then keys l else k :: keys l := by
+theorem keys_insertEntryIfNew_perm [BEq α] [EquivBEq α]
+    (k : α) (v : β k) {l : List ((a : α) × β a)} :
+    (keys <| insertEntryIfNew k v l).Perm <| if (containsKey k l) then keys l else k :: keys l := by
   simp only [insertEntryIfNew]
   by_cases h : containsKey k l <;> simp [h]