From ae25818a695f7b63cb9aca47342afe03aff3885f Mon Sep 17 00:00:00 2001
From: monsterkrampe <monsterkrampe@users.noreply.github.com>
Date: Tue, 3 Dec 2024 16:27:23 +0100
Subject: [PATCH] Incorporate smaller remarks from PR

---
 src/Std/Data/DHashMap/Internal/List/Associative.lean |  2 +-
 src/Std/Data/DHashMap/Internal/RawLemmas.lean        |  6 +++---
 src/Std/Data/DHashMap/Internal/WF.lean               | 11 -----------
 3 files changed, 4 insertions(+), 15 deletions(-)

diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean
index d52543f3d951..217cabfc61ab 100644
--- a/src/Std/Data/DHashMap/Internal/List/Associative.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean
@@ -2750,7 +2750,7 @@ theorem getValue_insertListConst_of_mem [BEq α] [PartialEquivBEq α]
   . exact distinct
 
 /-- Internal implementation detail of the hash map -/
-def insertListIfNewUnit [BEq α] (l: List ((_ : α) × Unit))(toInsert: List α) :
+def insertListIfNewUnit [BEq α] (l: List ((_ : α) × Unit)) (toInsert: List α) :
     List ((_ : α) × Unit) :=
   match toInsert with
   | .nil => l
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index cedc1b443c4a..d12cb9d954ad 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -984,14 +984,14 @@ 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 : List.Pairwise (fun a b => (a.1 == b.1) = false) l}:
+    {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)) →
     (m.insertMany l).1.1.size = m.1.size + l.length := by
   simp_to_model using length_insertList
 
 theorem isEmpty_insertMany_list_eq_false_of_isEmpty_eq_false [EquivBEq α] [LawfulHashable α]
     (h : m.1.WF) {l : List ((a : α) × β a)}:
-    (m.1.isEmpty = false) → (m.insertMany l).1.1.isEmpty  = false := by
+    (m.1.isEmpty = false) → (m.insertMany l).1.1.isEmpty = false := by
   simp_to_model using isEmpty_insertList_eq_false_of_isEmpty_eq_false
 
 theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
@@ -1000,7 +1000,7 @@ theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
   simp_to_model using isEmpty_insertList
 
 section
-variable {β: Type v} (m: Raw₀ α (fun _ => β))
+variable {β : Type v} (m : Raw₀ α (fun _ => β))
 
 theorem get?_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List ((_ : α) × β)} {k : α} (h : (l.map Sigma.fst).contains k = false) :
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 7c199d9a3a09..95bde8df4309 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -708,17 +708,6 @@ theorem wfImp_filter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m
 
 /-! # `insertListₘ` -/
 
-theorem wfImp_insertListₘ [BEq α] [Hashable α] [EquivBEq α][LawfulHashable α] {m : Raw₀ α β}
-    {l : List ((a : α) × β a)} (h : Raw.WFImp m.1) : Raw.WFImp (m.insertListₘ l).1 := by
-  induction l generalizing m with
-  | nil =>
-    simp only [insertListₘ]
-    exact h
-  | cons hd tl ih =>
-    simp only [insertListₘ]
-    apply ih
-    apply wfImp_insert h
-
 theorem toListModel_insertListₘ [BEq α] [Hashable α] [EquivBEq α][LawfulHashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.1) :
     Perm (toListModel (insertListₘ m l).1.buckets) (List.insertList (toListModel m.1.buckets) l) := by
   induction l generalizing m with