diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index 1ce5dd2b5fc8..00849a9c3282 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -926,7 +926,7 @@ theorem getD_insertMany_list_of_mem [LawfulBEq α] (h : m.1.WF) theorem getKey?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List ((a : α) × β a)} {k : α} - (h : (l.map Sigma.fst).contains k = false) : + (h' : (l.map Sigma.fst).contains k = false) : (m.insertMany l).1.getKey? k = m.getKey? k := by simp_to_model using getKey?_insertList_of_contains_eq_false @@ -984,7 +984,7 @@ theorem getKeyD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m. simp_to_model using getKeyD_insertList_of_mem theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF) - {l : List ((a : α) × β a)} {distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)} : + {l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) : (∀ (a : α), m.contains a → (l.map Sigma.fst).contains a = false) → (m.insertMany l).1.1.size = m.1.size + l.length := by simp_to_model using length_insertList diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index 3c4f8c8a5b95..4a323de994ce 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -1217,12 +1217,14 @@ theorem insertMany_nil [EquivBEq α] [LawfulHashable α] (h : m.WF) : rw [Raw₀.Const.insertMany_nil] @[simp] -theorem insertMany_list_singleton {k : α} {v : β} [EquivBEq α] [LawfulHashable α] (h : m.WF) : +theorem insertMany_list_singleton [EquivBEq α] [LawfulHashable α] (h : m.WF) + {k : α} {v : β} : insertMany m [⟨k, v⟩] = m.insert k v := by simp_to_raw rw [Raw₀.Const.insertMany_list_singleton] -theorem insertMany_cons {l : List (α × β)} {k : α} {v : β} [EquivBEq α] [LawfulHashable α] (h : m.WF) : +theorem insertMany_cons [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List (α × β)} + {k : α} {v : β} : insertMany m (⟨k, v⟩ :: l) = insertMany (m.insert k v) l := by simp_to_raw rw [Raw₀.Const.insertMany_cons]