Small style fixes

leanprover · Dec 28, 2024 · 62f5a53 · 62f5a53
1 parent e1234aa
commit 62f5a53
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 4 deletions.
diff --git 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
@@ -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]