Style fixes & simplified equality lemmas

leanprover · Jan 15, 2025 · b43dfca · b43dfca
1 parent aea42fb
commit b43dfca
Show file tree

Hide file tree

Showing 7 changed files with 66 additions and 66 deletions.
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -1177,7 +1177,7 @@ theorem insertManyIfNewUnit_nil :
   simp [insertManyIfNewUnit, Id.run]
 
 @[simp]
-theorem insertManyIfNewUnit_list_singleton [EquivBEq α] [LawfulHashable α] {k : α} :
+theorem insertManyIfNewUnit_list_singleton {k : α} :
     insertManyIfNewUnit m [k] = m.insertIfNew k () := by
   simp [insertManyIfNewUnit, Id.run]
 
@@ -1319,16 +1319,16 @@ namespace Raw₀
 variable [BEq α] [Hashable α]
 
 @[simp]
-theorem insertMany_empty_list_nil [EquivBEq α] [LawfulHashable α] :
+theorem insertMany_empty_list_nil :
     (insertMany empty ([] : List ((a : α) × (β a)))).1 = empty := by
   simp
 
 @[simp]
-theorem insertMany_empty_list_singleton {k : α} {v : β k} [EquivBEq α] [LawfulHashable α] :
+theorem insertMany_empty_list_singleton {k : α} {v : β k} :
     (insertMany empty [⟨k, v⟩]).1 = empty.insert k v := by
   simp
 
-theorem insertMany_empty_list_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β k}
+theorem insertMany_empty_list_cons {k : α} {v : β k}
     {tl : List ((a : α) × (β a))} :
     (insertMany empty (⟨k, v⟩ :: tl)).1 = ((empty.insert k v).insertMany tl).1 := by
   rw [insertMany_cons]
@@ -1464,16 +1464,16 @@ namespace Const
 variable {β : Type v}
 
 @[simp]
-theorem insertMany_empty_list_nil [EquivBEq α] [LawfulHashable α] :
+theorem insertMany_empty_list_nil :
     (insertMany empty ([] : List (α × β))).1 = empty := by
   simp only [insertMany_nil]
 
 @[simp]
-theorem insertMany_empty_list_singleton {k : α} {v : β} [EquivBEq α] [LawfulHashable α] :
+theorem insertMany_empty_list_singleton {k : α} {v : β} :
     (insertMany empty [⟨k, v⟩]).1 = empty.insert k v := by
   simp only [insertMany_list_singleton]
 
-theorem insertMany_empty_list_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
+theorem insertMany_empty_list_cons {k : α} {v : β}
     {tl : List (α × β)} :
     (insertMany empty (⟨k, v⟩ :: tl)) = (insertMany (empty.insert k v) tl).1 := by
   rw [insertMany_cons]
@@ -1606,17 +1606,17 @@ theorem isEmpty_insertMany_empty_list [EquivBEq α] [LawfulHashable α]
   simp [isEmpty_insertMany_list _ Raw.WF.empty₀]
 
 @[simp]
-theorem insertManyIfNewUnit_empty_list_nil [EquivBEq α] [LawfulHashable α] :
+theorem insertManyIfNewUnit_empty_list_nil :
     insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) ([] : List α) =
       (empty : Raw₀ α (fun _ => Unit)) := by
   simp
 
 @[simp]
-theorem insertManyIfNewUnit_empty_list_singleton [EquivBEq α] [LawfulHashable α] {k : α} :
+theorem insertManyIfNewUnit_empty_list_singleton {k : α} :
     (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) [k]).1 = empty.insertIfNew k () := by
   simp
 
-theorem insertManyIfNewUnit_empty_list_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List α} :
+theorem insertManyIfNewUnit_empty_list_cons {hd : α} {tl : List α} :
     insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) (hd :: tl) =
       (insertManyIfNewUnit (empty.insertIfNew hd ()) tl).1 := by
   rw [insertManyIfNewUnit_cons]

diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
@@ -1308,7 +1308,7 @@ theorem insertManyIfNewUnit_nil :
     (Raw₀.Const.insertManyIfNewUnit_nil ⟨m.1, m.2.size_buckets_pos⟩) :)
 
 @[simp]
-theorem insertManyIfNewUnit_list_singleton [EquivBEq α] [LawfulHashable α] {k : α} :
+theorem insertManyIfNewUnit_list_singleton {k : α} :
     insertManyIfNewUnit m [k] = m.insertIfNew k () :=
   Subtype.eq (congrArg Subtype.val
     (Raw₀.Const.insertManyIfNewUnit_list_singleton ⟨m.1, m.2.size_buckets_pos⟩) :)
@@ -1337,11 +1337,11 @@ theorem mem_of_mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α]
 
 theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] {l : List α} {k : α}
-    (not_mem : ¬ k ∈ m) (contains_eq_false' : l.contains k = false) :
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
     getKey? (insertManyIfNewUnit m l) k = none := by
   simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
   exact Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    ⟨m.1, _⟩ m.2 not_mem contains_eq_false'
+    ⟨m.1, _⟩ m.2 not_mem contains_eq_false
 
 theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k k' : α} (k_beq : k == k')
@@ -1467,16 +1467,16 @@ end DHashMap
 namespace DHashMap
 
 @[simp]
-theorem ofList_nil [EquivBEq α] [LawfulHashable α] :
+theorem ofList_nil :
     ofList ([] : List ((a : α) × (β a))) = ∅ :=
   Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_empty_list_nil (α := α)) :)
 
 @[simp]
-theorem ofList_singleton {k : α} {v : β k} [EquivBEq α] [LawfulHashable α] :
+theorem ofList_singleton {k : α} {v : β k} :
     ofList [⟨k, v⟩] = (∅: DHashMap α β).insert k v :=
   Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_empty_list_singleton (α := α)) :)
 
-theorem ofList_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
+theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
     ofList (⟨k, v⟩ :: tl) = ((∅ : DHashMap α β).insert k v).insertMany tl :=
   Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_empty_list_cons (α := α)) :)
 
@@ -1611,16 +1611,16 @@ namespace Const
 variable {β : Type v}
 
 @[simp]
-theorem ofList_nil [EquivBEq α] [LawfulHashable α] :
+theorem ofList_nil :
     ofList ([] : List (α × β)) = ∅ :=
   Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_empty_list_nil (α:= α)) :)
 
 @[simp]
-theorem ofList_singleton {k : α} {v : β} [EquivBEq α] [LawfulHashable α] :
+theorem ofList_singleton {k : α} {v : β} :
     ofList [⟨k, v⟩] = (∅ : DHashMap α (fun _ => β)).insert k v :=
   Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_empty_list_singleton (α:= α)) :)
 
-theorem ofList_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β} {tl : List (α × β)} :
+theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : DHashMap α (fun _ => β)).insert k v) tl :=
   Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_empty_list_cons (α:= α)) :)
 
@@ -1751,16 +1751,16 @@ theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
   Raw₀.Const.isEmpty_insertMany_empty_list
 
 @[simp]
-theorem unitOfList_nil [EquivBEq α] [LawfulHashable α] :
+theorem unitOfList_nil :
     unitOfList ([] : List α) = ∅ :=
   Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_empty_list_nil (α := α)) :)
 
 @[simp]
-theorem unitOfList_singleton [EquivBEq α] [LawfulHashable α] {k : α} :
+theorem unitOfList_singleton {k : α} :
     unitOfList [k] = (∅ : DHashMap α (fun _ => Unit)).insertIfNew k () :=
   Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_empty_list_singleton (α := α)) :)
 
-theorem unitOfList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List α} :
+theorem unitOfList_cons {hd : α} {tl : List α} :
     unitOfList (hd :: tl) =
       insertManyIfNewUnit ((∅ : DHashMap α (fun _ => Unit)).insertIfNew hd ()) tl :=
   Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_empty_list_cons (α := α)) :)

diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1229,19 +1229,19 @@ namespace Const
 variable {β : Type v} {m : Raw α (fun _ => β)}
 
 @[simp]
-theorem insertMany_nil [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+theorem insertMany_nil (h : m.WF) :
     insertMany m [] = m := by
   simp_to_raw
   rw [Raw₀.Const.insertMany_nil]
 
 @[simp]
-theorem insertMany_list_singleton [EquivBEq α] [LawfulHashable α] (h : m.WF)
+theorem insertMany_list_singleton (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 [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List (α × β)}
+theorem insertMany_cons (h : m.WF) {l : List (α × β)}
     {k : α} {v : β} :
     insertMany m (⟨k, v⟩ :: l) = insertMany (m.insert k v) l := by
   simp_to_raw
@@ -1401,18 +1401,18 @@ theorem getD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
 variable {m : Raw α (fun _ => Unit)}
 
 @[simp]
-theorem insertManyIfNewUnit_nil [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+theorem insertManyIfNewUnit_nil (h : m.WF) :
     insertManyIfNewUnit m [] = m := by
   simp_to_raw
   rw [Raw₀.Const.insertManyIfNewUnit_nil]
 
 @[simp]
-theorem insertManyIfNewUnit_list_singleton [EquivBEq α] [LawfulHashable α] {k : α} (h : m.WF) :
+theorem insertManyIfNewUnit_list_singleton {k : α} (h : m.WF) :
     insertManyIfNewUnit m [k] = m.insertIfNew k () := by
   simp_to_raw
   rw [Raw₀.Const.insertManyIfNewUnit_list_singleton]
 
-theorem insertManyIfNewUnit_cons [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} :
+theorem insertManyIfNewUnit_cons (h : m.WF) {l : List α} {k : α} :
     insertManyIfNewUnit m (k :: l) = insertManyIfNewUnit (m.insertIfNew k ()) l := by
   simp_to_raw
   rw [Raw₀.Const.insertManyIfNewUnit_cons]
@@ -1570,13 +1570,13 @@ variable [BEq α] [Hashable α]
 open Internal.Raw Internal.Raw₀
 
 @[simp]
-theorem ofList_nil [EquivBEq α] [LawfulHashable α] :
+theorem ofList_nil :
     ofList ([] : List ((a : α) × (β a))) = ∅ := by
   simp_to_raw
   rw [Raw₀.insertMany_empty_list_nil]
 
 @[simp]
-theorem ofList_singleton {k : α} {v : β k} [EquivBEq α] [LawfulHashable α] :
+theorem ofList_singleton {k : α} {v : β k} :
     ofList [⟨k, v⟩] = (∅ : Raw α β).insert k v := by
   simp_to_raw
   rw [Raw₀.insertMany_empty_list_singleton]
@@ -1717,18 +1717,18 @@ namespace Const
 variable {β : Type v}
 
 @[simp]
-theorem ofList_nil [EquivBEq α] [LawfulHashable α] :
+theorem ofList_nil :
     ofList ([] : List (α × β)) = ∅ := by
   simp_to_raw
   simp
 
 @[simp]
-theorem ofList_singleton [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+theorem ofList_singleton {k : α} {v : β} :
     ofList [⟨k, v⟩] = (∅ : Raw α (fun _ => β)).insert k v := by
   simp_to_raw
   simp
 
-theorem ofList_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β} {tl : List (α × β)} :
+theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : Raw α (fun _ => β)).insert k v) tl := by
   simp_to_raw
   rw [Raw₀.Const.insertMany_empty_list_cons]
@@ -1860,18 +1860,18 @@ theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
   simp_to_raw using Raw₀.Const.isEmpty_insertMany_empty_list
 
 @[simp]
-theorem unitOfList_nil [EquivBEq α] [LawfulHashable α] :
+theorem unitOfList_nil :
     unitOfList ([] : List α) = ∅ := by
   simp_to_raw
   simp
 
 @[simp]
-theorem unitOfList_singleton [EquivBEq α] [LawfulHashable α] {k : α} :
+theorem unitOfList_singleton {k : α} :
     unitOfList [k] = (∅ : Raw α (fun _ => Unit)).insertIfNew k () := by
   simp_to_raw
   simp
 
-theorem unitOfList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List α} :
+theorem unitOfList_cons {hd : α} {tl : List α} :
     unitOfList (hd :: tl) = insertManyIfNewUnit ((∅ : Raw α (fun _ => Unit)).insertIfNew hd ()) tl := by
   simp_to_raw
   rw [Raw₀.Const.insertManyIfNewUnit_empty_list_cons]

diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
@@ -869,7 +869,7 @@ theorem insertManyIfNewUnit_nil :
   ext DHashMap.Const.insertManyIfNewUnit_nil
 
 @[simp]
-theorem insertManyIfNewUnit_list_singleton [EquivBEq α] [LawfulHashable α] {k : α} :
+theorem insertManyIfNewUnit_list_singleton {k : α} :
     insertManyIfNewUnit m [k] = m.insertIfNew k () :=
   ext DHashMap.Const.insertManyIfNewUnit_list_singleton
 
@@ -1014,16 +1014,16 @@ end
 section
 
 @[simp]
-theorem ofList_nil [EquivBEq α] [LawfulHashable α] :
+theorem ofList_nil :
     ofList ([] : List (α × β)) = ∅ :=
   ext DHashMap.Const.ofList_nil
 
 @[simp]
-theorem ofList_singleton {k : α} {v : β} [EquivBEq α] [LawfulHashable α] :
+theorem ofList_singleton {k : α} {v : β} :
     ofList [⟨k, v⟩] = (∅ : HashMap α β).insert k v :=
   ext DHashMap.Const.ofList_singleton
 
-theorem ofList_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β} {tl : List (α × β)} :
+theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : HashMap α β).insert k v) tl :=
   ext DHashMap.Const.ofList_cons
 
@@ -1154,16 +1154,16 @@ theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
   DHashMap.Const.isEmpty_ofList
 
 @[simp]
-theorem unitOfList_nil [EquivBEq α] [LawfulHashable α] :
+theorem unitOfList_nil :
     unitOfList ([] : List α) = ∅ :=
   ext DHashMap.Const.unitOfList_nil
 
 @[simp]
-theorem unitOfList_singleton [EquivBEq α] [LawfulHashable α] {k : α} :
+theorem unitOfList_singleton {k : α} :
     unitOfList [k] = (∅ : HashMap α Unit).insertIfNew k () :=
   ext DHashMap.Const.unitOfList_singleton
 
-theorem unitOfList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List α} :
+theorem unitOfList_cons {hd : α} {tl : List α} :
     unitOfList (hd :: tl) =
       insertManyIfNewUnit ((∅ : HashMap α Unit).insertIfNew hd ()) tl :=
   ext DHashMap.Const.unitOfList_cons

diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
@@ -706,17 +706,17 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
   DHashMap.Raw.distinct_keys h.out
 
 @[simp]
-theorem insertMany_nil [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+theorem insertMany_nil (h : m.WF) :
     insertMany m [] = m :=
   ext (DHashMap.Raw.Const.insertMany_nil h.out)
 
 @[simp]
-theorem insertMany_list_singleton [EquivBEq α] [LawfulHashable α] (h : m.WF)
+theorem insertMany_list_singleton (h : m.WF)
     {k : α} {v : β} :
     insertMany m [⟨k, v⟩] = m.insert k v :=
   ext (DHashMap.Raw.Const.insertMany_list_singleton h.out)
 
-theorem insertMany_cons [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List (α × β)}
+theorem insertMany_cons (h : m.WF) {l : List (α × β)}
     {k : α} {v : β} :
     insertMany m (⟨k, v⟩ :: l) = insertMany (m.insert k v) l :=
   ext (DHashMap.Raw.Const.insertMany_cons h.out)
@@ -873,16 +873,16 @@ theorem getD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
 variable {m : Raw α Unit}
 
 @[simp]
-theorem insertManyIfNewUnit_nil [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+theorem insertManyIfNewUnit_nil (h : m.WF) :
     insertManyIfNewUnit m [] = m :=
   ext (DHashMap.Raw.Const.insertManyIfNewUnit_nil h.out)
 
 @[simp]
-theorem insertManyIfNewUnit_list_singleton [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+theorem insertManyIfNewUnit_list_singleton (h : m.WF) {k : α} :
     insertManyIfNewUnit m [k] = m.insertIfNew k () :=
   ext (DHashMap.Raw.Const.insertManyIfNewUnit_list_singleton h.out)
 
-theorem insertManyIfNewUnit_cons [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} :
+theorem insertManyIfNewUnit_cons (h : m.WF) {l : List α} {k : α} :
     insertManyIfNewUnit m (k :: l) = insertManyIfNewUnit (m.insertIfNew k ()) l :=
   ext (DHashMap.Raw.Const.insertManyIfNewUnit_cons h.out)
 
@@ -1032,16 +1032,16 @@ namespace Raw
 variable [BEq α] [Hashable α]
 
 @[simp]
-theorem ofList_nil [EquivBEq α] [LawfulHashable α] :
+theorem ofList_nil :
     ofList ([] : List (α × β)) = ∅ :=
   ext DHashMap.Raw.Const.ofList_nil
 
 @[simp]
-theorem ofList_singleton [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+theorem ofList_singleton {k : α} {v : β} :
     ofList [⟨k, v⟩] = (∅ : Raw α β).insert k v :=
   ext DHashMap.Raw.Const.ofList_singleton
 
-theorem ofList_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β} {tl : List (α × β)} :
+theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : Raw α β).insert k v) tl :=
   ext DHashMap.Raw.Const.ofList_cons
 
@@ -1172,16 +1172,16 @@ theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
   DHashMap.Raw.Const.isEmpty_ofList
 
 @[simp]
-theorem unitOfList_nil [EquivBEq α] [LawfulHashable α] :
+theorem unitOfList_nil :
     unitOfList ([] : List α) = ∅ :=
   ext DHashMap.Raw.Const.unitOfList_nil
 
 @[simp]
-theorem unitOfList_singleton [EquivBEq α] [LawfulHashable α] {k : α} :
+theorem unitOfList_singleton {k : α} :
     unitOfList [k] = (∅ : Raw α Unit).insertIfNew k () :=
   ext DHashMap.Raw.Const.unitOfList_singleton
 
-theorem unitOfList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List α} :
+theorem unitOfList_cons {hd : α} {tl : List α} :
     unitOfList (hd :: tl) = insertManyIfNewUnit ((∅ : Raw α Unit).insertIfNew hd ()) tl :=
   ext DHashMap.Raw.Const.unitOfList_cons