From b43dfca34647df025964d2505f2c62425696550d Mon Sep 17 00:00:00 2001 From: jt0202 Date: Wed, 15 Jan 2025 10:41:21 +0100 Subject: [PATCH] Style fixes & simplified equality lemmas --- src/Std/Data/DHashMap/Internal/RawLemmas.lean | 20 ++++++------- src/Std/Data/DHashMap/Lemmas.lean | 24 ++++++++-------- src/Std/Data/DHashMap/RawLemmas.lean | 28 +++++++++---------- src/Std/Data/HashMap/Lemmas.lean | 14 +++++----- src/Std/Data/HashMap/RawLemmas.lean | 24 ++++++++-------- src/Std/Data/HashSet/Lemmas.lean | 10 +++---- src/Std/Data/HashSet/RawLemmas.lean | 12 ++++---- 7 files changed, 66 insertions(+), 66 deletions(-) diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index e08aa970e851..f04f9403231d 100644 --- 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 index c9e49d1c13be..7d2eebadcef7 100644 --- 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 index 4aa6d3e5774a..147a2ce3bd3d 100644 --- 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 index 19e2d073bc57..688be7b35a72 100644 --- 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 index bdcc2b0b857c..02d8442c622c 100644 --- 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 diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean index b943edb2fec8..b3c9d8b8858e 100644 --- a/src/Std/Data/HashSet/Lemmas.lean +++ b/src/Std/Data/HashSet/Lemmas.lean @@ -380,7 +380,7 @@ theorem insertMany_nil : ext HashMap.insertManyIfNewUnit_nil @[simp] -theorem insertMany_list_singleton [EquivBEq α] [LawfulHashable α] {k : α} : +theorem insertMany_list_singleton {k : α} : insertMany m [k] = m.insert k := ext HashMap.insertManyIfNewUnit_list_singleton @@ -412,7 +412,7 @@ theorem get?_insertMany_list_of_not_mem_of_contains_eq_false HashMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false not_mem contains_eq_false -theorem get?_insertMany_list_of_not_mem_false_of_mem [EquivBEq α] [LawfulHashable α] +theorem get?_insertMany_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : k == k') (not_mem : ¬ k ∈ m) (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) : @@ -507,16 +507,16 @@ end section @[simp] -theorem ofList_nil [EquivBEq α] [LawfulHashable α] : +theorem ofList_nil : ofList ([] : List α) = ∅ := ext HashMap.unitOfList_nil @[simp] -theorem ofList_singleton [EquivBEq α] [LawfulHashable α] {k : α} : +theorem ofList_singleton {k : α} : ofList [k] = (∅ : HashSet α).insert k := ext HashMap.unitOfList_singleton -theorem ofList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List α} : +theorem ofList_cons {hd : α} {tl : List α} : ofList (hd :: tl) = insertMany ((∅ : HashSet α).insert hd) tl := ext HashMap.unitOfList_cons diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index b527824e97c9..344cd8e2667f 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -391,16 +391,16 @@ theorem distinct_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) : HashMap.Raw.distinct_keys h.1 @[simp] -theorem insertMany_nil [EquivBEq α] [LawfulHashable α] (h : m.WF) : +theorem insertMany_nil (h : m.WF) : insertMany m [] = m := ext (HashMap.Raw.insertManyIfNewUnit_nil h.1) @[simp] -theorem insertMany_list_singleton [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} : +theorem insertMany_list_singleton (h : m.WF) {k : α} : insertMany m [k] = m.insert k := ext (HashMap.Raw.insertManyIfNewUnit_list_singleton h.1) -theorem insertMany_cons [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} : +theorem insertMany_cons (h : m.WF) {l : List α} {k : α} : insertMany m (k :: l) = insertMany (m.insert k) l := ext (HashMap.Raw.insertManyIfNewUnit_cons h.1) @@ -519,16 +519,16 @@ theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF) HashMap.Raw.isEmpty_insertManyIfNewUnit_list h.1 @[simp] -theorem ofList_nil [EquivBEq α] [LawfulHashable α] : +theorem ofList_nil : ofList ([] : List α) = ∅ := ext HashMap.Raw.unitOfList_nil @[simp] -theorem ofList_singleton [EquivBEq α] [LawfulHashable α] {k : α} : +theorem ofList_singleton {k : α} : ofList [k] = (∅ : Raw α).insert k := ext HashMap.Raw.unitOfList_singleton -theorem ofList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List α} : +theorem ofList_cons {hd : α} {tl : List α} : ofList (hd :: tl) = insertMany ((∅ : Raw α).insert hd) tl := ext HashMap.Raw.unitOfList_cons